Take hypotheses from the local context (#91)

* The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context
* `prop2bool_hyps` also apply to hypotheses not in the local context
* Second strategy for vauto (still incomplete)

6 files changed, 241 insertions, 85 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 25662ad..64d88cf 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -26,7 +26,11 @@ Ltac prop2bool :=
     match goal with
     | [ |- forall _ : ?t, _ ] =>
       lazymatch type of t with
-      | Prop => fail
+      | Prop =>
+        match t with
+        | forall _ : _, _ => intro
+        | _ => fail
+        end
       | _ => intro
       end
 
@@ -197,7 +201,7 @@ Ltac prop2bool_hyp H :=
     [ bool2prop; apply H | ];
 
     (* Replace the Prop version with the bool version *)
-    clear H; assert (H:=H'); clear H'
+    try clear H; let H := fresh H in assert (H:=H'); clear H'
   ].
 
 Ltac prop2bool_hyps Hs :=
@@ -220,11 +224,14 @@ Section Test.
     prop2bool_hyp basic.
     prop2bool_hyp no_eq.
     prop2bool_hyp uninterpreted_type.
+    admit.
+    prop2bool_hyp plus_n_O.
   Abort.
 
   Goal True.
   Proof.
-    prop2bool_hyps (basic, no_eq, uninterpreted_type).
+    prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, plus_O_n).
+    admit.
   Abort.
 End Test.
 
diff --git a/src/QInst.v b/src/QInst.v
index bb2cfd1..4ebdcc9 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -45,8 +45,11 @@ Proof.
   destruct a; destruct c; intuition.
 Qed.
 
-(* verit considers equality modulo its symmetry, so we have to recover the
-   right direction in the instances of the theorems *)
+(** verit considers equality modulo its symmetry, so we have to recover the
+    right direction in the instances of the theorems *)
+(* TODO: currently incomplete *)
+
+(* An auxiliary lemma to rewrite an eqb_of_compdec into its the symmetrical version *)
 Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) :
   eqb_of_compdec HA b a = eqb_of_compdec HA a b.
 Proof.
@@ -58,6 +61,10 @@ Proof.
       intro H1. elim H. symmetry. now rewrite compdec_eq_eqb.
 Qed.
 
+(* First strategy: change the order of all equalities in the goal or the
+   hypotheses
+   Incomplete: all or none of the equalities are changed, whereas we may
+   need to change some of them but not all of them *)
 Definition hidden_eq_Z (a b : Z) := (a =? b)%Z.
 Definition hidden_eq_U (A:Type) (HA:CompDec A) (a b : A) := eqb_of_compdec HA a b.
 Ltac apply_sym_hyp T :=
@@ -98,20 +105,63 @@ Ltac apply_sym_goal :=
            replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a);
            [ | now rewrite eqb_of_compdec_sym]
          end.
+Ltac strategy1 H :=
+  first [ apply H
+        | apply_sym_goal; apply H
+        | apply_sym_hyp H; apply H
+        | apply_sym_goal; apply_sym_hyp H; apply H
+        ].
+
+(* Second strategy: find the order of equalities
+   Incomplete: does not work if the lemma is quantified *)
+Ltac order_equalities g TH :=
+  match g with
+  | eqb_of_compdec ?HC ?a1 ?b1 =>
+    match TH with
+    | eqb_of_compdec _ ?a2 _ =>
+      first [ constr_eq a1 a2 | replace (eqb_of_compdec HC a1 b1) with (eqb_of_compdec HC b1 a1) by now rewrite eqb_of_compdec_sym ]
+    | _ => idtac
+    end
+  | Z.eqb ?a1 ?b1 =>
+    match TH with
+    | Z.eqb ?a2 _ =>
+      first [ constr_eq a1 a2 | replace (Z.eqb a1 b1) with (Z.eqb b1 a1) by now rewrite Z.eqb_sym ]
+    | _ => idtac
+    end
+  | ?f1 ?t1 =>
+    match TH with
+    | ?f2 ?t2 => order_equalities f1 f2; order_equalities t1 t2
+    | _ => idtac
+    end
+  | _ => idtac
+  end.
+Ltac strategy2 H :=
+  match goal with
+  | [ |- ?g ] =>
+    let TH := type of H in
+    order_equalities g TH;
+    apply H
+  end.
+
 
 (* An automatic tactic that takes into account all those transformations *)
 Ltac vauto :=
