diff options
author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
---|---|---|
committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /examples/Example.v | |
parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip |
Adding support for lemmas in the command verit
Diffstat (limited to 'examples/Example.v')
-rw-r--r-- | examples/Example.v | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/examples/Example.v b/examples/Example.v index 0c50909..60d1a2b 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -136,3 +136,79 @@ verit. Qed. Local Close Scope nat_scope. + +Open Scope Z_scope. + +(* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto> + 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_base Hf; vauto. +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. + 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_base f_k_linear; vauto. Qed. +End With_lemmas. + +(* 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 mult3_21 : mult3 7 =? 21. + Proof. verit. Qed. + + Clear_lemmas. +End mult3. + +Section group. + Variable op : Z -> Z -> Z. + Variable inv : Z -> Z. + Variable e : Z. + + Hypothesis associative : + forall a b c : Z, op a (op b c) =? op (op a b) c. + Hypothesis identity : + forall a : Z, (op e a =? a) && (op a e =? a). + Hypothesis inverse : + forall a : Z, (op a (inv a) =? e) && (op (inv a) a =? e). + Add_lemmas associative identity inverse. + + Lemma unique_identity e': + (forall z, op e' z =? z) -> e' =? e. + Proof. intros pe'. verit_base pe'; vauto. Qed. + + Lemma simplification_right x1 x2 y: + op x1 y =? op x2 y -> x1 =? x2. + Proof. intro H. verit_base H; vauto. Qed. + + Lemma simplification_left x1 x2 y: + op y x1 =? op y x2 -> x1 =? x2. + Proof. intro H. verit_base H; vauto. Qed. + + Clear_lemmas. +End group. |