diff options
| -rw-r--r-- | README.md | 30 | ||||
| -rw-r--r-- | examples/Example.v | 183 |
2 files changed, 119 insertions, 94 deletions
@@ -108,6 +108,10 @@ forall l, b1 = b2 where `l` is a quantifier-free list of variables and `b1` and `b2` are expressions of type `bool`. +A more efficient version of this tactic, called `zchaff_no_check`, +performs only the check at `Qed`. (Thus it is safe, but a proof may fail +at `Qed` even if everything went through during proof elaboration.) + #### veriT @@ -156,12 +160,14 @@ The theories that are currently supported by these commands are `QF_UF` ##### veriT as a Coq decision procedure -The `verit_bool` tactic can be used to solve any goal of the form: +The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` where `l` is a quantifier-free list of variables and `b1` and `b2` are -expressions of type `bool`. +expressions of type `bool`. This tactic *supports quantifiers*: it takes +optional arguments which are names of universally quantified +lemmas/hypotheses that can be used to solve the goal. In addition, the `verit` tactic applies to Coq goals of sort `Prop`: it first converts the goal into a term of type `bool` (thanks to the @@ -172,6 +178,10 @@ The theories that are currently supported by these tactics are `QF_UF` (theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL` (integer difference logic), and their combinations. +A more efficient version of this tactic, called `verit_no_check`, +performs only the check at `Qed`. (Thus it is safe, but a proof may fail +at `Qed` even if everything went through during proof elaboration.) + #### CVC4 @@ -242,6 +252,10 @@ The theories that are currently supported by these tactics are `QF_UF` (integer difference logic), `QF_BV` (theory of fixed-size bit vectors), `QF_A` (theory of arrays), and their combinations. +A more efficient version of this tactic, called `cvc4_no_check`, +performs only the check at `Qed`. (Thus it is safe, but a proof may fail +at `Qed` even if everything went through during proof elaboration.) + ### The smt tactic @@ -251,3 +265,15 @@ first converts the goal to a term of type `bool` (thanks to the `cvc4_bool` and `verit_bool` tactics, and it finally converts any unsolved subgoals back to `Prop`, thus offering to the user the possibility to solve these (usually simpler) subgoals. + +A more efficient version of this tactic, called `smt_no_check`, +performs only the check at `Qed`. (Thus it is safe, but a proof may fail +at `Qed` even if everything went through during proof elaboration.) + + +### Conversion tactics + +SMTCoq provides conversion tactics, to inject various integer types into +the type Z supported by SMTCoq. They can be called before the other +SMTCoq tactics. These tactics are named `nat_convert`, `N_convert` and +`pos_convert`. They can be combined. diff --git a/examples/Example.v b/examples/Example.v index 5c740d6..5bb1a83 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -62,7 +62,10 @@ Proof. zchaff. Qed. -Goal forall a b c, +Goal forall (i j k : Z), + let a := Z.eqb i j in + let b := Z.eqb j k in + let c := Z.eqb k i in (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. Proof. zchaff. @@ -73,7 +76,8 @@ Qed. variable), which handle - propositional logic - theory of equality - - linear integer arithmetic *) + - linear integer arithmetic + - universally quantified hypotheses *) Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false. Proof. @@ -107,6 +111,57 @@ Proof. Qed. +(*Some examples of using verit with lemmas. Use <verit H1 .. Hn> + to temporarily add the lemmas H1 .. Hn to the verit environment. *) + +Lemma const_fun_is_eq_val_0 : + forall f : Z -> Z, + (forall a b, f a =? f b) -> + forall x, f x =? f 0. +Proof. + intros f Hf. + verit Hf. +Qed. + +Section With_lemmas. + Variable f : Z -> Z. + Variable k : Z. + Hypothesis f_k_linear : forall x, f (x + 1) =? f x + k. + + Lemma fSS2: + forall x, f (x + 2) =? f x + 2 * k. + Proof. verit_no_check f_k_linear. Qed. +End With_lemmas. + +(* Instantiating a lemma with multiple quantifiers *) +Section NonLinear. + Lemma distr_right_inst a b (mult : Z -> Z -> Z) : + (forall x y z, mult (x + y) z =? mult x z + mult y z) -> + (mult (3 + a) b =? mult 3 b + mult a b). + Proof. + intro H. + verit H. + Qed. +End NonLinear. + +(* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to + the environment. If you did so in a section then, at the end of the section, + you should use <Clear_lemmas> to empty the globally added lemmas because + those lemmas won't be available outside of the section. *) + +Section mult3. + Variable mult3 : Z -> Z. + Hypothesis mult3_0 : mult3 0 =? 0. + Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. + Add_lemmas mult3_0 mult3_Sn. + + Lemma mult_3_4_12 : mult3 4 =? 12. + Proof. verit. Qed. + + Clear_lemmas. +End mult3. + + (* Examples of the smt tactic (requires verit and cvc4 in your PATH environment variable): - propositional logic @@ -188,7 +243,9 @@ Proof. Qed. -(** Examples of using the conversion tactics **) +(** SMTCoq also provides conversion tactics, to inject various integer + types into the type Z supported by SMTCoq. They can be called before + the standard SMTCoq tactics. **) Local Open Scope positive_scope. @@ -197,8 +254,8 @@ Goal forall (f : positive -> positive) (x y : positive), ((f (x + 3)) <=? (f y)) = true. Proof. -pos_convert. -verit. + pos_convert. + verit. Qed. Goal forall (f : positive -> positive) (x y : positive), @@ -206,8 +263,8 @@ Goal forall (f : positive -> positive) (x y : positive), ((3 <? y) && ((f (x + 3)) <=? (f y))) = true. Proof. -pos_convert. -verit. + pos_convert. + verit. Qed. Local Close Scope positive_scope. @@ -215,21 +272,21 @@ Local Close Scope positive_scope. Local Open Scope N_scope. Goal forall (f : N -> N) (x y : N), - implb ((x + 3) =? y) - ((f (x + 3)) <=? (f y)) - = true. + implb ((x + 3) =? y) + ((f (x + 3)) <=? (f y)) + = true. Proof. -N_convert. -verit. + N_convert. + verit. Qed. Goal forall (f : N -> N) (x y : N), - implb ((x + 3) =? y) - ((2 <? y) && ((f (x + 3)) <=? (f y))) - = true. + implb ((x + 3) =? y) + ((2 <? y) && ((f (x + 3)) <=? (f y))) + = true. Proof. -N_convert. -verit. + N_convert. + verit. Qed. Local Close Scope N_scope. @@ -238,21 +295,21 @@ Require Import NPeano. Local Open Scope nat_scope. Goal forall (f : nat -> nat) (x y : nat), - implb (Nat.eqb (x + 3) y) - ((f (x + 3)) <=? (f y)) - = true. + implb (Nat.eqb (x + 3) y) + ((f (x + 3)) <=? (f y)) + = true. Proof. -nat_convert. -verit. + nat_convert. + verit. Qed. Goal forall (f : nat -> nat) (x y : nat), - implb (Nat.eqb (x + 3) y) - ((2 <? y) && ((f (x + 3)) <=? (f y))) - = true. + implb (Nat.eqb (x + 3) y) + ((2 <? y) && ((f (x + 3)) <=? (f y))) + = true. Proof. -nat_convert. -verit. + nat_convert. + verit. Qed. Local Close Scope nat_scope. @@ -263,75 +320,17 @@ Goal forall f : positive -> nat -> N, forall (x : positive) (y : nat), (implb (Nat.eqb y 7) (implb (f 3%positive 7%nat =? 12)%N (f x y =? 12)%N)) = true. -pos_convert. -nat_convert. -N_convert. -verit. + pos_convert. + nat_convert. + N_convert. + verit. Qed. Open Scope Z_scope. -(** Some examples of using verit with lemmas. Use <verit H1 .. Hn> - to temporarily add the lemmas H1 .. Hn to the verit environment. **) - -Lemma const_fun_is_eq_val_0 : - forall f : Z -> Z, - (forall a b, f a =? f b) -> - forall x, f x =? f 0. -Proof. - intros f Hf. - verit Hf. -Qed. - -Section With_lemmas. - Variable f : Z -> Z. - Variable k : Z. - Hypothesis f_k_linear : forall x, f (x + 1) =? f x + k. - - Lemma fSS2: - forall x, f (x + 2) =? f x + 2 * k. - Proof. verit_no_check f_k_linear. Qed. -End With_lemmas. - -(* Can't express the k-linearity of a function without lemmas *) -Section Without_lemmas. - Lemma fSS: - forall (f : Z -> Z) (k : Z) (x : Z), - implb (f (x+1) =? f x + k) - (implb (f (x+2) =? f (x+1) + k) - (f (x+2) =? f x + 2 * k)). - Proof. verit. Qed. -End Without_lemmas. - -(* Instantiating a lemma with multiple quantifiers *) -Section NonLinear. - Lemma distr_right_inst a b (mult : Z -> Z -> Z) : - (forall x y z, mult (x + y) z =? mult x z + mult y z) -> - (mult (3 + a) b =? mult 3 b + mult a b). - Proof. - intro H. - verit H. - Qed. -End NonLinear. - - -(** You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to - the environment. If you did so in a section then, at the end of the section, - you should use <Clear_lemmas> to empty the globally added lemmas because - those lemmas won't be available outside of the section. **) - -Section mult3. - Variable mult3 : Z -> Z. - Hypothesis mult3_0 : mult3 0 =? 0. - Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. - Add_lemmas mult3_0 mult3_Sn. - - Lemma mult_3_4_12 : mult3 4 =? 12. - Proof. verit_no_check. Qed. - - Clear_lemmas. -End mult3. +(** Now more insightful examples. The first one automatically proves + properties in group theory. **) Section group. Variable op : Z -> Z -> Z. @@ -375,7 +374,7 @@ Section group. End group. -(* Example coming from CompCert, slightly revisited. +(* A full example coming from CompCert, slightly revisited. See: https://hal.inria.fr/inria-00289542 https://xavierleroy.org/memory-model/doc/Memory.html (Section 3) *) |