aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/Example.v15
-rw-r--r--src/Tactics.v14
-rw-r--r--unit-tests/Tests_verit.v60
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 <verit_base H1 .. Hn; vauto>
+(* 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,
@@ -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 <Add_lemmas H1 .. Hn> 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 <verit_bool_base H1 .. Hn; vauto>
+(* Some examples of using verit with lemmas. Use <verit H1 .. Hn>
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 <? x) -> 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 <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,
@@ -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.
+
generated by cgit (git 2.34.1) at 2024-06-29 07:38:21 +0000