diff options
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Example.v | 88 | ||||
-rw-r--r-- | examples/Non_terminating.v | 11 | ||||
-rw-r--r-- | examples/one_equality_switch.v | 25 | ||||
-rw-r--r-- | examples/switching_input.v | 10 | ||||
-rw-r--r-- | examples/sym_zeq.v | 12 |
5 files changed, 139 insertions, 7 deletions
diff --git a/examples/Example.v b/examples/Example.v index 2f3ca73..60d1a2b 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -53,23 +53,21 @@ Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), - (negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b). + negb (f a =? b) || negb (P (f a)) || (P b). Proof. verit. Qed. - Goal forall b1 b2 x1 x2, implb (ifb b1 - (ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2))) - (ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2)))) - ((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)). + (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) + (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) + ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). Proof. verit. Qed. - (* Examples of using the conversion tactics *) Local Open Scope positive_scope. @@ -137,4 +135,80 @@ nat_convert. verit. Qed. -Local Close Scope nat_scope.
\ No newline at end of file +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. diff --git a/examples/Non_terminating.v b/examples/Non_terminating.v new file mode 100644 index 0000000..087301a --- /dev/null +++ b/examples/Non_terminating.v @@ -0,0 +1,11 @@ +Require Import SMTCoq. + +Parameter g : Z -> Z. + +Axiom g_2_linear : forall x, Zeq_bool (g (x + 1)) ((g x) + 2). + +Lemma apply_lemma_multiple : + forall x y, Zeq_bool (g (x + y)) ((g x) + y * 2). + +Proof. + verit g_2_linear. diff --git a/examples/one_equality_switch.v b/examples/one_equality_switch.v new file mode 100644 index 0000000..3473d08 --- /dev/null +++ b/examples/one_equality_switch.v @@ -0,0 +1,25 @@ +Require Import SMTCoq. +Require Import Bool. +Local Open Scope int63_scope. + +Parameter f : Z -> Z. + +Lemma sym_zeq_bool x y : + Zeq_bool x y = Zeq_bool y x. + +Proof. + case_eq (Zeq_bool x y). + rewrite <- Zeq_is_eq_bool. intro H. symmetry. now rewrite <- Zeq_is_eq_bool. + symmetry. apply not_true_is_false. + intro H1. rewrite <- Zeq_is_eq_bool in H1. + symmetry in H1. rewrite Zeq_is_eq_bool in H1. + rewrite H in H1. discriminate H1. +Qed. + +Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). + +Lemma f_1 : f 1 =? 1. + +Proof. + verit_base f_spec; vauto; rewrite Z.eqb_sym; auto. +Qed. diff --git a/examples/switching_input.v b/examples/switching_input.v new file mode 100644 index 0000000..52261d8 --- /dev/null +++ b/examples/switching_input.v @@ -0,0 +1,10 @@ +Require Import SMTCoq. +Require Import Bool. +Local Open Scope int63_scope. + +Parameter m : Z -> Z. +Axiom m_0 : m 0 =? 5. + +Lemma cinq_m_0 : + m 0 =? 5. +Proof. verit_base m_0; vauto. Qed. diff --git a/examples/sym_zeq.v b/examples/sym_zeq.v new file mode 100644 index 0000000..b940490 --- /dev/null +++ b/examples/sym_zeq.v @@ -0,0 +1,12 @@ +Require Import SMTCoq. +Require Import Bool. +Local Open Scope int63_scope. + +Open Scope Z_scope. + +Parameter h : Z -> Z -> Z. +Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + +Lemma h_1_0 : + h 1 0 =? h 0 0. +Proof. verit_base h_Sm_n; vauto. Qed. |