diff options
author | QGarchery <QGarchery@users.noreply.github.com> | 2019-02-12 14:52:13 +0100 |
---|---|---|
committer | ckeller <ckeller@users.noreply.github.com> | 2019-02-12 14:52:13 +0100 |
commit | 66f68dfa5aac0252563816d3abef9456e8622adf (patch) | |
tree | ded537507b8eb5b432a528fb7598773052275629 /examples/Example.v | |
parent | 769c2054cc14af50e70a38b0d2340ae6170863e0 (diff) | |
download | smtcoq-66f68dfa5aac0252563816d3abef9456e8622adf.tar.gz smtcoq-66f68dfa5aac0252563816d3abef9456e8622adf.zip |
Cleaning (#35)
Removing tests from the example folder
More commentaries in Example.v
Diffstat (limited to 'examples/Example.v')
-rw-r--r-- | examples/Example.v | 62 |
1 files changed, 37 insertions, 25 deletions
diff --git a/examples/Example.v b/examples/Example.v index d9523ca..e4a50da 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -188,7 +188,7 @@ Proof. Qed. -(* Examples of using the conversion tactics *) +(** Examples of using the conversion tactics **) Local Open Scope positive_scope. @@ -271,8 +271,10 @@ 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. *) + +(** 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) -> @@ -282,15 +284,6 @@ Proof. verit Hf. Qed. -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. - Section With_lemmas. Variable f : Z -> Z. Variable k : Z. @@ -301,37 +294,52 @@ Section With_lemmas. Proof. verit_no_check f_k_linear. Qed. End With_lemmas. -(* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to +(* 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. *) + 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 mult3_21 : mult3 4 =? 12. + Lemma mult_3_4_12 : mult3 4 =? 12. Proof. verit_no_check. Qed. Clear_lemmas. End mult3. -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. - Section group. Variable op : Z -> Z -> Z. Variable inv : Z -> Z. Variable e : Z. + (* We can prove automatically that we have a group if we only have the "left" versions + of the axioms of a group *) Hypothesis associative : forall a b c : Z, op a (op b c) =? op (op a b) c. Hypothesis inverse : @@ -339,15 +347,19 @@ Section group. Hypothesis identity : forall a : Z, (op e a =? a). Add_lemmas associative identity inverse. + + (* The "right" version of inverse *) Lemma inverse' : forall a : Z, (op a (inv a) =? e). Proof. verit_no_check. Qed. Add_lemmas inverse'. + (* The "right" version of identity *) Lemma identity' : forall a : Z, (op a e =? a). Proof. verit_no_check. Qed. Add_lemmas identity'. + (* Some other interesting facts about groups *) Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. Proof. intros pe'. verit pe'. Qed. |