From 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Wed, 21 Apr 2021 09:46:30 +0200
Subject: Convert hypotheses from Prop to bool (#89)

* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed.

* Some current limitations are detailed in src/PropToBool.v.

* Partially enhances #30 .
---
 examples/Example.v                          |  15 +-
 src/BoolToProp.v                            |  74 --------
 src/PropToBool.v                            | 250 +++++++++++++++++++++++++++-
 src/SMTCoq.v                                |   2 +-
 src/classes/SMT_classes_instances.v         |   1 +
 src/trace/coqTerms.ml                       |  25 ++-
 src/trace/coqTerms.mli                      |   4 +
 src/trace/smtMisc.ml                        |   2 +-
 src/verit/verit.ml                          |  10 ++
 src/verit/verit.mli                         |   4 +-
 src/versions/standard/Tactics_standard.v    |  40 ++---
 src/versions/standard/_CoqProject           |   1 -
 src/versions/standard/g_smtcoq_standard.ml4 |   4 +-
 unit-tests/Tests_lfsc_tactics.v             |   4 +-
 unit-tests/Tests_verit_tactics.v            | 209 ++++++++++++++++++-----
 15 files changed, 484 insertions(+), 161 deletions(-)
 delete mode 100644 src/BoolToProp.v

diff --git a/examples/Example.v b/examples/Example.v
index 628811c..dab31e7 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -375,11 +375,11 @@ Section Group.
 
   Lemma simplification_right x1 x2 y:
       op x1 y ==? op x2 y -> x1 ==? x2.
-  Proof. intro H. smt_no_check H inverse'. Qed.
+  Proof. intro H. smt_no_check (H, 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. intro H. smt_no_check (H, inverse'). Qed.
 
   Clear_lemmas.
 End Group.
@@ -393,7 +393,6 @@ Section CompCert.
 
   Variable block : Set.
   Hypothesis eq_block : CompDec block.
-  Local Notation "a ==? b" := (@eqb_of_compdec block eq_block a b) (at level 60).
 
   Variable mem: Set.
   Hypothesis dec_mem : CompDec mem.
@@ -403,11 +402,11 @@ Section CompCert.
 
   Hypothesis alloc_valid_block_1:
     forall m lo hi b,
-      valid_block (alloc_mem m lo hi) b ---> ((b ==? (alloc_block m lo hi)) || valid_block m b).
+      valid_block (alloc_mem m lo hi) b -> ((b = (alloc_block m lo hi)) \/ valid_block m b).
 
   Hypothesis alloc_valid_block_2:
     forall m lo hi b,
-      ((b ==? (alloc_block m lo hi)) || valid_block m b) ---> valid_block (alloc_mem m lo hi) b.
+      ((b = (alloc_block m lo hi)) \/ valid_block m b) -> (valid_block (alloc_mem m lo hi) b).
 
   Hypothesis alloc_not_valid_block:
     forall m lo hi,
@@ -416,13 +415,13 @@ Section CompCert.
   Lemma alloc_valid_block_inv m lo hi b :
     valid_block m b -> valid_block (alloc_mem m lo hi) b.
   Proof.
-    intro H. verit alloc_valid_block_2 H.
+    intro H. verit (alloc_valid_block_2, H).
   Qed.
 
   Lemma alloc_not_valid_block_2 m lo hi b' :
-    valid_block m b' -> b' ==? (alloc_block m lo hi) = false.
+    valid_block m b' -> b' <> (alloc_block m lo hi).
   Proof.
-    intro H. verit alloc_not_valid_block H.
+    intro H. verit (alloc_not_valid_block, H).
   Qed.
 
 End CompCert.
diff --git a/src/BoolToProp.v b/src/BoolToProp.v
deleted file mode 100644
index 8a3b134..0000000
--- a/src/BoolToProp.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-Require Import
-        Bool ZArith BVList Logic BVList FArray
-        SMT_classes SMT_classes_instances ReflectFacts.
-Import BVList.BITVECTOR_LIST. 
-
-Local Coercion is_true : bool >-> Sortclass.
-
-Infix "--->" := implb (at level 60, right associativity) : bool_scope.
-Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
-
-Ltac bool2prop :=
-  repeat
-    match goal with
-    | [ |- forall _ : bitvector _, _] => intro
-    | [ |- forall _ : farray _ _, _] => intro
-    | [ |- forall _ : _ -> _, _] => intro
-    | [ |- forall _ : Z, _] => intro
-    | [ |- forall _ : bool, _] => intro
-    | [ |- forall _ : Type, _] => intro
-    | [ p: Type |-  context[ forall _ : ?t, _ ] ] => intro
-
-    | [ |- forall t : Type, CompDec t -> _  ] => intro
-    | [ |- CompDec _ -> _  ] => intro
-
-    | [ |- context[ bv_ult _ _ ] ] => unfold is_true; rewrite bv_ult_B2P
-    | [ |- context[ bv_slt _ _ ] ] => unfold is_true; rewrite bv_slt_B2P
-    | [ |- context[ bv_eq _ _ ] ]  => unfold is_true; rewrite bv_eq_reflect
-    | [ |- context[ equal _ _ ] ]  => unfold is_true; rewrite equal_iff_eq
-    | [ |- context[ Z.ltb _ _ ] ]  => unfold is_true; rewrite Z.ltb_lt
-    | [ |- context[ Z.gtb _ _ ] ]  => unfold is_true; rewrite Z.gtb_lt
-    | [ |- context[ Z.leb _ _ ] ]  => unfold is_true; rewrite Z.leb_le
-    | [ |- context[ Z.geb _ _ ] ]  => unfold is_true; rewrite Z.geb_le
-    | [ |- context[ Z.eqb _ _ ] ]  => unfold is_true; rewrite Z.eqb_eq
-
-    | [ |- context[?G0 ---> ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true -> G1 = true)  (G0 ---> G1)); 
-      [ | apply implyP]
-
-    | [ |- context[?G0 || ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1)); 
-      [ | apply orP]
-
-    | [ |- context[?G0 && ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (G0 && G1)); 
-      [ | apply andP]
-
-    | [ |- context[?G0 <---> ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (G0 <---> G1)); 
-      [ | apply iffP]
-
-    | [ |- context[ negb ?G ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G <> true) (negb G)); 
-      [ | apply negP]
-
-    | [R : CompDec ?t |- context[ CompDec ?t  ] ] => exact R
-
-    | [R : EqbType ?t |- context[ EqbType ?t  ] ] => exact R
-
-    | [ |- context[ false = true ] ] => rewrite FalseB
-                                              
-    | [ |- context[ true = true ] ] => rewrite TrueB
-
-    end.
diff --git a/src/PropToBool.v b/src/PropToBool.v
index a9cbded..25662ad 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -13,7 +13,13 @@
 Require Import
         Bool ZArith BVList Logic BVList FArray
         SMT_classes SMT_classes_instances ReflectFacts.
-Import BVList.BITVECTOR_LIST. 
+Import BVList.BITVECTOR_LIST.
+
+
+Lemma geb_ge (n m : Z) : (n >=? m)%Z = true <-> (n >= m)%Z.
+Proof.
+  now rewrite Z.geb_le, Z.ge_le_iff.
+Qed.
 
 Ltac prop2bool :=
   repeat
@@ -27,9 +33,9 @@ Ltac prop2bool :=
     | [ |- context[ bv_ultP _ _ ] ] => rewrite <- bv_ult_B2P
     | [ |- context[ bv_sltP _ _ ] ] => rewrite <- bv_slt_B2P
     | [ |- context[ Z.lt _ _ ] ] => rewrite <- Z.ltb_lt
-    | [ |- context[ Z.gt _ _ ] ] => rewrite Z.gt_lt_iff; rewrite <- Z.ltb_lt
+    | [ |- context[ Z.gt _ _ ] ] => rewrite Zgt_is_gt_bool
     | [ |- context[ Z.le _ _ ] ] => rewrite <- Z.leb_le
-    | [ |- context[ Z.ge _ _ ] ] => rewrite Z.ge_le_iff; rewrite <- Z.leb_le
+    | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge
     | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq
 
     | [ |- context[ @Logic.eq ?t _ _ ] ] =>
@@ -77,7 +83,243 @@ Ltac prop2bool :=
     | [ |- context[ True ] ] => rewrite <- TrueB
 
     | [ |- context[ False ] ] => rewrite <- FalseB
+    end.
 
-    (* | [ |- _ : (CompDec _ )] => try easy *)
+
+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[ 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
+  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[@eq ?A _ _] ] => instantiate (prop2bool_t_evar := A); instantiate (prop2bool_comp_evar := true)
+           | _ => instantiate (prop2bool_t_evar := nat); instantiate (prop2bool_comp_evar := false)
+           end;
+    destruct HFalse
+  | ];
+  clear H';
+  match (eval compute in prop2bool_comp) with
+  | true =>
+    let A := eval cbv in prop2bool_t in
+    match goal with
+    | [ _ : CompDec A |- _ ] => idtac
+    | _ =>
+      let Hcompdec := fresh "Hcompdec" in
+      assert (Hcompdec: CompDec A);
+      [ auto with typeclass_instances | ]
+    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;
+      match 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 | ];
+
+    (* Replace the Prop version with the bool version *)
+    clear H; assert (H:=H'); clear H'
+  ].
+
+Ltac prop2bool_hyps Hs :=
+  match Hs with
+  | (?Hs, ?H) => try prop2bool_hyp H; [ .. | prop2bool_hyps Hs]
+  | ?H => try prop2bool_hyp H
+  end.
+
+
+
+Section Test.
+  Variable A : Type.
+
+  Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+  Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
+  Hypothesis uninterpreted_type : forall (a:A), a = a.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp basic.
+    prop2bool_hyp no_eq.
+    prop2bool_hyp uninterpreted_type.
+  Abort.
+
+  Goal True.
+  Proof.
+    prop2bool_hyps (basic, no_eq, uninterpreted_type).
+  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).
+
+  Variable e' : G.
+  Hypothesis other_id : forall e' z, op e' z = z.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp associative.
+    prop2bool_hyp identity.
+    prop2bool_hyp inverse.
+    prop2bool_hyp other_id.
+    exact I.
+  Qed.
+
+  Goal True.
+  Proof.
+    prop2bool_hyps (associative, identity, inverse, other_id).
+    exact I.
+  Qed.
+
+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.
+
+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.
+  Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp basic.
+    Fail prop2bool_hyp uninterpreted_type.
+  Abort.
+
+End Poly.
+
+
+
+
+
+Infix "--->" := implb (at level 60, right associativity) : bool_scope.
+Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
+
+
+
+(* 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: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.
diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index 6b69058..398d066 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Export PropToBool BoolToProp.  (* Before SMTCoq.State *)
+Require Export PropToBool.
 Require Export Int63 List PArray.
 Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances.
 Require Export Tactics.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 89d6c62..50c02b7 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -764,6 +764,7 @@ End list.
 Hint Resolve unit_ord unit_eqbtype unit_comp unit_inh unit_compdec : typeclass_instances.
 Hint Resolve bool_ord bool_eqbtype bool_dec bool_comp bool_inh bool_compdec : typeclass_instances.
 Hint Resolve Z_ord Z_eqbtype Z_dec Z_comp Z_inh Z_compdec : typeclass_instances.
+Hint Resolve Nat_ord Nat_eqbtype Nat_dec Nat_comp Nat_inh Nat_compdec : typeclass_instances.
 Hint Resolve Positive_ord Positive_eqbtype Positive_dec Positive_comp Positive_inh Positive_compdec : typeclass_instances.
 Hint Resolve BV_ord BV_eqbtype BV_dec BV_comp BV_inh BV_compdec : typeclass_instances.
 Hint Resolve FArray_ord FArray_eqbtype FArray_dec FArray_comp FArray_inh FArray_compdec : typeclass_instances.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index a6d0023..ca5f3cc 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -355,7 +355,6 @@ let rec mk_bv_list = function
 
 
 (* Reification *)
-
 let mk_bool b =
   let c, args = Structures.decompose_app b in
   if Structures.eq_constr c (Lazy.force ctrue) then true
@@ -435,3 +434,27 @@ let mk_bvsize n =
       else assert false
     | _ -> assert false
   else mk_N n
+
+(** Switches between constr and OCaml *)
+(* Transform a option constr into a constr option *)
+let option_of_constr_option co =
+  let c, args = Structures.decompose_app co in
+  if c = Lazy.force cSome then
+    match args with
+      | [_;c] -> Some c
+      | _ -> assert false
+  else
+    None
+
+(* Transform a tuple of constr into a (reversed) list of constr *)
+let list_of_constr_tuple =
+  let rec list_of_constr_tuple acc t =
+    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
+        | _ -> assert false
+    else
+      t::acc
+  in
+  list_of_constr_tuple []
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index bf626b3..b5ca6b7 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int
 val mk_N : Structures.constr -> int
 val mk_Z : Structures.constr -> int
 val mk_bvsize : Structures.constr -> int
+
+(* Switches between constr and OCaml *)
+val option_of_constr_option : Structures.constr -> Structures.constr option
+val list_of_constr_tuple : Structures.constr -> Structures.constr list
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..aad8b07 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -23,8 +23,8 @@ let mkInt i =
 (** Generic representation of shared object *)
 type 'a gen_hashed = { index : int; hval : 'a }
 
-(** Functions over constr *)
 
+(** Functions over constr *)
 let mklApp f args = Structures.mkApp (Lazy.force f, args)
 
 let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index fbc04e3..3080372 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -218,6 +218,16 @@ let verit_logic =
   SL.of_list [LUF; LLia]
 
 let tactic_gen vm_cast lcpl lcepl =
+  (* Transform the tuple of lemmas given by the user into a list *)
+  let lcpl =
+    let lcpl = EConstr.Unsafe.to_constr lcpl in
+    let lcpl = CoqTerms.option_of_constr_option lcpl in
+    match lcpl with
+      | Some lcpl -> CoqTerms.list_of_constr_tuple lcpl
+      | None -> []
+  in
+
+  (* Core tactic *)
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 6fa62d8..4b84b58 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
 val theorem : Structures.id -> string -> string -> unit
-val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 4162f13..6ddf5a5 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -10,18 +10,18 @@
 (**************************************************************************)
 
 
-Require Import PropToBool BoolToProp.  (* Before SMTCoq.State *)
+Require Import PropToBool.
 Require Import Int63 List PArray Bool ZArith.
 Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst.
 
 Declare ML Module "smtcoq_plugin".
 
 
-Tactic Notation "verit_bool" constr_list(h) :=
-  verit_bool_base h; vauto.
+Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto.
+Tactic Notation "verit_bool"           := verit_bool_base (@None nat); vauto.
 
-Tactic Notation "verit_bool_no_check" constr_list(h) :=
-  verit_bool_no_check_base h; vauto.
+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.
 
 
 (** Tactics in Prop **)
@@ -29,32 +29,18 @@ Tactic Notation "verit_bool_no_check" constr_list(h) :=
 Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
 Ltac zchaff_no_check := prop2bool; zchaff_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 ].
+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 ].
 
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
-
-(* Ltac smt := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool *)
-(*                 | [ |- _ : bool] => try (cvc4_bool; verit_bool) *)
-(*               end; *)
-(*             bool2prop. *)
-(* Ltac smt_no_check := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool_no_check *)
-(*                 | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *)
-(*               end; *)
-(*             bool2prop. *)
-
-Tactic Notation "smt" constr_list(h) := (prop2bool; [ .. | try verit_bool h; cvc4_bool; try verit_bool h; bool2prop ]).
-Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; [ .. | try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; 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]).
 
 
 
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index e067da8..86dd443 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -149,7 +149,6 @@ Misc.v
 SMTCoq.v
 ReflectFacts.v
 PropToBool.v
