diff options
| -rw-r--r-- | examples/Example.v | 62 | ||||
| -rw-r--r-- | examples/Non_terminating.v | 23 | ||||
| -rw-r--r-- | examples/one_equality_switch.v | 37 | ||||
| -rw-r--r-- | examples/switching_input.v | 22 | ||||
| -rw-r--r-- | examples/sym_zeq.v | 24 | ||||
| -rw-r--r-- | unit-tests/Tests_verit.v | 144 | ||||
| -rw-r--r-- | unit-tests/debug_coq.v (renamed from unit-tests/debug_coq) | 2 |
7 files changed, 176 insertions, 138 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. diff --git a/examples/Non_terminating.v b/examples/Non_terminating.v deleted file mode 100644 index 7dad08f..0000000 --- a/examples/Non_terminating.v +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -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 deleted file mode 100644 index 61fd9c7..0000000 --- a/examples/one_equality_switch.v +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -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 deleted file mode 100644 index 629a3ad..0000000 --- a/examples/switching_input.v +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -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 deleted file mode 100644 index 1c4be83..0000000 --- a/examples/sym_zeq.v +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -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. diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 6a22f8e..f374b1b 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -33,11 +33,15 @@ Qed. (* Proof. *) (* intros f g Hf. *) (* verit Hf. *) -(* exists (fun x y => match (x, y) with (Int31.D0, Int31.D0) | (Int31.D1, Int31.D1) => true | _ => false end). *) -(* intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *) -(* exists Int63Native.eqb. *) -(* apply Int63Properties.reflect_eqb. *) -(* Qed. *) +(* -admit. *) +(* (* a proof that there is a decidable equality on digits : *) *) +(* (* exists (fun x y => match (x, y) with (Int31.D0, Int31.D0) +| (Int31.D1, Int31.D1) => true | _ => false end). *) *) +(* (* intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *) *) +(* (* exists Int63Native.eqb. *) *) +(* (* apply Int63Properties.reflect_eqb. *) *) +(* -apply int63_compdec. *) + Open Scope Z_scope. @@ -1178,7 +1182,7 @@ Section mult3. Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. Add_lemmas mult3_0 mult3_Sn. - Lemma mult3_21 : mult3 4 =? 12. + Lemma mult3_4_12 : mult3 4 =? 12. Proof. verit. Qed. (* slow to verify with standard coq *) Clear_lemmas. @@ -1337,3 +1341,131 @@ Section group. Clear_lemmas. End group. +Section Linear1. + Parameter f : Z -> Z. + Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). + + (* Cuts are not automatically proved when one equality is switched *) + Lemma f_1 : f 1 =? 1. + Proof. + verit_bool f_spec; replace (0 =? f 0) with (f 0 =? 0) by apply Z.eqb_sym; auto. + Qed. +End Linear1. + +Section Linear2. + Parameter g : Z -> Z. + + Axiom g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). + +(* The call to veriT does not terminate *) +(* Lemma apply_lemma_infinite : *) +(* forall x y, Z.eqb (g (x + y)) ((g x) + y * 2). *) +(* Proof. verit g_2_linear. *) +End Linear2. + +Section Input_switched1. + Parameter m : Z -> Z. + + Axiom m_0 : m 0 =? 5. + + (* veriT switches the input lemma in this case *) + Lemma cinq_m_0 : m 0 =? 5. + Proof. verit m_0. Qed. +End Input_switched1. + +Section Input_switched2. + Parameter h : Z -> Z -> Z. + + Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + + (* veriT switches the input lemma in this case *) + Lemma h_1_0 : h 1 0 =? h 0 0. + Proof. verit h_Sm_n. Qed. +End Input_switched2. + + +(** Examples of using the conversion tactics **) + +Local Open Scope positive_scope. + +Goal forall (f : positive -> positive) (x y : positive), + implb ((x + 3) =? y) + ((f (x + 3)) <=? (f y)) + = true. +Proof. +pos_convert. +verit. +Qed. + +Goal forall (f : positive -> positive) (x y : positive), + implb ((x + 3) =? y) + ((3 <? y) && ((f (x + 3)) <=? (f y))) + = true. +Proof. +pos_convert. +verit. +Qed. + +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. +Proof. +N_convert. +verit. +Qed. + +Goal forall (f : N -> N) (x y : N), + implb ((x + 3) =? y) + ((2 <? y) && ((f (x + 3)) <=? (f y))) + = true. +Proof. +N_convert. +verit. +Qed. + +Local Close Scope N_scope. + +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. +Proof. +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. +Proof. +nat_convert. +verit. +Qed. + +Local Close Scope nat_scope. + +(* An example with all 3 types and a binary function *) +Goal forall f : positive -> nat -> N, forall (x : positive) (y : nat), + implb (x =? 3)%positive + (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. +Qed. + + +(* The tactic simpl does too much here : *) +(* Goal forall x, 3 + x = x + 3. *) +(* nat_convert. *) diff --git a/unit-tests/debug_coq b/unit-tests/debug_coq.v index 61b9fd9..9ed4b35 100644 --- a/unit-tests/debug_coq +++ b/unit-tests/debug_coq.v @@ -1,4 +1,4 @@ -(* This file is useful when the tactic goes through but not hte Qed *) +(* This file is useful when the tactic goes through but not the Qed *) (* It is works as is for standard-coq and checker_b but can be adapted for native-coq and/or checker_eq *) (* Paste the environment and the following code : *) |