From 05fc195f4e6e0a194323e68efa0d18dafece96ae Mon Sep 17 00:00:00 2001 From: QGarchery Date: Fri, 8 Feb 2019 07:51:05 +0100 Subject: tactic notations (#31) --- examples/Example.v | 15 ++++++------ src/Tactics.v | 14 +++++------ unit-tests/Tests_verit.v | 60 ++++++++++++++++++++++++------------------------ 3 files changed, 45 insertions(+), 44 deletions(-) diff --git a/examples/Example.v b/examples/Example.v index f7877b7..4b2fda9 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -152,6 +152,7 @@ Proof. smt. Qed. +(* From cvc4_bool : Uncaught exception Not_found *) (* Goal forall (a b c d: farray Z Z), *) (* b[0 <- 4] = c -> *) (* d = b[0 <- 4][1 <- 4] -> *) @@ -258,7 +259,7 @@ Qed. Open Scope Z_scope. -(* Some examples of using verit with lemmas. Use +(* Some examples of using verit with lemmas. Use to temporarily add the lemmas H1 .. Hn to the verit environment. *) Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, @@ -266,7 +267,7 @@ Lemma const_fun_is_eq_val_0 : forall x, f x =? f 0. Proof. intros f Hf. - verit_bool_base Hf; vauto. + verit Hf. Qed. Section Without_lemmas. @@ -285,7 +286,7 @@ Section With_lemmas. Lemma fSS2: forall x, f (x + 2) =? f x + 2 * k. - Proof. verit_bool_base f_k_linear; vauto. Qed. + Proof. verit f_k_linear. Qed. End With_lemmas. (* You can use to permanently add the lemmas H1 .. Hn to @@ -310,7 +311,7 @@ Section NonLinear. (mult (3 + a) b =? mult 3 b + mult a b). Proof. intro H. - verit_bool_base H; vauto. + verit H. Qed. End NonLinear. @@ -337,14 +338,14 @@ Section group. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit_bool_base pe'; vauto. Qed. + Proof. intros pe'. verit pe'. Qed. Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit_bool_base H; vauto. Qed. + Proof. intro H. verit H. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit_bool_base H; vauto. Qed. + Proof. intro H. verit H. Qed. Clear_lemmas. End group. diff --git a/src/Tactics.v b/src/Tactics.v index 23818fb..4e193ca 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -74,11 +74,11 @@ Ltac vauto := apply H); auto. -Ltac verit_bool := - verit_bool_base; vauto. +Tactic Notation "verit_bool" constr_list(h) := + verit_bool_base h; vauto. -Ltac verit_bool_no_check := - verit_bool_no_check_base; vauto. +Tactic Notation "verit_bool_no_check" constr_list(h) := + verit_bool_no_check_base h; vauto. (** Tactics in Prop **) @@ -86,8 +86,8 @@ Ltac verit_bool_no_check := Ltac zchaff := prop2bool; zchaff_bool; bool2prop. Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. -Ltac verit := prop2bool; verit_bool; bool2prop. -Ltac verit_no_check := prop2bool; verit_bool_no_check; bool2prop. +Tactic Notation "verit" constr_list(h) := prop2bool; verit_bool h; bool2prop. +Tactic Notation "verit_no_check" constr_list(h) := prop2bool; verit_bool_no_check h; bool2prop. Ltac cvc4 := prop2bool; cvc4_bool; bool2prop. Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. @@ -110,5 +110,5 @@ Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. (* end; *) (* bool2prop. *) -Ltac smt := (prop2bool; try verit_bool; cvc4_bool; try verit_bool; bool2prop). +Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop). Ltac smt_no_check := (prop2bool; try verit_bool_no_check; cvc4_bool_no_check; try verit_bool_no_check; bool2prop). diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 9117864..6a22f8e 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -26,13 +26,13 @@ Proof. verit. Qed. -(* In standard coq we need decidability of Int31.digits *) +(* (* In standard coq we need decidability of Int31.digits *) *) (* Lemma fun_const : *) (* forall f (g : int -> int -> bool), *) (* (forall x, g (f x) 2) -> g (f 3) 2. *) (* Proof. *) (* intros f g Hf. *) -(* verit_base Hf; vauto. *) +(* 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. *) @@ -41,12 +41,12 @@ Qed. Open Scope Z_scope. + Lemma fun_const2 : forall f (g : Z -> Z -> bool), (forall x, g (f x) 2) -> g (f 3) 2. Proof. - intros f g Hf. - verit_bool_base Hf; vauto. + intros f g Hf. verit Hf. Qed. (* Toplevel input, characters 916-942: @@ -565,7 +565,6 @@ Qed. Goal forall a , (xorb a a) || negb (xorb a a). verit. Qed. -Print Unnamed_thm5. Goal forall a, (a||negb a) || negb (a||negb a). verit. @@ -1021,85 +1020,85 @@ Proof. Qed. -(* Some examples of using verit with lemmas. Use +(* Some examples of using verit with lemmas. Use to temporarily add the lemmas H1 .. Hn to the verit environment. *) Lemma taut1 : forall f, f 2 =? 0 -> f 2 =? 0. -Proof. intros f p. verit_bool_base p; vauto. Qed. +Proof. intros f p. verit p. Qed. Lemma taut2 : forall f, 0 =? f 2 -> 0 =?f 2. -Proof. intros f p. verit_bool_base p; vauto. Qed. +Proof. intros f p. verit p. Qed. Lemma taut3 : forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0. -Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed. +Proof. intros f p1 p2. verit p1 p2. Qed. Lemma taut4 : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. -Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed. +Proof. intros f p1 p2. verit p1 p2. Qed. Lemma test_eq_sym a b : implb (a =? b) (b =? a). Proof. verit. Qed. Lemma taut5 : forall f, 0 =? f 2 -> f 2 =? 0. -Proof. intros f p. verit_bool_base p; vauto. Qed. +Proof. intros f p. verit p. Qed. Lemma fun_const_Z : forall f , (forall x, f x =? 2) -> f 3 =? 2. -Proof. intros f Hf. verit_bool_base Hf; vauto. Qed. +Proof. intros f Hf. verit Hf. Qed. Lemma lid (A : bool) : A -> A. -Proof. intro a. verit_bool_base a; vauto. Qed. +Proof. intro a. verit a. Qed. Lemma lpartial_id A : (xorb A A) -> (xorb A A). -Proof. intro xa. verit_bool_base xa; vauto. Qed. +Proof. intro xa. verit xa. Qed. Lemma llia1 X Y Z: (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) -> (X + Y <=? 10) || (X + Z <=? 12). -Proof. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma llia2 X: X - 3 =? 7 -> X >=? 10. -Proof. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma llia3 X Y: X >? Y -> Y + 1 <=? X. -Proof. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma llia6 X: andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10. -Proof. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma even_odd b1 b2 x1 x2: (ifb b1 (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. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma lcongr1 (a b : Z) (P : Z -> bool) f: (f a =? b) -> (P (f a)) -> P b. -Proof. intros eqfab pfa. verit_bool_base eqfab pfa; vauto. Qed. +Proof. intros eqfab pfa. verit eqfab pfa. Qed. Lemma lcongr2 (f:Z -> Z -> Z) x y z: x =? y -> f z x =? f z y. -Proof. intro p. verit_bool_base p; vauto. Qed. +Proof. intro p. verit p. Qed. Lemma lcongr3 (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. -Proof. intros eqxy pzx. verit_bool_base eqxy pzx; vauto. Qed. +Proof. intros eqxy pzx. verit eqxy pzx. Qed. Lemma test20 : forall x, (forall a, a 0 <=? x = false. -Proof. intros x H. verit_bool_base H; vauto. Qed. +Proof. intros x H. verit H. Qed. Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). -Proof. intros x H. verit_bool_base H; vauto. Qed. +Proof. intros x H. verit H. Qed. Lemma un_menteur (a b c d : Z) dit: dit a =? c -> @@ -1108,13 +1107,13 @@ Lemma un_menteur (a b c d : Z) dit: (a =? c) || (a =? d) -> (b =? c) || (b =? d) -> a =? d. -Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. +Proof. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed. 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_bool_base Hf; vauto. Qed. +Proof. intros f Hf. verit Hf. Qed. (* You can use to permanently add the lemmas H1 .. Hn to the environment. If you did so in a section then, at the end of the section, @@ -1193,7 +1192,7 @@ End mult3. (* Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *) (* Lemma mult_1_x : forall x, mult 1 x =? x. *) -(* Proof. verit_bool_base mult_0 mult_Sx. *) +(* Proof. verit mult_0 mult_Sx. *) (* Qed. *) (* End mult. *) @@ -1325,15 +1324,16 @@ Section group. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit_bool_base pe'; vauto. Qed. + Proof. intros pe'. verit pe'. Qed. Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit_bool_base H; vauto. Qed. + Proof. intro H. verit H. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit_bool_base H; vauto. Qed. + Proof. intro H. verit H. Qed. Clear_lemmas. End group. + -- cgit