Do not add CompDec on the fly

3 files changed, 386 insertions, 272 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index fcfe671..003e4cb 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -16,11 +16,159 @@ Require Import
 Import BVList.BITVECTOR_LIST.
 
 
+(* List of interpreted types *)
+
+Ltac is_interpreted_type T :=
+  lazymatch T with
+  | BVList.BITVECTOR_LIST.bitvector _ => constr:(true)
+  | FArray.farray _ _ => constr:(true)
+  | Z => constr:(true)
+  | bool => constr:(true)
+  | _ => constr:(false)
+  end.
+
+
+(* Add CompDec for types over which an equality appears in the goal or
+   in a local hypothesis *)
+
+Ltac add_compdecs_term u :=
+  match u with
+  | context C [@Logic.eq ?t _ _] =>
+    let u' := context C [True] in
+    lazymatch is_interpreted_type t with
+    | true =>
+      (* For interpreted types, we need a specific Boolean equality *)
+      add_compdecs_term u'
+    | false =>
+      (* For uninterpreted types, we use CompDec *)
+      lazymatch goal with
+      (* If it is already in the local context, do nothing *)
+      | _ : SMT_classes.CompDec t |- _ => add_compdecs_term u'
+      (* Otherwise, add it in the local context *)
+      | _ =>
+        let p := fresh "p" in
+        assert (p:SMT_classes.CompDec t);
+        [ try (exact _)       (* Use the typeclass machinery *)
+        | add_compdecs_term u' ]
+      end
+    end
+  | _ => idtac
+  end.
+
+Ltac add_compdecs_names Hs :=
+  match Hs with
+  | (?Hs1, ?Hs2) => add_compdecs_names Hs1; [ .. |  add_compdecs_names Hs2 ]
+  | ?H => let t := type of H in add_compdecs_term t
+  end.
+
+(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *)
+(*     3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *)
+(*     17%positive = 42%positive /\ (5,6) = (6,7). *)
+(* Proof. *)
+(*   intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *)
+(*   destruct H as [H1 H2]. *)
+(*   add_compdecs_names (H1, H2). *)
+(*   Show 3. *)
+(* Abort. *)
+
+(* (* It is sensitive to the order of the equalities... *) *)
+(* Goal forall (A:Type) (a:A) (l:list A), a = a -> l = l -> True. *)
+(* Proof. *)
+(*   intros A a l H1 H2. *)
+(*   add_compdecs_names (H1, H2). *)
+
+(* Abort. *)
+(* Goal forall (A:Type) (a:A) (l:list A), l = l -> a = a -> True. *)
+(* Proof. *)
+(*   intros A a l H1 H2. *)
+(*   add_compdecs_names (H1, H2). *)
+(* Abort. *)
+
+
+Ltac add_compdecs_names_and_goal Hs :=
+  lazymatch Hs with
+  | Some ?Hs => add_compdecs_names Hs
+  | None => idtac
+  end;
+  [ .. | match goal with
+         | |- ?g => add_compdecs_term g
+         end ].
+
+(* Goal forall (A B C:Type) (HA:SMT_classes.CompDec A) (a1 a2:A) (b1 b2 b3 b4:B) (c1 c2:C), *)
+(*     3%Z = 4%Z /\ a1 = a2 /\ b1 = b2 /\ b3 = b4 /\ 5%nat = 6%nat /\ c1 = c2 -> *)
+(*     17%positive = 42%positive /\ (5,6) = (6,7). *)
+(* Proof. *)
+(*   intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *)
+(*   add_compdecs_names_and_goal (Some H). *)
+(*   Show 3. *)
+(* Abort. *)
+
+
+Tactic Notation "add_compdecs" constr(h) := add_compdecs_names_and_goal (Some h).
+Tactic Notation "add_compdecs"           := add_compdecs_names_and_goal (@None nat).
+
+
+(* Auxiliary lemma *)
+
 Lemma geb_ge (n m : Z) : (n >=? m)%Z = true <-> (n >= m)%Z.
 Proof.
   now rewrite Z.geb_le, Z.ge_le_iff.
 Qed.
 
+
+(* Conversion from bool to Prop *)
+
+Ltac bool2prop_true :=
+  repeat
+    match goal with
+    | [ |- forall _ : ?t, _ ] =>
+      lazymatch type of t with
+      | Prop => fail
+      | _ => intro
+      end
+
+    | [ |- context[ bv_ult _ _ = true ] ] => rewrite bv_ult_B2P
+    | [ |- context[ bv_slt _ _ = true ] ] => rewrite bv_slt_B2P
+    | [ |- context[ Z.ltb _ _ = true ] ] => rewrite Z.ltb_lt
+    | [ |- context[ Z.gtb _ _ ] ] => rewrite <- Zgt_is_gt_bool
+    | [ |- context[ Z.leb _ _ = true ] ] => rewrite Z.leb_le
+    | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge
+    | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq
+
+    |  [ |- context[ Bool.eqb _ _ = true ] ] => rewrite eqb_true_iff
+
+    | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p)
+
+    | [ |- context[ ?G0 || ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1));
+      [ | apply orP]
+
+    | [ |- context[ implb ?G0 ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1));
+      [ | apply implyP]
+
+    | [ |- context[?G0 && ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1));
+      [ | apply andP]
+
+    | [ |- context[Bool.eqb ?G0 ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1));
+      [ | apply iffP]
+
+    | [ |- context[ negb ?G = true ] ] =>
+      rewrite <- (@reflect_iff (~ G = true) (negb G));
+      [ | apply negP]
+
+    | [ |- context[ true = true ] ] => rewrite TrueB
+
+    | [ |- context[ false = true ] ] => rewrite FalseB
+    end.
+
+Ltac bool2prop := unfold is_true; bool2prop_true.
+
+
+(* Conversion from Prop to bool, all CompDecs being in the context *)
+
 Ltac prop2bool :=
   repeat
     match goal with