-  try (let H := fresh "H" in
+  try (unfold is_true;
+       let H := fresh "H" in
        intro H;
-       try apply H;
-       try (apply_sym_goal; apply H);
-       try (apply_sym_hyp H; apply H);
-       try (apply_sym_goal; apply_sym_hyp H; apply H);
-       match goal with
-       | [ |- is_true (negb ?A || ?B) ] =>
-         try (eapply impl_or_split_right; apply H);
-         eapply impl_or_split_left; apply H
-       end
+       first [ strategy1 H
+             | strategy2 H
+             | match goal with
+               | [ |- (negb ?A || ?B) = true ] =>
+                 first [ eapply impl_or_split_right;
+                         first [ strategy1 H
+                               | strategy2 H ]
+                       | eapply impl_or_split_left;
+                         first [ strategy1 H
+                               | strategy2 H ]
+                       ]
+               end
+             ]
       );
   auto.
 
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index ca5f3cc..6cbdbc0 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -452,7 +452,9 @@ let list_of_constr_tuple =
     let c, args = Structures.decompose_app t in
     if c = Lazy.force cpair then
       match args with
-        | [_;_;t;l] -> list_of_constr_tuple (l::acc) t
+        | [_;_;t1;t2] ->
+           let acc' = list_of_constr_tuple acc t1 in
+           list_of_constr_tuple acc' t2
         | _ -> assert false
     else
       t::acc
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 6ddf5a5..468de7a 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -17,11 +17,74 @@ Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances
 Declare ML Module "smtcoq_plugin".
 
 
-Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto.
-Tactic Notation "verit_bool"           := verit_bool_base (@None nat); vauto.
+(** Collect all the hypotheses from the context *)
 
-Tactic Notation "verit_bool_no_check" constr(h) := verit_bool_no_check_base (Some h); vauto.
-Tactic Notation "verit_bool_no_check"           := verit_bool_no_check_base (@None nat); vauto.
+Ltac get_hyps_acc acc k :=
+  match goal with
+  | [ H : ?P |- _ ] =>
+    let T := type of P in
+    match T with
+    | Prop =>
+      lazymatch P with
+      | id _ => fail
+      | _ =>
+        change P with (id P) in H;
+        match acc with
+        | Some ?t => get_hyps_acc (Some (H, t)) k
+        | None => get_hyps_acc (Some H) k
+        end
+      end
+    | _ => fail
+    end
+  | _ => k acc
+  end.
+
+Ltac eliminate_id :=
+  repeat match goal with
+  | [ H : ?P |- _ ] =>
+    lazymatch P with
+    | id ?Q => change P with Q in H
+    | _ => fail
+    end
+  end.
+
+Ltac get_hyps k := get_hyps_acc (@None nat) ltac:(fun Hs => eliminate_id; k Hs).
+
+
+Section Test.
+  Variable A : Type.
+  Hypothesis H1 : forall a:A, a = a.
+  Variable n : Z.
+  Hypothesis H2 : n = 17%Z.
+
+  Goal True.
+  Proof.
+    (* get_hyps ltac:(fun acc => idtac acc). *)
+  Abort.
+End Test.
+
+
+(** Tactics in bool *)
+
+Tactic Notation "verit_bool" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_base (Some (h, Hs))
+                   | None => verit_bool_base (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool"           :=
+  get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto).
+
+Tactic Notation "verit_bool_no_check" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_no_check_base (Some (h, Hs))
+                   | None => verit_bool_no_check_base (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool_no_check"           :=
+  get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto).
 
 
 (** Tactics in Prop **)
@@ -29,18 +92,58 @@ Tactic Notation "verit_bool_no_check"           := verit_bool_no_check_base (@No
 Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
 Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
 
-Tactic Notation "verit" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool h; bool2prop ] ].
-Tactic Notation "verit"           := prop2bool; [ .. | verit_bool  ; bool2prop ].
-Tactic Notation "verit_no_check" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool_no_check h; bool2prop ] ].
-Tactic Notation "verit_no_check"           := prop2bool; [ .. | verit_bool_no_check  ; bool2prop ].
+Tactic Notation "verit" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_base (Some (h, Hs)) ]
+                                   | None => verit_bool_base (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_base (Some Hs) ]
+                          | None => verit_bool_base (@None nat)
+                          end; vauto)
+  ].
+Tactic Notation "verit_no_check" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_no_check_base (Some (h, Hs)) ]
+                                   | None => verit_bool_no_check_base (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit_no_check"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_no_check_base (Some Hs) ]
+                          | None => verit_bool_no_check_base (@None nat)
+                          end; vauto)
+  ].
 
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
-Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool h ]); cvc4_bool; try (prop2bool_hyps h; [ .. | verit_bool h ]); bool2prop ]).
-Tactic Notation "smt"           := (prop2bool; [ .. | try verit_bool  ; cvc4_bool; try verit_bool  ; bool2prop ]).
-Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); cvc4_bool_no_check; try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); bool2prop]).
-Tactic Notation "smt_no_check"           := (prop2bool; [ .. | try verit_bool_no_check  ; cvc4_bool_no_check; try verit_bool_no_check  ; bool2prop]).
+Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try verit h; cvc4_bool; try verit h; bool2prop ]).
+Tactic Notation "smt"           := (prop2bool; [ .. | try verit  ; cvc4_bool; try verit  ; bool2prop ]).
+Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try verit_no_check h; cvc4_bool_no_check; try verit_no_check h; bool2prop]).
+Tactic Notation "smt_no_check"           := (prop2bool; [ .. | try verit_no_check  ; cvc4_bool_no_check; try verit_no_check  ; bool2prop]).
 
 
 
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v
index eb9744b..280ed17 100644
--- a/unit-tests/Tests_lfsc_tactics.v
+++ b/unit-tests/Tests_lfsc_tactics.v
@@ -714,13 +714,13 @@ Section A_BV_EUF_LIA_PR.
   Goal forall (x: bitvector 1), bv_subt x #b|0| = x.
   Proof using.
     smt.