-BoolToProp.v
 QInst.v
 Tactics.v
 SMT_terms.v
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
index 6c3b8cf..2411316 100644
--- a/src/versions/standard/g_smtcoq_standard.ml4
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -109,8 +109,8 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
-| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
+| [ "verit_bool_base" constr(lpl) ] -> [ Verit.tactic lpl (get_lemmas ()) ]
+| [ "verit_bool_no_check_base" constr(lpl) ] -> [ Verit.tactic_no_check lpl (get_lemmas ()) ]
 END
 
 TACTIC EXTEND Tactic_cvc4
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v
index a948e06..eb9744b 100644
--- a/unit-tests/Tests_lfsc_tactics.v
+++ b/unit-tests/Tests_lfsc_tactics.v
@@ -764,11 +764,11 @@ Section Group.
 
   Lemma simplification_right x1 x2 y:
       op x1 y ==? op x2 y -> x1 ==? x2.
-  Proof. intro H. smt_no_check H inverse'. Qed.
+  Proof. intro H. smt_no_check (H, 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. intro H. smt_no_check (H, inverse'). Qed.
 
   Clear_lemmas.
 End Group.
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 83acc45..59c40a1 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -529,34 +529,59 @@ Qed.
 (* Some examples of using verit with lemmas. Use <verit H1 .. Hn>
    to temporarily add the lemmas H1 .. Hn to the verit environment. *)
 
-Lemma taut1 :
+Lemma taut1_bool :
   forall f, f 2 =? 0 -> f 2 =? 0.
 Proof using. intros f p. verit p. Qed.
 
+Lemma taut1 :
+  forall f, f 2 = 0 -> f 2 = 0.
+Proof using. intros f p. verit p. Qed.
+
+Lemma taut2_bool :
+  forall f, 0 =? f 2 -> 0 =? f 2.
+Proof using. intros f p. verit p. Qed.
+
 Lemma taut2 :
-  forall f, 0 =? f 2 -> 0 =?f 2.
+  forall f, 0 = f 2 -> 0 = f 2.
 Proof using. intros f p. verit p. Qed.
 
-Lemma taut3 :
+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. intros f p1 p2. verit (p1, p2). Qed.
 
-Lemma taut4 :
+Lemma taut3 :
+  forall f, f 2 = 0 -> f 3 = 5 -> f 2 = 0.
+Proof using. intros f p1 p2. verit (p1, p2). 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. intros f p1 p2. verit (p1, p2). Qed.
+
+Lemma taut4 :
+  forall f, f 3 = 5 -> f 2 = 0 -> f 2 = 0.
+Proof using. intros f p1 p2. verit (p1, p2). Qed.
 
 Lemma test_eq_sym a b : implb (a =? b) (b =? a).
 Proof using. verit. Qed.
 
-Lemma taut5 :
+Lemma taut5_bool :
   forall f, 0 =? f 2 -> f 2 =? 0.
 Proof using. intros f p. verit p. Qed.
 
-Lemma fun_const_Z :
+Lemma taut5 :
+  forall f, 0 = f 2 -> f 2 = 0.
+Proof using. intros f p. verit p. Qed.
+
+Lemma fun_const_Z_bool :
   forall f , (forall x, f x =? 2) ->
              f 3 =? 2.
 Proof using. intros f Hf. verit Hf. Qed.
 
+Lemma fun_const_Z :
+  forall f , (forall x, f x = 2) ->
+             f 3 = 2.
+Proof using. intros f Hf. verit Hf. Qed.
+
 Lemma lid (A : bool) :  A -> A.
 Proof using. intro a. verit a. Qed.
 
@@ -564,23 +589,40 @@ Lemma lpartial_id A :
   (xorb A A) -> (xorb A A).
 Proof using. intro xa. verit xa. Qed.
 
-Lemma llia1 X Y Z:
+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.
 
-Lemma llia2 X:
+Lemma llia1 X Y Z:
+  (X <= 3) /\ ((Y <= 7) \/ (Z <= 9)) ->
+  (X + Y <= 10) \/ (X + Z <= 12).
+Proof using. intro p. verit p. Qed.
+
+Lemma llia2_bool X:
   X - 3 =? 7 -> X >=? 10.
 Proof using. intro p. verit p. Qed.
 
-Lemma llia3 X Y:
+Lemma llia2 X:
+  X - 3 = 7 -> X >= 10.
+Proof using. intro p. verit p. Qed.
+
+Lemma llia3_bool X Y:
   X >? Y -> Y + 1 <=? X.
 Proof using. intro p. verit p. Qed.
 
-Lemma llia6 X:
+Lemma llia3 X Y:
+  X > Y -> Y + 1 <= X.
+Proof using. intro p. verit p. Qed.
+
+Lemma llia6_bool X:
   andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10.
 Proof using. intro p. verit p. Qed.
 
+Lemma llia6 X:
+  ((X - 3) <= 7) /\ (7 <= (X - 3)) -> X >= 10.
+Proof using. 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))
@@ -588,43 +630,76 @@ Lemma even_odd b1 b2 x1 x2:
   ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
 Proof using. intro p. verit p. Qed.
 