@@ -56,12 +204,6 @@ Ltac prop2bool :=
         lazymatch goal with
         | [ p: (CompDec t) |- _ ] =>
           rewrite (@compdec_eq_eqb _ p)
-        | _ =>
-          let p := fresh "p" in
-          assert (p:CompDec t);
-          [ try (exact _)       (* Use the typeclass machinery *)
-          | rewrite (@compdec_eq_eqb _ p)
-          ]
         end
       end
 
@@ -94,123 +236,45 @@ Ltac prop2bool :=
     end.
 
 
-Ltac bool2prop_true :=
-  repeat
-    match goal with
-    | [ |- forall _ : ?t, _ ] =>
-      lazymatch type of t with
-      | Prop => fail
-      | _ => intro
-      end
-
-    | [ |- context[ bv_ult _ _ = true ] ] => rewrite bv_ult_B2P
-    | [ |- context[ bv_slt _ _ = true ] ] => rewrite bv_slt_B2P
-    | [ |- context[ Z.ltb _ _ = true ] ] => rewrite Z.ltb_lt
-    | [ |- context[ Z.gtb _ _ ] ] => rewrite <- Zgt_is_gt_bool
-    | [ |- context[ Z.leb _ _ = true ] ] => rewrite Z.leb_le
-    | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge
-    | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq
-
-    |  [ |- context[ Bool.eqb _ _ = true ] ] => rewrite eqb_true_iff
-
-    | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p)
-
-    | [ |- context[ ?G0 || ?G1 = true ] ] =>
-      rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1));
-      [ | apply orP]
-
-    | [ |- context[ implb ?G0 ?G1 = true ] ] =>
-      rewrite <- (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1));
-      [ | apply implyP]
-
-    | [ |- context[?G0 && ?G1 = true ] ] =>
-      rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1));
-      [ | apply andP]
-
-    | [ |- context[Bool.eqb ?G0 ?G1 = true ] ] =>
-      rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1));
-      [ | apply iffP]
-
-    | [ |- context[ negb ?G = true ] ] =>
-      rewrite <- (@reflect_iff (~ G = true) (negb G));
-      [ | apply negP]
-
-    | [ |- context[ true = true ] ] => rewrite TrueB
-
-    | [ |- context[ false = true ] ] => rewrite FalseB
-    end.
-
-Ltac bool2prop := unfold is_true; bool2prop_true.
-
-
 Ltac prop2bool_hyp H :=
   let TH := type of H in
 
