Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

4 files changed, 190 insertions, 28 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 3d4dee3..bbcff4a 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 3933856..1c0016c 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 with smtcoq_core.
 
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 51e99ae..a5a95ea 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -451,7 +451,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]).