Merge remote-tracking branch 'origin/master' into coq-8.10

2 files changed, 67 insertions, 101 deletions

diff --git a/src/QInst.v b/src/QInst.v
index b2dd836..8a8890b 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -27,7 +27,6 @@ Proof.
    installed when we compile SMTCoq. *)
 Qed.
 
-Hint Resolve impl_split : smtcoq_core.
 
 (** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
    or into a <or (not b) c> when instantiating such a quantified theorem *)
@@ -90,86 +89,30 @@ 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. apply eqb_sym2. 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 *)
+(* Strategy: change or not the order of each equality
+   Complete but exponential in some cases *)
 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 :=
-  repeat match T with
-         | context [ (?A =? ?B)%Z] =>
-           change (A =? B)%Z with (hidden_eq_Z A B) in T
-         end;
-  repeat match T with
-         | context [ @eqb_of_compdec ?A ?HA ?a ?b ] =>
-           change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in T
-         end;
-  repeat match T with
-         | context [ hidden_eq_Z ?A ?B] =>
-           replace (hidden_eq_Z A B) with (B =? A)%Z in T;
-           [ | now rewrite Z.eqb_sym]
-         end;
-  repeat match T with
-         | context [ hidden_eq_U ?A ?HA ?a ?b] =>
-           replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a) in T;
-           [ | now rewrite eqb_of_compdec_sym]
-         end.
-Ltac apply_sym_goal :=
-  repeat match goal with
-         | [ |- context [ (?A =? ?B)%Z] ] =>
-           change (A =? B)%Z with (hidden_eq_Z A B)
-         end;
-  repeat match goal with
-         | [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] =>
-           change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b)
-         end;
-  repeat match goal with
-         | [ |- context [ hidden_eq_Z ?A ?B] ] =>
-           replace (hidden_eq_Z A B) with (B =? A)%Z;
-           [ | now rewrite Z.eqb_sym]
-         end;
-  repeat match goal with
-         | [ |- context [ hidden_eq_U ?A ?HA ?a ?b] ] =>
-           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
+Ltac apply_sym_hyp H :=
+  let TH := type of H in
+  lazymatch TH with
+  | context [ (?A =? ?B)%Z ] =>
+    first [ change (A =? B)%Z with (hidden_eq_Z A B) in H; apply_sym_hyp H
+          | replace (A =? B)%Z with (hidden_eq_Z B A) in H; [apply_sym_hyp H | now rewrite Z.eqb_sym] ]
+  | context [ @eqb_of_compdec ?A ?HA ?a ?b ] =>
+    first [ change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in H; apply_sym_hyp H
+          | replace (eqb_of_compdec HA a b) with (hidden_eq_U A HA b a) in H; [apply_sym_hyp H | now rewrite eqb_of_compdec_sym] ]
+  | _ => apply H
   end.
-Ltac strategy2 H :=
-  match goal with
-  | [ |- ?g ] =>
-    let TH := type of H in
-    order_equalities g TH;
-    apply H
+Ltac apply_sym H :=
+  lazymatch goal with
+  | [ |- context [ (?A =? ?B)%Z ] ] =>
+    first [ change (A =? B)%Z with (hidden_eq_Z A B); apply_sym H
+          | replace (A =? B)%Z with (hidden_eq_Z B A); [apply_sym H | now rewrite Z.eqb_sym] ]
+  | [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] =>
+    first [ change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b); apply_sym H
+          | replace (eqb_of_compdec HA a b) with (hidden_eq_U A HA b a); [apply_sym H | now rewrite eqb_of_compdec_sym] ]
+  | _ => apply_sym_hyp H
   end.
 
 