-  (* Add a CompDec hypothesis if needed *)
-  let prop2bool_t := fresh "prop2bool_t" in epose (prop2bool_t := ?[prop2bool_t_evar] : Type);
-  let prop2bool_comp := fresh "prop2bool_comp" in epose (prop2bool_comp := ?[prop2bool_comp_evar] : bool);
-  let H' := fresh in
+  (* Compute the bool version of the lemma *)
+  let prop2bool_Hbool := fresh "prop2bool_Hbool" in epose (prop2bool_Hbool := ?[prop2bool_Hbool_evar] : Prop);
   assert (H':False -> TH);
   [ let HFalse := fresh "HFalse" in intro HFalse;
-    repeat match goal with
-           | [ |- forall _ : ?t, _ ] =>
-             lazymatch type of t with
-             | Prop => fail
-             | _ => intro
-             end
-           | [ |- context[@Logic.eq ?A _ _] ] => instantiate (prop2bool_t_evar := A); instantiate (prop2bool_comp_evar := true)
-           | _ => instantiate (prop2bool_t_evar := nat); instantiate (prop2bool_comp_evar := false)
-           end;
+    let rec tac_rec :=
+        match goal with
+        | [ |- forall _ : ?t, _ ] =>
+          lazymatch type of t with
+          | Prop => fail
+          | _ =>
+            let H := fresh in
+            intro H; tac_rec; revert H
+          end
+        | _ => prop2bool
+        end in
+    tac_rec;
+    lazymatch goal with
+    | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
+    end;
     destruct HFalse
   | ];
   clear H';
-  lazymatch (eval compute in prop2bool_comp) with
-  | true =>
-    let A := eval cbv in prop2bool_t in
-    lazymatch goal with
-    | [ _ : CompDec A |- _ ] => idtac
-    | _ =>
-      let Hcompdec := fresh "Hcompdec" in
-      assert (Hcompdec: CompDec A);
-      [ try (exact _) | ]
-    end
-  | false => idtac
-  end;
-  clear prop2bool_t; clear prop2bool_comp;
-
-  (* Compute the bool version of the lemma *)
-  [ .. |
-    let prop2bool_Hbool := fresh "prop2bool_Hbool" in epose (prop2bool_Hbool := ?[prop2bool_Hbool_evar] : Prop);
-    assert (H':False -> TH);
-    [ let HFalse := fresh "HFalse" in intro HFalse;
-      let rec tac_rec :=
-          match goal with
-          | [ |- forall _ : ?t, _ ] =>
-            lazymatch type of t with
-            | Prop => fail
-            | _ =>
-              let H := fresh in
-              intro H; tac_rec; revert H
-            end
-          | _ => prop2bool
-          end in
-      tac_rec;
-      lazymatch goal with
-      | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
-      end;
-      destruct HFalse
-    | ];
-    clear H';
 
-    (* Assert and prove the bool version of the lemma *)
-    assert (H':prop2bool_Hbool); subst prop2bool_Hbool;
-    [ bool2prop; apply H | ];
+  (* Assert and prove the bool version of the lemma *)
+  assert (H':prop2bool_Hbool); subst prop2bool_Hbool;
+  [ bool2prop; apply H | ];
 
-    (* Replace the Prop version with the bool version *)
-    try clear H; let H := fresh H in assert (H:=H'); clear H'
-  ].
+  (* Replace the Prop version with the bool version *)
+  try clear H; let H := fresh H in assert (H:=H'); clear H'.
 
 
+(* Change hypotheses of the form
+   [CompDec A1 -> ... -> CompDec An -> P]
+   into
+   [P]
+ *)
 Ltac remove_compdec_hyp H :=
   let TH := type of H in
   lazymatch TH with
@@ -239,6 +303,11 @@ Ltac prop2bool_hyps Hs :=
   end.
 
 
+(* Notations *)
+
+Infix "--->" := implb (at level 60, right associativity) : bool_scope.
+Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
+
 
 (* Section Test. *)
 (*   Variable A : Type. *)
@@ -250,113 +319,113 @@ Ltac prop2bool_hyps Hs :=
 
 (*   Goal True. *)
 (*   Proof. *)
+(*     add_compdecs. *)
+(*     admit. *)
 (*     prop2bool_hyp basic. *)
 (*     prop2bool_hyp no_eq. *)
 (*     prop2bool_hyp uninterpreted_type. *)
-(*     admit. *)
 (*     prop2bool_hyp bool_eq. *)
 (*     prop2bool_hyp plus_n_O. *)
 (*   Abort. *)
 
 (*   Goal True. *)
 (*   Proof. *)
-(*     prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n). *)
+(*     add_compdecs. *)
 (*     admit. *)
+(*     prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n). *)
 (*   Abort. *)
 (* End Test. *)
 
-Section Group.
-
-  Variable G : Type.
-  Variable HG : CompDec G.
-  Variable op : G -> G -> G.
-  Variable inv : G -> G.
-  Variable e : G.
 
-  Hypothesis associative :
-    forall a b c : G, op a (op b c) = op (op a b) c.
-  Hypothesis identity :
-    forall a : G, (op e a = a) /\ (op a e = a).
-  Hypothesis inverse :
-    forall a : G, (op a (inv a) = e) /\ (op (inv a) a = e).
+(* Section Group. *)
 
-  Variable e' : G.
-  Hypothesis other_id : forall e' z, op e' z = z.
+(*   Variable G : Type. *)
+(*   Variable HG : CompDec G. *)
+(*   Variable op : G -> G -> G. *)
+(*   Variable inv : G -> G. *)
+(*   Variable e : G. *)
 
-  Goal True.
-  Proof.
-    prop2bool_hyp associative.
-    prop2bool_hyp identity.
-    prop2bool_hyp inverse.
-    prop2bool_hyp other_id.
-    exact I.
-  Qed.
+(*   Hypothesis associative : *)
+(*     forall a b c : G, op a (op b c) = op (op a b) c. *)
+(*   Hypothesis identity : *)
+(*     forall a : G, (op e a = a) /\ (op a e = a). *)
+(*   Hypothesis inverse : *)
+(*     forall a : G, (op a (inv a) = e) /\ (op (inv a) a = e). *)
 
-  Goal True.
-  Proof.
-    prop2bool_hyps (associative, identity, inverse, other_id).
-    exact I.
-  Qed.
+(*   Variable e' : G. *)
+(*   Hypothesis other_id : forall e' z, op e' z = z. *)
 
-End Group.
-
-
-Section MultipleCompDec.
-
-  Variables A B : Type.
-  Hypothesis multiple : forall (a1 a2:A) (b1 b2:B), a1 = a2 -> b1 = b2.
-
-  Goal True.
-  Proof.
-    Fail prop2bool_hyp multiple.
-  Abort.
+(*   Goal True. *)
+(*   Proof. *)
+(*     add_compdecs. *)
+(*     prop2bool_hyp associative. *)
+(*     prop2bool_hyp identity. *)
+(*     prop2bool_hyp inverse. *)
+(*     prop2bool_hyp other_id. *)
+(*     exact I. *)
+(*   Qed. *)
 
-End MultipleCompDec.
+(*   Goal True. *)
+(*   Proof. *)
+(*     add_compdecs. *)
+(*     prop2bool_hyps (associative, identity, inverse, other_id). *)
+(*     exact I. *)
+(*   Qed. *)
 
+(* End Group. *)
 
-(* We can assume that we deal only with monomorphic hypotheses, since
-   polymorphism will be removed before *)
-Section Poly.
-  Hypothesis basic : forall (A:Type) (l1 l2:list A),
-    length (l1++l2) = (length l1 + length l2)%nat.
-  Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
 
-  Goal True.
-  Proof.
-    prop2bool_hyp basic.
-    Fail prop2bool_hyp uninterpreted_type.
-  Abort.
+(* Section MultipleCompDec. *)
 
-End Poly.
+(*   Variables A B : Type. *)
+(*   Hypothesis multiple : forall (a1 a2:A) (b1 b2:B), a1 = a2 -> b1 = b2. *)
 
+(*   Goal True. *)
+(*   Proof. *)
+(*     add_compdecs. *)
+(*     admit. admit. *)
+(*     prop2bool_hyp multiple. *)
+(*   Abort. *)
 
+(* End MultipleCompDec. *)
 
 
+(* (* We can assume that we deal only with monomorphic hypotheses, since *)
+(*    polymorphism will be removed before *) *)
+(* Section Poly. *)
+(*   Hypothesis basic : forall (A:Type) (l1 l2:list A), *)
+(*     length (l1++l2) = (length l1 + length l2)%nat. *)
+(*   Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a. *)
 
-Infix "--->" := implb (at level 60, right associativity) : bool_scope.
-Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
+(*   Goal True. *)
+(*   Proof. *)
+(*     add_compdecs. *)
+(*     prop2bool_hyp basic. *)
+(*     prop2bool_hyp uninterpreted_type. *)
+(*   Abort. *)
 
+(* End Poly. *)
 
 
-(* Does not fail since 8.10 *)
+(* (* Does not fail since 8.10 *) *)
 
-Goal True.
-  evar (t:Type).
-  assert (H:True).
-  - instantiate (t:=nat). exact I.
-  - exact I.
-Qed.
+(* Goal True. *)
+(*   evar (t:Type). *)
+(*   assert (H:True). *)
+(*   - instantiate (t:=nat). exact I. *)
+(*   - exact I. *)
+(* Qed. *)
 
-Goal True.
-  evar (t:option Set).
-  assert (H:True).
-  - instantiate (t:=Some nat). exact I.
-  - exact I.
-Qed.
+(* Goal True. *)
+(*   evar (t:option Set). *)
+(*   assert (H:True). *)
+(*   - instantiate (t:=Some nat). exact I. *)
+(*   - exact I. *)
+(* Qed. *)
 
-Goal True.
-  evar (t:option Type).
-  assert (H:True).
-  - Fail instantiate (t:=Some nat). exact I.
-  - exact I.
-Abort.
+(* Goal True. *)
+(*   evar (t:option Type). *)
+(*   assert (H:True). *)
+(*   - Fail instantiate (t:=Some nat). exact I. *)
+(*   - exact I. *)
+(* Abort. *)
diff --git a/src/Tactics.v b/src/Tactics.v
index 6f2c7b1..d6c772c 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -125,108 +125,134 @@ Tactic Notation "verit_bool_no_check_timeout"   int_or_var(timeout)        :=
 
 (** Tactics in Prop **)
 
-Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
-Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
+Ltac zchaff          := add_compdecs; [ .. | prop2bool; zchaff_bool; bool2prop ].
+Ltac zchaff_no_check := add_compdecs; [ .. | prop2bool; zchaff_bool_no_check; bool2prop].
 
 Tactic Notation "verit" constr(h) :=
-  prop2bool;
-  [ .. | prop2bool_hyps h;
-         [ .. | let Hs := get_hyps in
-                match Hs with
-                | Some ?Hs =>
-                  prop2bool_hyps Hs;
-                  [ .. | verit_bool_base_auto (Some (h, Hs)) ]
-                | None => verit_bool_base_auto (Some h)
-                end; vauto
-         ]
+  intros;
+  let Hs := get_hyps in
+  let Hs :=
+    lazymatch Hs with
+    | Some ?Hs => constr:(Some (h, Hs))
+    | None => constr:(Some h)
+    end
+  in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_base_auto Hs; vauto ]
   ].
 Tactic Notation "verit"           :=
-  prop2bool;
-  [ .. | let Hs := get_hyps in
-         match Hs with
-         | Some ?Hs =>
-           prop2bool_hyps Hs;
-           [ .. | verit_bool_base_auto (Some Hs) ]
-         | None => verit_bool_base_auto (@None nat)
-         end; vauto
+  intros;
+  let Hs := get_hyps in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_base_auto Hs; vauto ]
   ].
 Tactic Notation "verit_no_check" constr(h) :=
-  prop2bool;
-  [ .. | prop2bool_hyps h;
-         [ .. | let Hs := get_hyps in
-                match Hs with
-                | Some ?Hs =>
-                  prop2bool_hyps Hs;
-                  [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ]
-                | None => verit_bool_no_check_base_auto (Some h)
-                end; vauto
-         ]
+  intros;
+  let Hs := get_hyps in
+  let Hs :=
+    lazymatch Hs with
+    | Some ?Hs => constr:(Some (h, Hs))
+    | None => constr:(Some h)
+    end
+  in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_no_check_base_auto Hs; vauto ]
   ].
 Tactic Notation "verit_no_check"           :=
-  prop2bool;
-  [ .. | let Hs := get_hyps in
-         match Hs with
-         | Some ?Hs =>
-           prop2bool_hyps Hs;
-           [ .. | verit_bool_no_check_base_auto (Some Hs) ]
-         | None => verit_bool_no_check_base_auto (@None nat)
-         end; vauto
+  intros;
+  let Hs := get_hyps in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_no_check_base_auto Hs; vauto ]
   ].
 
 Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=
-  prop2bool;
-  [ .. | prop2bool_hyps h;
-         [ .. | let Hs := get_hyps in
-                match Hs with
-                | Some ?Hs =>
-                    prop2bool_hyps Hs;
-                    [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout ]
-                | None => verit_bool_base_auto_timeout (Some h) timeout
-                end; vauto
-         ]
+  intros;
+  let Hs := get_hyps in
+  let Hs :=
+    lazymatch Hs with
+    | Some ?Hs => constr:(Some (h, Hs))
+    | None => constr:(Some h)
+    end
+  in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_base_auto_timeout Hs timeout; vauto ]
   ].