-Lemma lcongr1 (a b : Z) (P : Z -> bool) f:
+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. intros eqfab pfa. verit (eqfab, pfa). Qed.
 
-Lemma lcongr2 (f:Z -> Z -> Z) x y z:
+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.
+
+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.
 
-Lemma lcongr3 (P:Z -> Z -> bool) x y z:
+Lemma lcongr2 (f:Z -> Z -> Z) x y z:
+  x = y -> f z x = f z y.
+Proof using. intro p. verit p. 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. intros eqxy pzx. verit (eqxy, pzx). Qed.
 
-Lemma test20 :  forall x, (forall a, a <? x) -> 0 <=? x = false.
+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.
+
+Lemma test20_bool :  forall x, (forall a, a <? x) -> 0 <=? x = false.
 Proof using. intros x H. verit H. Qed.
 
-Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
+Lemma test20 :  forall x, (forall a, a < x) -> ~ (0 <= x).
 Proof using. intros x H. verit H. Qed.
 
-Lemma un_menteur (a b c d : Z) dit:
+Lemma test21_bool : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
+Proof using. intros x H. verit H. Qed.
+
+Lemma test21 : forall x, (forall a, ~ (x <= a)) -> ~ (0 <= x).
+Proof using. intros x H. verit H. Qed.
+
+Lemma un_menteur_bool (a b c d : Z) dit:
   dit a =? c ->
   dit b =? d ->
   (d =? a) || (b =? c) ->
   (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. intros H1 H2 H3 H4 H5. verit (H1, H2, H3, H4, H5). Qed.
 
-Lemma const_fun_is_eq_val_0 :
+Lemma un_menteur (a b c d : Z) dit:
+  dit a = c ->
+  dit b = d ->
+  (d = a) \/ (b = c) ->
+  (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.
+
+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.
 
-(* 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,
-   you should use <Clear_lemmas> to empty the globally added lemmas because
-   those lemmas won't be available outside of the section. *)
+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.
+
+(* 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
+   need them anymore (all the time, but especially for lemmas that were
+   section hypotheses before closing the section) *)
 
 Section S.
   Variable f : Z -> Z.
@@ -838,7 +913,7 @@ Section GroupZ.
 End GroupZ.
 
 
-Section Group.
+Section GroupBool.
   Variable G : Type.
   Variable HG : CompDec G.
   Variable op : G -> G -> G.
@@ -855,18 +930,59 @@ Section Group.
     forall a : G, (op a (inv a) ==? e) && (op (inv a) a ==? e).
   Add_lemmas associative identity inverse.
 
-  Lemma unique_identity e':
+  Lemma unique_identity_bool e':
     (forall z, op e' z ==? z) -> e' ==? e.
   Proof using associative identity inverse. intros pe'. verit pe'. Qed.
 
-  Lemma simplification_right x1 x2 y:
+  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.
 
-  Lemma simplification_left x1 x2 y:
+  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.
 
+  Clear_lemmas.
+End GroupBool.
+
+
+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).
+  (* TODO: apply [prop2bool_hyp] to lemmas added with [Add_lemmas] *)
+  (* Add_lemmas associative identity inverse. *)
+
+  Lemma unique_identity e':
+    (forall z, op e' z = z) -> e' = e.
+  Proof using associative identity inverse HG.
+    intros pe'.
+    verit (associative, identity, inverse, pe').
+  Qed.
+
+  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).
+  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).
+  Qed.
+
   Clear_lemmas.
 End Group.
 
@@ -893,23 +1009,43 @@ Section Linear2.
 (* Proof using. verit g_2_linear. *)
 End Linear2.
 
-Section Input_switched1.
+Section Input_switched1Bool.
   Variable m : Z -> Z.
 
   Hypothesis m_0 : m 0 =? 5.
 
   (* veriT switches the input lemma in this case *)
-  Lemma cinq_m_0 : m 0 =? 5.
+  Lemma five_m_0_bool : m 0 =? 5.
+  Proof using m_0. verit m_0. Qed.
+End Input_switched1Bool.
+
+Section Input_switched1.
+  Variable m : Z -> Z.
+
+  Hypothesis m_0 : m 0 = 5.
+
+  (* veriT switches the input lemma in this case *)
+  Lemma five_m_0 : m 0 = 5.
   Proof using m_0. verit m_0. Qed.
 End Input_switched1.
 
-Section Input_switched2.
+Section Input_switched2Bool.
   Variable h : Z -> Z -> Z.
 
   Hypothesis h_Sm_n : forall x y, h (x+1) y =? h x y.
 
   (* veriT switches the input lemma in this case *)
-  Lemma h_1_0 : h 1 0 =? h 0 0.
+  Lemma h_1_0_bool : h 1 0 =? h 0 0.
+  Proof using h_Sm_n. verit h_Sm_n. Qed.
+End Input_switched2Bool.
+
+Section Input_switched2.
+  Variable h : Z -> Z -> Z.
+
+  Hypothesis h_Sm_n : forall x y, h (x+1) y = h x y.
+
+  (* veriT switches the input lemma in this case *)
+  Lemma h_1_0 : h 1 0 = h 0 0.
   Proof using h_Sm_n. verit h_Sm_n. Qed.
 End Input_switched2.
 
@@ -1079,10 +1215,7 @@ Section AppliedPolymorphicTypes2.
   Proof. verit. Qed.
 
   Hypothesis append_assoc_B :
-    forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 ++ (l2 ++ l3)) ((l1 ++ l2) ++ l3) = true.
-  (* TODO: make it possible to apply prop2bool to hypotheses *)
-  (* Hypothesis append_assoc_B : *)
-  (*   forall l1 l2 l3 : list B, l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. *)
+    forall l1 l2 l3 : list B, l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
 
   (* The hypothesis is not used *)
   Goal forall l1 l2 l3 l4 : list B,
-- 
cgit