@@ -178,33 +121,19 @@ Ltac vauto :=
   try (unfold is_true;
        let H := fresh "H" in
        intro H;
-       first [ strategy1 H
-             | strategy2 H
+       first [ apply_sym 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 ]
-                       | eapply eqb_sym_or_split_right;
-                         first [ strategy1 H
-                               | strategy2 H ]
-                       | eapply eqb_sym_or_split_left;
-                         first [ strategy1 H
-                               | strategy2 H ]
-                       | eapply eqb_or_split_right;
-                         first [ strategy1 H
-                               | strategy2 H ]
-                       | eapply eqb_or_split_left;
-                         first [ strategy1 H
-                               | strategy2 H ]
+                 first [ eapply impl_split; apply_sym H
+                       | eapply impl_or_split_right; apply_sym H
+                       | eapply impl_or_split_left; apply_sym H
+                       | eapply eqb_sym_or_split_right; apply_sym H
+                       | eapply eqb_sym_or_split_left; apply_sym H
+                       | eapply eqb_or_split_right; apply_sym H
+                       | eapply eqb_or_split_left; apply_sym H
                        ]
                | [ |- (negb ?A || ?B || ?C) = true ] =>
-                 eapply eqb_or_split;
-                 first [ strategy1 H
-                       | strategy2 H ]
+                 eapply eqb_or_split; apply_sym H
                end
              ]
       );
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 34b5dfd..2bdc520 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1369,3 +1369,40 @@ Section PropToBool.
   Goal (forall (x x0 : bool) (x1 x2 : list bool), x :: x1 = x0 :: x2 -> x = x0) -> true.
   Proof. verit. Qed.
 End PropToBool.
+
+
+Section EqSym.
+  Variable A : Type.
+  Variable HA : CompDec A.
+  Variable H8 : forall (h : list A) (l : list (list A)), tl (h :: l) = l.
+  Variable H12_A : forall (h : A) (l : list A), tl (h :: l) = l.
+  Variable H9 : forall (h : option A) (l : list (option A)), tl (h :: l) = l.
+  Variable H12 : @tl (list A) nil = nil.
+  Variable H13_A : @tl A nil = nil.
+  Variable H14 : @tl (option A) nil = nil.
+  Variable H13 : forall (h : list A) (l : list (list A)), hd_error (h :: l) = Some h.
+  Variable H10_A : forall (h : A) (l : list A), hd_error (h :: l) = Some h.
+  Variable H15 : forall (h : option A) (l : list (option A)), hd_error (h :: l) = Some h.
+  Variable H10 : @hd_error (list A) nil = None.
+  Variable H11_A : @hd_error A nil = None.
+  Variable H16 : @hd_error (option A) nil = None.
+  Variable H11 : forall x : list A, Some x = None -> False.
+  Variable H7_A : forall x : A, Some x = None -> False.
+  Variable H17 : forall x : option A, Some x = None -> False.
+  Variable H7 : forall x x0 : list A, Some x = Some x0 -> x = x0.
+  Variable H6_A : forall x x0 : A, Some x = Some x0 -> x = x0.
+  Variable H18 : forall x x0 : option A, Some x = Some x0 -> x = x0.
+  Variable H4 : forall (x : list A) (x0 : list (list A)), nil = x :: x0 -> False.
+  Variable H3_A : forall (x : A) (x0 : list A), nil = x :: x0 -> False.
+  Variable H5 : forall (x : option A) (x0 : list (option A)), nil = x :: x0 -> False.
+  Variable H3 : forall (x x0 : list A) (x1 x2 : list (list A)), x :: x1 = x0 :: x2 -> x = x0.
+  Variable H2_A : forall (x x0 : A) (x1 x2 : list A), x :: x1 = x0 :: x2 -> x = x0.
+  Variable H6 : forall (x x0 : option A) (x1 x2 : list (option A)), x :: x1 = x0 :: x2 -> x = x0.
+  Variable x : A.
+  Variable xs : list A.
+  Variable a : A.
+  Variable r : list A.
+
+  Goal hd_error (x :: xs) = Some a /\ tl (x :: xs) = r <-> x :: xs = a :: r.
+  Proof. verit. Qed.
+End EqSym.