-Tactic Notation "verit_timeout"   int_or_var(timeout)        :=
-  prop2bool;
-  [ .. | let Hs := get_hyps in
-         match Hs with
-         | Some ?Hs =>
-             prop2bool_hyps Hs;
-             [ .. | verit_bool_base_auto_timeout (Some Hs) timeout ]
-         | None => verit_bool_base_auto_timeout (@None nat) timeout
-         end; vauto
+Tactic Notation "verit_timeout"           int_or_var(timeout) :=
+  intros;
+  let Hs := get_hyps in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_base_auto_timeout Hs timeout; vauto ]
   ].
 Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) :=
-  prop2bool;
-  [ .. | prop2bool_hyps h;
-         [ .. | let Hs := get_hyps in
-                match Hs with
-                | Some ?Hs =>
-                    prop2bool_hyps Hs;
-                    [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
-                | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
-                end; vauto
-         ]
+  intros;
+  let Hs := get_hyps in
+  let Hs :=
+    lazymatch Hs with
+    | Some ?Hs => constr:(Some (h, Hs))
+    | None => constr:(Some h)
+    end
+  in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_no_check_base_auto_timeout Hs timeout; vauto ]
   ].
-Tactic Notation "verit_no_check_timeout"   int_or_var(timeout)        :=
-  prop2bool;
-  [ .. | let Hs := get_hyps in
-         match Hs with
-         | Some ?Hs =>
-             prop2bool_hyps Hs;
-             [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout ]
-         | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
-         end; vauto
+Tactic Notation "verit_no_check_timeout"           int_or_var(timeout) :=
+  intros;
+  let Hs := get_hyps in
+  add_compdecs Hs;
+  [ .. | prop2bool;
+         lazymatch Hs with
+         | Some ?Hs => prop2bool_hyps Hs
+         | None => idtac
+         end;
+         [ .. | verit_bool_no_check_base_auto_timeout Hs timeout; vauto ]
   ].
 
-
-Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
-Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_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]).
-
+Ltac cvc4            := add_compdecs; [ .. | prop2bool; cvc4_bool; bool2prop ].
+Ltac cvc4_no_check   := add_compdecs; [ .. | prop2bool; cvc4_bool_no_check; bool2prop ].
+
+Tactic Notation "smt" constr(h) :=
+  add_compdecs; [ .. | prop2bool; try verit h; cvc4_bool; try verit h; bool2prop ].
+Tactic Notation "smt"           :=
+  add_compdecs; [ .. | prop2bool; try verit  ; cvc4_bool; try verit  ; bool2prop ].
+Tactic Notation "smt_no_check" constr(h) :=
+  add_compdecs; [ .. | prop2bool; try verit_no_check h; cvc4_bool_no_check; try verit_no_check h; bool2prop].
+Tactic Notation "smt_no_check"           :=
+  add_compdecs; [ .. | prop2bool; try verit_no_check  ; cvc4_bool_no_check; try verit_no_check  ; bool2prop].
 
 
 (* 
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 4285f96..5164308 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1562,3 +1562,22 @@ Section TimeoutProp.
     verit_no_check_timeout 10.
   Qed.
 End TimeoutProp.
+
+
+(* Test CompDec open goals *)
+
+Section OpenCompdec.
+
+  Variable A : Type.
+  Variable l : list A.
+  Variable x : A.
+  Variable H1 : hd_error l = Some x.
+  Variable H2 : hd_error (@nil A) = None.
+  Variable H3 : forall x : A, Some x = None -> False.
+  Variable Hpb : forall x x0 : A, Some x = Some x0 -> x = x0.
+
+  Goal l <> nil.
+  Proof. verit. Abort.
+  (* Should leave open CompDec goals but not fail *)
+
+End OpenCompdec.