I’ve just added blastLib.BBLAST_PROVE_TAC, which calls blastLib.BBLAST_PROVE on the current goal.
If this bit-vector procedure succeeds in proving your goal then a witness (which is the one used for the proof) can be viewed by attempting to prove the goal’s negation. In this case: > blastLib.BBLAST_PROVE ``!r:word8. ~(100w ≤₊ r + 251w ∧ r + 251w <₊ 200w)``; Found counterexample: r -> 112w Exception- SAT_cex |- ¬(100w ≤₊ 112w + 251w ∧ 112w + 251w <₊ 200w) ⇔ F raised This will work for ordinary propositional formula as well. For example: > blastLib.BBLAST_PROVE ``a = b:bool``; will give you “b" is F and “a" is T as the counterexample. I’m not aware of other HOL4 decision procedures that can readily supply counterexamples, e.g. METIS_PROVE and numLib.ARITH_PROVE don’t. Isabelle/HOL has much better support for this sort of thing: http://www4.in.tum.de/~blanchet/nitpick.html Others can probably comment on how well it does in producing counterexamples for arithmetic goals. - Anthony On 28 Jun 2014, at 02:56, Jiaqi Tan <tanji...@cmu.edu> wrote: > Hi Anthony, > > Thank you for the pointer! That works and I am able to prove the theorem. > > Does blastLib (or any other HOL4 library) also support the generation of > witnesses for such theorems? > > Thank you! > > Regards, > Jiaqi > > > > On Fri, Jun 27, 2014 at 6:23 PM, Anthony Fox <ac...@cam.ac.uk> wrote: > The tactic > > ACCEPT_TAC > (blastLib.BBLAST_PROVE > ``?r:word8. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``) > > will prove your goal. If you’re doing this sort of thing a lot then you > should consider wrapping this process up into a custom tactic. > > - Anthony > > On 27 Jun 2014, at 18:49, Jiaqi Tan <tanji...@cmu.edu> wrote: > > > Hi, > > > > Is it possible, using just the built-in HOL4 libraries/theorems, to > > automatically generate witnesses for an existentially quantified theorem > > over a finite set? > > > > Specifically, I have theorems of the form: > > {r − 5w} ⊆ {a | 100w ≤₊ a ∧ a <₊ 200w} > > > > Where the variable r is of type word8, and the set specification is also > > over word8. > > > > I tried simplifying using the following simplification sets: > > > > SIMP_TAC (std_ss ++ ARITH_ss ++ wordsLib.WORD_ss ++ > > pred_setSimps.PRED_SET_ss) [] > > > > And this yields the subgoal: > > val it = [([],``∃r. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)]: goal list > > > > Is it possible, using just the available theorems in the base HOL4 > > installation, to automatically discharge such existential goals of > > membership in fixed size word sets? > > > > Thank you! > > > > Regards, > > Jiaqi Tan > > > > > > > > ------------------------------------------------------------------------------ > > Open source business process management suite built on Java and Eclipse > > Turn processes into business applications with Bonita BPM Community Edition > > Quickly connect people, data, and systems into organized workflows > > Winner of BOSSIE, CODIE, OW2 and Gartner awards > > http://p.sf.net/sfu/Bonitasoft_______________________________________________ > > hol-info mailing list > > hol-info@lists.sourceforge.net > > https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ Open source business process management suite built on Java and Eclipse Turn processes into business applications with Bonita BPM Community Edition Quickly connect people, data, and systems into organized workflows Winner of BOSSIE, CODIE, OW2 and Gartner awards http://p.sf.net/sfu/Bonitasoft _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