-  Admitted.
+  Abort.
 
   (* The original issue (invalid) *)
   Goal forall (x: bitvector 1), bv_subt (bv_shl #b|0| x) #b|0| = #b|0|.
   Proof using.
     smt.
-  Admitted.
+  Abort.
 
 End A_BV_EUF_LIA_PR.
 
@@ -760,15 +760,15 @@ Section Group.
   (* Some other interesting facts about groups *)
   Lemma unique_identity e':
     (forall z, op e' z ==? z) -> e' ==? e.
-  Proof. intros pe'; smt pe'. Qed.
+  Proof. smt. Qed.
 
   Lemma simplification_right x1 x2 y:
       op x1 y ==? op x2 y -> x1 ==? x2.
-  Proof. intro H. smt_no_check (H, inverse'). Qed.
+  Proof. smt_no_check inverse'. Qed.
 
   Lemma simplification_left x1 x2 y:
       op y x1 ==? op y x2 -> x1 ==? x2.
-  Proof. intro H. smt_no_check (H, inverse'). Qed.
+  Proof. smt_no_check inverse'. Qed.
 
   Clear_lemmas.
 End Group.
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 59c40a1..a270fdd 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -30,9 +30,7 @@ Qed.
 Lemma fun_const2 :
   forall f (g : Z -> Z -> bool),
     (forall x, g (f x) 2) -> g (f 3) 2.
-Proof using.
-  intros f g Hf. verit Hf.
-Qed.
+Proof using. verit. Qed.
 
 
 (* Simple connectives *)
@@ -531,140 +529,140 @@ Qed.
 
 Lemma taut1_bool :
   forall f, f 2 =? 0 -> f 2 =? 0.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma taut1 :
   forall f, f 2 = 0 -> f 2 = 0.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma taut2_bool :
   forall f, 0 =? f 2 -> 0 =? f 2.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma taut2 :
   forall f, 0 = f 2 -> 0 = f 2.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma taut3_bool :
   forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0.
-Proof using. intros f p1 p2. verit (p1, p2). Qed.
+Proof using. verit. Qed.
 
 Lemma taut3 :
   forall f, f 2 = 0 -> f 3 = 5 -> f 2 = 0.
-Proof using. intros f p1 p2. verit (p1, p2). Qed.
+Proof using. verit. Qed.
 
 Lemma taut4_bool :
   forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0.
-Proof using. intros f p1 p2. verit (p1, p2). Qed.
+Proof using. verit. Qed.
 
 Lemma taut4 :
   forall f, f 3 = 5 -> f 2 = 0 -> f 2 = 0.
-Proof using. intros f p1 p2. verit (p1, p2). Qed.
+Proof using. verit. Qed.
 
 Lemma test_eq_sym a b : implb (a =? b) (b =? a).
 Proof using. verit. Qed.
 
 Lemma taut5_bool :
   forall f, 0 =? f 2 -> f 2 =? 0.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma taut5 :
   forall f, 0 = f 2 -> f 2 = 0.
-Proof using. intros f p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma fun_const_Z_bool :
   forall f , (forall x, f x =? 2) ->
              f 3 =? 2.
-Proof using. intros f Hf. verit Hf. Qed.
+Proof using. verit. Qed.
 
 Lemma fun_const_Z :
   forall f , (forall x, f x = 2) ->
              f 3 = 2.
-Proof using. intros f Hf. verit Hf. Qed.
+Proof using. verit. Qed.
 
 Lemma lid (A : bool) :  A -> A.
-Proof using. intro a. verit a. Qed.
+Proof using. verit. Qed.
 
 Lemma lpartial_id A :
   (xorb A A) -> (xorb A A).
-Proof using. intro xa. verit xa. Qed.
+Proof using. verit. Qed.
 
 Lemma llia1_bool X Y Z:
   (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) ->
   (X + Y <=? 10) || (X + Z <=? 12).
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia1 X Y Z:
   (X <= 3) /\ ((Y <= 7) \/ (Z <= 9)) ->
   (X + Y <= 10) \/ (X + Z <= 12).
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia2_bool X:
   X - 3 =? 7 -> X >=? 10.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia2 X:
   X - 3 = 7 -> X >= 10.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia3_bool X Y:
   X >? Y -> Y + 1 <=? X.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia3 X Y:
   X > Y -> Y + 1 <= X.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia6_bool X:
   andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma llia6 X:
   ((X - 3) <= 7) /\ (7 <= (X - 3)) -> X >= 10.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. 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 using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr1_bool (a b : Z) (P : Z -> bool) f:
   (f a =? b) -> (P (f a)) -> P b.
-Proof using. intros eqfab pfa. verit (eqfab, pfa). Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr1 (a b : Z) (P : Z -> bool) f:
   (f a = b) -> (P (f a)) -> P b.
-Proof using. intros eqfab pfa. verit (eqfab, pfa). Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr2_bool (f:Z -> Z -> Z) x y z:
   x =? y -> f z x =? f z y.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr2 (f:Z -> Z -> Z) x y z:
   x = y -> f z x = f z y.
-Proof using. intro p. verit p. Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr3_bool (P:Z -> Z -> bool) x y z:
   x =? y -> P z x -> P z y.
-Proof using. intros eqxy pzx. verit (eqxy, pzx). Qed.
+Proof using. verit. Qed.
 
 Lemma lcongr3 (P:Z -> Z -> bool) x y z:
   x = y -> P z x -> P z y.
-Proof using. intros eqxy pzx. verit (eqxy, pzx). Qed.
+Proof using. verit. Qed.
 
 Lemma test20_bool :  forall x, (forall a, a <? x) -> 0 <=? x = false.
-Proof using. intros x H. verit H. Qed.
+Proof using. verit. Qed.
 
 Lemma test20 :  forall x, (forall a, a < x) -> ~ (0 <= x).
-Proof using. intros x H. verit H. Qed.
+Proof using. verit. Qed.
 
 Lemma test21_bool : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
-Proof using. intros x H. verit H. Qed.
+Proof using. verit. Qed.
 
 Lemma test21 : forall x, (forall a, ~ (x <= a)) -> ~ (0 <= x).
-Proof using. intros x H. verit H. Qed.
+Proof using. verit. Qed.
 
 Lemma un_menteur_bool (a b c d : Z) dit:
   dit a =? c ->
@@ -673,7 +671,7 @@ Lemma un_menteur_bool (a b c d : Z) dit:
   (a =? c) || (a =? d) ->
   (b =? c) || (b =? d) ->
   a =? d.
-Proof using. intros H1 H2 H3 H4 H5. verit (H1, H2, H3, H4, H5). Qed.
+Proof using. verit. Qed.
 
 Lemma un_menteur (a b c d : Z) dit:
   dit a = c ->
@@ -682,19 +680,19 @@ Lemma un_menteur (a b c d : Z) dit:
   (a = c) \/ (a = d) ->
   (b = c) \/ (b = d) ->
   a = d.
-Proof using. intros H1 H2 H3 H4 H5. verit (H1, H2, H3, H4, H5). Qed.
+Proof using. verit. Qed.
 
 Lemma const_fun_is_eq_val_0_bool :
   forall f : Z -> Z,
     (forall a b, f a =? f b) ->
     forall x, f x =? f 0.
-Proof using. intros f Hf. verit Hf. Qed.
+Proof using. verit. 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 using. intros f Hf. verit Hf. Qed.
+Proof using. verit. Qed.
 
 (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 ..
    Hn to the environment. You should use <Clear_lemmas> when you do not
@@ -899,15 +897,15 @@ Section GroupZ.
 
   Lemma unique_identity_Z e':
     (forall z, op e' z =? z) -> e' =? e.
-  Proof using associative identity inverse. intros pe'. verit pe'. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Lemma simplification_right_Z x1 x2 y:
       op x1 y =? op x2 y -> x1 =? x2.
-  Proof using associative identity inverse. intro H. verit H. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Lemma simplification_left_Z x1 x2 y:
       op y x1 =? op y x2 -> x1 =? x2.
-  Proof using associative identity inverse. intro H. verit H. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Clear_lemmas.
 End GroupZ.
@@ -932,15 +930,15 @@ Section GroupBool.
 
   Lemma unique_identity_bool e':
     (forall z, op e' z ==? z) -> e' ==? e.
-  Proof using associative identity inverse. intros pe'. verit pe'. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Lemma simplification_right_bool x1 x2 y:
       op x1 y ==? op x2 y -> x1 ==? x2.
-  Proof using associative identity inverse. intro H. verit H. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Lemma simplification_left_bool x1 x2 y:
       op y x1 ==? op y x2 -> x1 ==? x2.
-  Proof using associative identity inverse. intro H. verit H. Qed.
+  Proof using associative identity inverse. verit. Qed.
 
   Clear_lemmas.
 End GroupBool.
@@ -972,15 +970,13 @@ Section Group.
   Lemma simplification_right x1 x2 y:
       op x1 y = op x2 y -> x1 = x2.
   Proof using associative identity inverse HG.
-    intro H.
-    verit (associative, identity, inverse, H).
+    verit (associative, identity, inverse).
   Qed.
 
   Lemma simplification_left x1 x2 y:
       op y x1 = op y x2 -> x1 = x2.
   Proof using associative identity inverse HG.
-    intro H.
-    verit (associative, identity, inverse, H).
+    verit (associative, identity, inverse).
   Qed.
 
   Clear_lemmas.
@@ -1144,14 +1140,12 @@ Qed.
 
 Goal forall (x : positive), Zpos x <=? Zpos x.
 Proof using.
-  intros.
   verit.
 Qed.
 
 
 Goal forall (x : positive) (a : Z), (Z.eqb a a) || negb (Zpos x <? Zpos x).
 Proof using.
-  intros.
   verit.
 Qed.