Use trakt

7 files changed, 712 insertions, 951 deletions

diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
deleted file mode 100644
index 0483db0..0000000
--- a/src/Conversion_tactics.v
+++ /dev/null
@@ -1,460 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-(* This file provides:
-   - a generic way to inject, via tactics, types of natural numbers into
-     the type Z, which is the type known by SMT solvers and, thus, by
-     SMTCoq
-   - an instanciation for the types nat, positive and N.
-*)
-
-
-
-Require Import ZArith.
-
-(* This module represents the structure to be injected into Z *)
-Module Type convert_type.
-
-(* The type to be injected *)
-Parameter T : Type.
-
-(* Mapping both ways *)
-Parameter Z2T : Z -> T.
-Parameter T2Z : T -> Z.
-(* T2Z is an injection *)
-Axiom T2Z_id : forall x : T, Z2T (T2Z x) = x.
-
-(* A property about elements of Z coming from elements of T.
-   For instance, for nat, all elements are non-negative: (0 <=? z)%Z *)
-Parameter inT : Z -> bool.
-(* The image of the injection satisfies this property *)
-Axiom T2Z_pres : forall x : T, inT (T2Z x) = true.
-(* It is always possible to define inT as <fun z => Z.eqb z (T2Z (Z2T z))>.
-   In this case, the proof of the axiom is simply:
-    <rewrite T2Z_id, Z.eqb_eq>. *)
-
-(* We ask this injection to be a morphism for all the following symbols *)
-
-(* Addition *)
-Parameter add : T -> T -> T.
-Axiom t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y').
-
-(* Multiplication *)
-Parameter mul : T -> T -> T.
-Axiom t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y').
-
-(* <= *)
-Parameter leb : T -> T -> bool.
-Axiom t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'.
-
-(* < *)
-Parameter ltb : T -> T -> bool.
-Axiom t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'.
-
-(* = *)
-Parameter eqb : T -> T -> bool.
-Axiom t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'.
-End convert_type.
-
-(* This fonctor builds a conversion tactic from a module of the signature above *)
-Module convert (M : convert_type).
-
-Import M.
-
-(* SMTCoq uses Booleans *)
-Lemma implb_impl : forall a b : bool, (implb a b = true -> a = true -> b = true).
-Proof.
-intros a b H.
-destruct a; destruct b; try reflexivity; discriminate.
-Qed.
-
-(* Get the head symbol of an application *)
-Ltac get_head x := lazymatch x with ?x _ => get_head x | _ => x end.
-
-(* [inverse_tactic tactic] succceds when [tactic] fails, and the other way round *)
-Ltac inverse_tactic tactic := try (tactic; fail 1).
-
-(* [constr_neq t u] fails if and only if [t] and [u] are convertible *)
-Ltac constr_neq t u := inverse_tactic ltac:(constr_eq t u).
-
-(* [is_not_constructor U sym] fails if and only if [sym] is a constructor of [U] *)
-Ltac is_not_constructor U sym :=
-let H := fresh in
-assert (U -> True) as H by
-       (let x := fresh in
-        let y := fresh in
-        intro x;
-        pose x as y;
-        destruct x;
-        let C := eval unfold y in y in
-        let c := get_head C in
-        constr_neq sym c;
-        exact I); clear H.
-
-(* [is_constructor U sym] succeeds if and only if [sym] is a constructor of [U] *)
-Ltac is_constructor U sym := inverse_tactic ltac:(is_not_constructor U sym).
-
-(* Replaces the sub-terms [x] of type [T] which are not under a known
-   symbol by Z2T (T2Z x) *)
-Ltac converting :=
-  (* The heart of the tactic *)
-  repeat
-    match goal with
-    (* We capture each subèterm [x] together with its context, i.e. the goal is C[x] *)
-    | |- context C[?x]  =>
-      (* If [x] has type [T] *)
-      let U := type of x in
-      lazymatch eval fold T in U with
-      | T =>
-        lazymatch x with
-        (* If x is of the shape Z2T (T2Z _) we stop since [x] is already in the expected shape *)
-        | Z2T (T2Z _) => fail
-        | _ =>
-          (* We generate a fresh variable of type T *)
-          let var := fresh in
-          pose proof x as var;
-          (* Otherwise, we analyze the formula obtained by replacing [x] by the fresh variable in the goal *)
-          lazymatch context C[var] with
-          | context [?h var] =>
-            let h := get_head h in
-            lazymatch h with
-            (* [x] is already in the expected shape *)
-            | T2Z => fail
-            (* Not necessary to rewrite under symbols commuting with T2Z *)
-            | add => fail | mul => fail | ltb => fail | leb => fail | eqb => fail
-            (* Do not rewrite inside a constant *)
-            | Zpos => fail | Zneg => fail
-            | _ =>
-            (* Idem: if the context contains a constructor of [T], and
-               [x] starts with a constructor of [T], we are inside a
-               constant *)
-            let hx := get_head x in
-            try (is_constructor T h; is_constructor T hx; fail 1);
-            (* Otherwise, we rewrite *)
-            let old_goal := context C[x] in
-            let new_goal := context C[Z2T (T2Z x)] in
-            replace old_goal with new_goal by (rewrite (T2Z_id x); reflexivity) end
-          end;
-          (* We clear the fresh variable *)
-          clear var
-        end
-      end
-    end.
-
-Ltac rewriting :=
-  repeat (try rewrite <- t2z_leb_morph;
-          try rewrite <- t2z_ltb_morph;
-          try rewrite <- t2z_eqb_morph;
-          try rewrite <- t2z_add_morph;
-          try rewrite <- t2z_mul_morph).
-
-
-(* expand_type [Tn;...T2;;T1] T = T1->T2->...->Tn->T *)
-Fixpoint expand_type l T : Type :=
-  match l with
-    | nil => T
-    | cons h l => expand_type l (h -> T)
-  end.
-(* get_args (f t1 t2 ... tn) = [(Tn,tn);...;(T2,t2);(T1,t1)] *)
-Ltac get_args X :=
-  lazymatch X with
-    | ?x ?y => let x_args := get_args x in let T := type of y in constr:(cons (existT (fun z => z) T y) x_args)
-    | _ => constr:(@nil (sigT (fun x => x)))
-  end.
-(* get_args_types [(Tn,tn);...;(T2,t2);(T1,t1)] = [Tn;...;T2;T1] *)
-Fixpoint get_args_types (l : list (sigT (fun x => x))) : list Type :=
-  match l with
-    | nil => nil
-    | cons (@existT _ _ T _) l => cons T (get_args_types l)
-  end.
-(* apply_args [(Tn,tn);...;(T2,t2);(T1,t1)] T (f : T1->T2->...->Tn->T) = f t1 t2 ... tn *)
-Ltac apply_args f args :=
-  lazymatch args with
-    | nil => constr:(f)
-    | cons ?arg ?args => match arg with existT _ _ ?arg => let f := apply_args f args in constr:(f arg) end
-  end.
-
-(* expand_fun [Tn;...;T2;T1] T U (f : T1->T2->...->Tn->T) (g : T->U) = fun x1 x2 ... xn => g (f x1 x2 ... xn) *)
-Fixpoint expand_fun (l : list Type) (T : Type) (U : Type) : expand_type l T -> (T -> U) -> expand_type l U :=
-  match l with
-    | nil => fun f g => g f
-    | cons h l' => fun f g => expand_fun l' (h -> T) (h -> U) f (fun a x => g (a x))
-  end.
-(* expand (f (t1:T1) (t2:T2) ... (tn:Tn) : T) (g : T->U) = fun x1 x2 ... xn => g (f x1 x2 ... xn) *)
-Ltac expand X g :=
-  (* Let argsX = [(Tn,tn);...;(T2,t2);(T1,t1)] *)
-  let argsX := get_args X in
-  (* Let argsXtypes = [Tn;...;T2;T1] *)
-  let argsXtypes := constr:(get_args_types argsX) in
-  (* Let typeX = T *)
-  let typeX := type of X in
-  (* Let h = f *)
-  let h := get_head X in
-  (* Let typeg = U *)
-  let typeg := match type of g with _ -> ?U => U end in
-  (* We return expand_fun [Tn;...;T2;T1] T Z f T2Z = fun x1 x2 ... xn => g (f x1 x2 ... xn) *)
-  constr:(expand_fun argsXtypes typeX typeg h g).
-
-(* Replaces function symbols with return type in T, and variables in T,
-   by their counterparts in Z, adding the positivity hypotheses *)
-Ltac renaming :=
-  repeat
-    match goal with
-      (* If there is a term of the shape (T2Z (f t1 ... tn)) *)
-      | |- context [T2Z ?X] =>
-        (* Get the head symbol *)
-        let f := get_head X in
-        (* Nothing to do if it is a constructor *)
-        is_not_constructor T f;
-        (* Otherwise, let fe = fun x1 ... xn => T2Z (f x1 ... xn) *)
-        let fe := expand X T2Z in
-        let fe := eval cbv in fe in
-        (* Pose fe_id := fun x1 ... xn => T2Z (f x1 ... xn) *)
-        let fe_id := fresh in pose (fe_id := fe);
-        repeat
-          match goal with
-            (* For each term of the shape (T2Z (f' t'1 ... t'n)) *)
-            | |- context [T2Z ?X'] =>
-              (* Get the head symbol *)
-              let f' := get_head X' in
-              (* If f' = f *)
-              constr_eq f f';
-              (* Add the hypothesis inT (T2Z X') *)
-              generalize (T2Z_pres X'); apply implb_impl;
-              (* Let args = [t'1;...;t'n] *)
-              let args := get_args X' in
-              (* Let Y = fe_id t'1 ... t'n *)
-              let Y := apply_args fe_id args in
-              (* Replace [T2Z (f' t'1 ... t'n)] by [Y] *)
-              change (T2Z X') with Y
-          end;
-        (* Abstract over [fe_id := fun x1 ... xn => T2Z (f x1 ... xn)] *)
-        generalize fe_id;
-        (* Erase the old f and the temporary fe_id *)
-        clear f fe_id;
-        (* Introduce the new f with the same name *)
-        let f := fresh f in
-        intro f
-    end.
-
-(* expand_fun' [Tn;...;T2;T1] T U (f : T1->T2->...->Tn->T) (a : T->U) = fun x1 x2 ... xn => a (f x1 x2 ... xn) *)
-Fixpoint expand_fun' (l : list Type) : forall T U : Type, expand_type l T -> (T -> U) -> expand_type l U :=
-  match l as l return forall T U, expand_type l T -> (T ->U) -> expand_type l U with
-    | nil => fun T U f a => a f
-    | cons T' l => fun T U f a => expand_fun' l (T' -> T) (T' -> U) f (fun g xn => a (g xn))
-  end.
-(* expand' (f (t1:T1) (t2:T2) ... (tn:Tn) : T) (g : U->Tn) = fun x1 x2 ... xn => f x1 x2 ... (g xn) *)
-Ltac expand' X g :=
-  (* Let argsX = [(Tn,tn);...;(T2,t2);(T1,t1)] *)
-  let argsX := get_args X in
-  (* Let argsXtypes = [Tn;...;T2;T1] *)
-  let argsXtypes := constr:(get_args_types argsX) in
-  let argsXtypes := eval cbv in argsXtypes in
-  (* Let Tn = Tn *)
-  let Tn := match argsXtypes with cons ?T _ => T end in
-  (* Let argsXtypes = [Tn-1;...;T2;T1] *)
-  let argsXtypes := match argsXtypes with cons _ ?args => args end in
-  (* Let typeX = T *)
-  let typeX := type of X in
-  (* Let h = f *)
-  let h := get_head X in
-  (* Let typeg = U *)
-  let typeg := match type of g with ?U -> _ => U end in
-  (* Return expand_fun' [Tn-1;...;T2;T1] (Tn->T) (Z->T) f (fun b x => b (g x))) = fun x1 x2 ... xn => f x1 x2 ... (g xn) *)
-  constr:(expand_fun' argsXtypes (Tn -> typeX) (typeg -> typeX) h (fun b x => b (g x))).
-
-(* Replaces function symbols with parameters in T, with their
-   counterparts with parameters in Z *)
-Ltac renaming' :=
-  repeat
-    match goal with
-      (* If there is a term of the shape (f t1 ... (Z2T tn)) *)
-      | |- context [?X (Z2T ?Y)] =>
-        (* Get the head symbol *)
-        let f := get_head X in
-        (* Nothing to do if it is a constructor *)
-        is_not_constructor T f;
-        (* Otherwise, let fe = fun x1 ... xn => f x1 ... (Z2T xn) *)
-        let fe := expand' (X (Z2T Y)) Z2T in
-        let fe := eval simpl in fe in
-        repeat
-          match goal with
-            (* For each term of the shape (f' t'1 ... (Z2T t'n)) *)
-            | |- context [?X' (Z2T ?Y')] =>
-              (* Get the head symbol *)
-              let f' := get_head X' in
-              (* If f' = f *)
-              constr_eq f f';
-              (* Let args = [t'1;...;t'(n-1)] *)
-              let args := get_args X' in
-              (* Let Z = (fun x1 ... xn => f x1 ... (Z2T xn)) t'1 ... t'(n-1) *)
-              let Z := apply_args fe args in
-              (* Replace (f' t'1 ... (Z2T t'n)) with (Z t'n) *)
-              change (X' (Z2T Y')) with (Z Y')
-          end;
-        (* Abstract over (fun x1 ... xn => (f x1 ... (Z2T xn)) *)
-        generalize fe;
-        (* Erase the old f *)
-        clear f;
-        (* Introduce the new f with the same name *)
-        let f := fresh f in
-        intro f
-    end.
-
-(* The whole tactic *)
-Ltac convert :=
-fold T add mul ltb leb eqb;
-intros;
-converting;
-rewriting;
-renaming;
-renaming';
-let T2Z_unfolded := eval red in T2Z in change T2Z with T2Z_unfolded;
-let inT_unfolded := eval red in inT in change inT with inT_unfolded;
-simpl.
-
-End convert.
-
-(* Instanciation for the type [positive] *)
-Module pos_convert_type <: convert_type.
-
-Definition T : Type := positive.
-
-Definition Z2T : Z -> T := fun z =>
-  match z with
-    | 0%Z => 1%positive
-    | Zpos p => p
-    | Zneg _ => 1%positive
-  end.
-
-Definition T2Z : T -> Z := Zpos.
-Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. reflexivity. Qed.
-
-Definition inT : Z -> bool := fun z => Z.ltb 0 z.
-Lemma T2Z_pres : forall x, inT (T2Z x) = true. reflexivity. Qed.
-
-Definition add : T -> T -> T := Pos.add.
-Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y').
-Proof. reflexivity. Qed.
-
-Definition mul : T -> T -> T := Pos.mul.
-Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y').
-Proof. reflexivity. Qed.
-
-Definition leb : T -> T -> bool := Pos.leb.
-Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'.
-Proof. reflexivity. Qed.
-
-Definition ltb : T -> T -> bool := Pos.ltb.
-Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'.
-Proof. reflexivity. Qed.
-
-Definition eqb : T -> T -> bool := Pos.eqb.
-Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'.
-Proof. reflexivity. Qed.
-End pos_convert_type.
-
-Module pos_convert_mod := convert pos_convert_type.
-
-Ltac pos_convert := pos_convert_mod.convert.
-
-
-(* Instanciation for the type [N] *)
-Module N_convert_type <: convert_type.
-
-Definition T : Type := N.
-
-Definition Z2T : Z -> T := Z.to_N.
-
-Definition T2Z : T -> Z := Z.of_N.
-Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. exact N2Z.id. Qed.
-
-Definition inT : Z -> bool := fun z => Z.leb 0 z.
-Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply N2Z.is_nonneg. Qed.
-
-Definition add : T -> T -> T := N.add.
-Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y').
-Proof. intros x y; destruct x, y; reflexivity. Qed.
-
-Definition mul : T -> T -> T := N.mul.
-Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y').
-Proof. intros x y; destruct x, y; reflexivity. Qed.
-
-Definition leb : T -> T -> bool := N.leb.
-Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'.
-Proof. intros x y; destruct x, y; reflexivity. Qed.
-
-Definition ltb : T -> T -> bool := N.ltb.
-Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'.
-Proof. intros x y; destruct x, y; reflexivity. Qed.
-
-Definition eqb : T -> T -> bool := N.eqb.
-Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'.
-Proof. intros x y; destruct x, y; reflexivity. Qed.
-
-End N_convert_type.
-
-Module N_convert_mod := convert N_convert_type.
-
-Ltac N_convert := N_convert_mod.convert.
-
-(* Instanciation for the type [nat] *)
-Require Import NPeano.
-Module nat_convert_type <: convert_type.
-
-Definition T : Type := nat.
-
-Definition Z2T : Z -> T := Z.to_nat.
-
-Definition T2Z : T -> Z := Z.of_nat.
-Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. exact Nat2Z.id. Qed.
-
-Definition inT : Z -> bool := fun z => Z.leb 0 z.
-Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply Nat2Z.is_nonneg. Qed.
-
-Definition add : T -> T -> T := Nat.add.
-Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y').
-Proof. symmetry. apply Nat2Z.inj_add. Qed.
-
-Definition mul : T -> T -> T := Nat.mul.
-Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y').
-Proof. symmetry. apply Nat2Z.inj_mul. Qed.
-
-Definition leb : T -> T -> bool := Nat.leb.
-Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'.
-Proof.
-  intros x y; unfold leb.
-  case_eq (Nat.leb x y); [| rewrite <- 2 Bool.not_true_iff_false];
-  rewrite <- Zle_is_le_bool; rewrite Nat.leb_le; rewrite Nat2Z.inj_le; auto.
-Qed.
-
-Definition ltb : T -> T -> bool := Nat.ltb.
-Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'.
-Proof.
-  intros x y; unfold ltb.
-  case_eq (Nat.ltb x y); [| rewrite <- 2 Bool.not_true_iff_false];
-  rewrite <- Zlt_is_lt_bool; rewrite Nat.ltb_lt; rewrite Nat2Z.inj_lt; auto.
-Qed.
-
-Definition eqb : T -> T -> bool := Nat.eqb.
-Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'.
-Proof.
-  intros x y; unfold eqb.
-  case_eq (Nat.eqb x y); [| rewrite <- 2 Bool.not_true_iff_false];
-  rewrite Z.eqb_eq; rewrite Nat.eqb_eq; rewrite Nat2Z.inj_iff; auto.
-Qed.
-
-End nat_convert_type.
-
-Module nat_convert_mod := convert nat_convert_type.
-
-Ltac nat_convert := nat_convert_mod.convert.
diff --git a/src/PropToBool.v b/src/PropToBool.v
deleted file mode 100644
index 31f8b2d..0000000
--- a/src/PropToBool.v
+++ /dev/null
@@ -1,362 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     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.
-
-
-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
-    match goal with
-    | [ |- forall _ : ?t, _ ] =>
-      lazymatch type of t with
-      | Prop =>
-        match t with
-        | forall _ : _, _ => intro
-        | _ => fail
-        end
-      | _ => intro
-      end
-
-    | [ |- 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 Zgt_is_gt_bool
-    | [ |- context[ Z.le _ _ ] ] => rewrite <- Z.leb_le
-    | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge
-    | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq
-
-    | [ |- context[ @Logic.eq ?t ?x ?y ] ] =>
-      lazymatch t with
-      | bitvector _ => rewrite <- bv_eq_reflect
-      | farray _ _ => rewrite <- equal_iff_eq
-      | Z => rewrite <- Z.eqb_eq
-      | bool =>
-        lazymatch y with
-        | true => fail
-        | _ => rewrite <- (eqb_true_iff x y)
-        end
-      | _ =>
-        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
-
-    | [ |- context[?G0 = true \/ ?G1 = true ] ] =>
-      rewrite (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1));
-      [ | apply orP]
-
-    | [ |- context[?G0 = true -> ?G1 = true ] ] =>
-      rewrite (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1)); 
-      [ | apply implyP]
-
-    | [ |- context[?G0 = true /\ ?G1 = true ] ] =>
-      rewrite (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1));
-      [ | apply andP]
-
-    | [ |- context[?G0 = true <-> ?G1 = true ] ] =>
-      rewrite (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1));
-      [ | apply iffP]
-          
-    | [ |- context[ ~ ?G = true ] ] =>
-      rewrite (@reflect_iff (~ G = true) (negb G));
-      [ | apply negP]
-
-    | [ |- context[ is_true ?G ] ] =>
-      unfold is_true
-
-    | [ |- context[ True ] ] => rewrite <- TrueB
-
-    | [ |- context[ False ] ] => rewrite <- FalseB
-    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
-  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;
-    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);
-      [ 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;
-      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 *)
-    try clear H; let H := fresh H in assert (H:=H'); clear H'
-  ].
-
-
-Ltac remove_compdec_hyp H :=
-  let TH := type of H in
-  match TH with
-  | forall p : CompDec ?A, _ =>
-    match goal with
-    | [ p' : CompDec A |- _ ] =>
-      let H1 := fresh in
-      assert (H1 := H p'); clear H; assert (H := H1); clear H1;
-      remove_compdec_hyp H
-    | _ =>
-      let c := fresh "c" in
-      assert (c : CompDec A);
-      [ try (exact _)
-      | let H1 := fresh in
-        assert (H1 := H c); clear H; assert (H := H1); clear H1;
-        remove_compdec_hyp H ]
-    end
-  | _ => idtac
-  end.
-
-
-Ltac prop2bool_hyps Hs :=
-  lazymatch Hs with
-  | (?Hs1, ?Hs2) => prop2bool_hyps Hs1; [ .. | prop2bool_hyps Hs2]
-  | ?H => remove_compdec_hyp 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)%nat.
-  Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
-  Hypothesis uninterpreted_type : forall (a:A), a = a.
-  Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
-
-  Goal True.
-  Proof.
-    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).
-    admit.
-  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)%nat.
-  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 694f2ed..f3904ae 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -10,9 +10,9 @@
 (**************************************************************************)
 
 
-Require Export PropToBool.
 Require Export Int63 List.
 Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances.
 Require Export Tactics.
-Require Export Conversion_tactics.
 Export Atom Form Sat_Checker Cnf_Checker Euf_Checker.
+From Trakt Require Export Trakt.
+Require Export Database_trakt.
diff --git a/src/Tactics.v b/src/Tactics.v
index 5be62cc..685cfdb 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -10,148 +10,104 @@
 (**************************************************************************)
 
 
-Require Import PropToBool.
+From Trakt Require Import Trakt.
+Require Import Conversion.
 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".
 
 
-(** Collect all the hypotheses from the context *)
-
-Ltac get_hyps_acc acc :=
-  match goal with
-  | [ H : ?P |- _ ] =>
-    let T := type of P in
-    lazymatch T with
-    | Prop =>
-      lazymatch P with
-      | id _ => fail
-      | _ =>
-        let _ := match goal with _ => change P with (id P) in H end in
-        match acc with
-        | Some ?t => get_hyps_acc (Some (H, t))
-        | None => get_hyps_acc (Some H)
-        end
-      end
-    | _ => fail
-    end
-  | _ => 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 :=
-  let Hs := get_hyps_acc (@None nat) in
-  let _ := match goal with _ => eliminate_id end in
-  Hs.
-
-
-(* Section Test. *)
-(*   Variable A : Type. *)
-(*   Hypothesis H1 : forall a:A, a = a. *)
-(*   Variable n : Z. *)
-(*   Hypothesis H2 : n = 17%Z. *)
-
-(*   Goal True. *)
-(*   Proof. *)
-(*     let Hs := get_hyps in idtac Hs. *)
-(*   Abort. *)
-(* End Test. *)
-
-
-(** Tactics in bool *)
+Ltac zchaff          := trakt Z bool; Tactics.zchaff_bool.
+Ltac zchaff_no_check := trakt Z bool; Tactics.zchaff_bool_no_check.
 
 Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; try (exact _).
 Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _).
 
-Tactic Notation "verit_bool" constr(h) :=
-  let Hs := get_hyps in
-  match Hs with
-  | Some ?Hs => verit_bool_base_auto (Some (h, Hs))
-  | None => verit_bool_base_auto (Some h)
-  end;
-  vauto.
-Tactic Notation "verit_bool"           :=
-  let Hs := get_hyps in
-  verit_bool_base_auto Hs; vauto.
-
-Tactic Notation "verit_bool_no_check" constr(h) :=
-  let Hs := get_hyps in
-  match Hs with
-  | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs))
-  | None => verit_bool_no_check_base_auto (Some h)
-  end;
-  vauto.
-Tactic Notation "verit_bool_no_check"           :=
-  let Hs := get_hyps in
-  fun Hs => verit_bool_no_check_base_auto Hs; vauto.
-
-
-(** Tactics in Prop **)
-
-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;
-         [ .. | 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
-         ]
+Tactic Notation "verit" constr(global) :=
+  intros;
+  unfold is_true in *;
+  let Hsglob := pose_hyps global (@None unit) in
+  let local := get_hyps_option in
+  let Hs :=
+      lazymatch local with
+      | Some ?local' => pose_hyps local' Hsglob
+      | None => constr:(Hsglob)
+      end
+  in
+  preprocess1 Hs;
+  [ .. |
+    let Hs' := intros_names in
+    preprocess2 Hs';
+    verit_bool_base_auto Hs';
+    QInst.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;
+  unfold is_true in *;
+  let local := get_hyps_option in
+  let Hs :=
+      lazymatch local with
+      | Some ?local' => pose_hyps local' (@None unit)
+      | None => constr:(@None unit)
+      end
+  in
+  preprocess1 Hs;
+  [ .. |
+    let Hs' := intros_names in
+    preprocess2 Hs';
+    verit_bool_base_auto Hs';
+    QInst.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
-         ]
+
+Tactic Notation "verit_no_check" constr(global) :=
+  intros;
+  unfold is_true in *;
+  let Hsglob := pose_hyps global (@None unit) in
+  let local := get_hyps_option in
+  let Hs :=
+      lazymatch local with
+      | Some ?local' => pose_hyps local' Hsglob
+      | None => constr:(Hsglob)
+      end
+  in
+  preprocess1 Hs;
+  [ .. |
+    let Hs' := intros_names in
+    preprocess2 Hs';
+    verit_bool_no_check_base_auto Hs';
+    QInst.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;
+  unfold is_true in *;
+  let local := get_hyps_option in
+  let Hs :=
+      lazymatch local with
+      | Some ?local' => pose_hyps local' (@None unit)
+      | None => constr:(@None unit)
+      end
+  in
+  preprocess1 Hs;
+  [ .. |
+    let Hs' := intros_names in
+    preprocess2 Hs';
+    verit_bool_no_check_base_auto Hs';
+    QInst.vauto
   ].
 
-Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
-Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
+Ltac cvc4            := trakt Z bool; [ .. | cvc4_bool ].
+Ltac cvc4_no_check   := trakt Z bool; [ .. | cvc4_bool_no_check ].
+
+Tactic Notation "smt" constr(h) := intros; try verit h; cvc4; try verit h.
+Tactic Notation "smt"           := intros; try verit  ; cvc4; try verit.
+Tactic Notation "smt_no_check" constr(h) :=
+  intros; try verit_no_check h; cvc4_no_check; try verit_no_check h.
+Tactic Notation "smt_no_check"           :=
+  intros; try verit_no_check  ; cvc4_no_check; try verit_no_check.
 
-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/src/_CoqProject b/src/_CoqProject
index 9ac5799..21bd41b 100644
--- a/src/_CoqProject
+++ b/src/_CoqProject
@@ -8,7 +8,7 @@
 
 ########################################################################
 ## To generate the Makefile:                                          ##
-##   coq_makefile -f Make -o Makefile                                 ##
+##   coq_makefile -f _CoqProject -o Makefile                          ##
 ##   sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ##
 ## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62)                 ##
 ########################################################################
@@ -26,6 +26,7 @@
 -I lia
 -I smtlib2
 -I trace
+-I preproc
 -I verit
 -I zchaff
 -I PArray
@@ -134,11 +135,12 @@ spl/Syntactic.v
 spl/Arithmetic.v
 spl/Operators.v
 
-Conversion_tactics.v
+preproc/Database_trakt.v
+preproc/Conversion.v
+
 Misc.v
 SMTCoq.v
 ReflectFacts.v
-PropToBool.v
 QInst.v
 Tactics.v
 SMT_terms.v
diff --git a/src/preproc/Conversion.v b/src/preproc/Conversion.v
new file mode 100644
index 0000000..635a47a
--- /dev/null
+++ b/src/preproc/Conversion.v
@@ -0,0 +1,401 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2021                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+From Trakt Require Import Trakt.
+Require Import Database_trakt.
+Require Import ZArith.
+
+Require SMT_classes BVList FArray.
+
+
+(* Conversion tactic *)
+
+Infix "--->" := implb (at level 60, right associativity) : bool_scope.
+Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
+
+
+(* Get all hypotheses of type Prop *)
+
+Ltac get_hyps_option :=
+  match goal with
+  | H : ?P |- _ =>
+    let _ := match goal with _ => revert H end in
+    let acc := get_hyps_option in
+    let _ := match goal with _ => intro H end in
+    let S := type of P in
+    lazymatch S with
+    | Prop =>
+      lazymatch acc with
+      | Some ?acc' => constr:(Some (acc',H))
+      | None => constr:(Some H)
+      end
+    | _ => constr:(acc)
+    end
+  | _ => constr:(@None unit)
+  end.
+
+
+(* Assert global and local hypotheses (local: to avoid problems with Section variables) *)
+
+Ltac pose_hyps Hs acc :=
+  lazymatch Hs with
+  | (?Hs1, ?Hs2) =>
+    let acc1 := pose_hyps Hs1 acc in
+    let acc2 := pose_hyps Hs2 acc1 in
+    constr:(acc2)
+  | ?H' =>
+    let H := fresh "H" in
+    let _ := match goal with _ => assert (H := H') end in
+    lazymatch acc with
+    | Some ?acc' => constr:(Some (acc', H))
+    | None => constr:(Some H)
+    end
+  end.
+
+(* Goal True. *)
+(*   let Hs := pose_hyps ((@List.nil_cons positive 5%positive nil), (@List.nil_cons N 42%N nil), List.nil_cons) (@None unit) in *)
+(*   idtac Hs. *)
+(* Abort. *)
+
+
+(* Get all the hypotheses and the goal *)
+
+Ltac get_context b :=
+  match goal with
+  | H : ?P |- _ =>
+    let _ := match goal with _ => revert H end in
+    let acc := get_context b in
+    let _ := match goal with _ => intro H end in
+    constr:((acc,P))
+  | _ => constr:(b)
+  end.
+
+Ltac get_context_concl :=
+  match goal with
+  | |- ?g => get_context 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. *)
+(* Proof. *)
+(*   intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *)
+(*   let h := get_context_concl in idtac h. *)
+(* Abort. *)
+
+
+(* 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) | nat => constr:(true) | positive => 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 *)
+      match 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_terms t :=
+  match t with
+  | (?t', ?H) =>
+    add_compdecs_term H;
+    add_compdecs_terms t'
+  | ?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. *)
+(*   let h := get_context_concl in add_compdecs_terms h. *)
+(*   Show 3. *)
+(* Abort. *)
+
+
+Ltac add_compdecs :=
+  let h := get_context_concl in
+  add_compdecs_terms h.
+
+(* 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. *)
+(*   Show 3. *)
+(* Abort. *)
+
+
+(* Collect CompDec in local hypotheses *)
+
+Ltac collect_compdecs :=
+  match goal with
+  | H : SMT_classes.CompDec ?T |- _ =>
+    let _ := match goal with _ => change (id (SMT_classes.CompDec T)) in H end in
+    let acc := collect_compdecs in
+    let _ := match goal with _ => change (SMT_classes.CompDec T) in H end in
+    let res :=
+        lazymatch is_interpreted_type T with
+        | true => constr:(acc)
+        | false => constr:((acc, H))
+        end
+    in
+    constr:(res)
+  | _ => constr:(unit)
+  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. *)
+(*   Focus 3. *)
+(*   let cs := collect_compdecs in idtac cs. *)
+(* Abort. *)
+
+
+(* Generate CompDec rels for trakt *)
+
+Ltac generate_rels compdecs :=
+  lazymatch compdecs with
+  | (?compdecs', ?HA) =>
+    let ty := type of HA in
+    lazymatch ty with
+    | SMT_classes.CompDec ?A =>
+      let rel := constr:((@eq A, @SMT_classes.eqb_of_compdec A HA, @SMT_classes.compdec_eq_eqb A HA)) in
+      let acc := generate_rels compdecs' in
+      lazymatch acc with
+      | None => constr:(Some rel)
+      | Some ?res => constr:(Some (res, rel))
+      end
+    end
+  | _ => constr:(@None unit)
+  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. *)
+(*   Focus 3. *)
+(*   let cs := collect_compdecs in *)
+(*   let rels := generate_rels cs in *)
+(*   idtac rels. *)
+(* Abort. *)
+
+
+(* Use trakt *)
+
+Ltac trakt_rels rels :=
+  lazymatch rels with
+  | Some ?rels' => trakt Z bool with rel rels'
+  | None => trakt Z bool
+  end.
+
+Ltac revert_and_trakt Hs rels :=
+  lazymatch Hs with
+  | (?Hs, ?H) =>
+    revert H;
+    revert_and_trakt Hs rels
+    (* intro H *)
+  | ?H =>
+    revert H;
+    trakt_rels rels
+    (* intro H *)
+  end.
+
+
+Definition sep := True.
+
+Ltac get_hyps_upto_sep :=
+  lazymatch goal with
+  | H' : ?P |- _ =>
+    lazymatch P with
+    | sep => constr:(@None unit)
+    | _ =>
+      let T := type of P in
+      lazymatch T with
+      | Prop =>
+        let _ := match goal with _ => revert H' end in
+        let acc := get_hyps_upto_sep in
+        let _ := match goal with _ => intro H' end in
+        lazymatch acc with
+        | Some ?acc' => constr:(Some (acc', H'))
+        | None => constr:(Some H')
+        end
+      | _ =>
+        let _ := match goal with _ => revert H' end in
+        let acc := get_hyps_upto_sep in
+        let _ := match goal with _ => intro H' end in
+        acc
+      end
+    end
+  end.
+
+
+(* Goal False -> 1 = 1 -> unit -> false = true -> True. *)
+(* Proof. *)
+(*   intros H1 H2. *)
+(*   assert (H : sep) by exact I. *)
+(*   intros H3 H4. *)
+(*   let Hs := get_hyps_upto_sep in idtac Hs. *)
+(* Abort. *)
+
+
+Ltac intros_names :=
+  let H := fresh in
+  let _ := match goal with _ => assert (H : sep) by exact I; intros end in
+  let Hs := get_hyps_upto_sep in
+  let _ := match goal with _ => clear H end in
+  Hs.
+
+
+(* Goal False -> 1 = 1 -> unit -> false = true -> True. *)
+(* Proof. *)
+(*   intros H1 H2. *)
+(*   let Hs := intros_names in idtac Hs. *)
+(* Abort. *)
+
+
+Ltac post_trakt Hs :=
+  lazymatch Hs with
+  | (?Hs1, ?Hs2) =>
+    post_trakt Hs1;
+    post_trakt Hs2
+  | ?H => try (revert H; trakt_reorder_quantifiers; trakt_boolify_arrows; intro H)
+  end.
+
+Ltac trakt1 rels Hs :=
+  lazymatch Hs with
+  | Some ?Hs => revert_and_trakt Hs rels
+  | None => trakt_rels rels
+  end.
+
+
+(* Section Test. *)
+(*   Variables (A:Type) (HA:SMT_classes.CompDec A). *)
+
+(*   Goal forall (a1 a2:A), a1 = a2. *)
+(*   Proof. *)
+(*     intros a1 a2. *)
+(*     trakt Z bool with rel (@eq A, @SMT_classes.eqb_of_compdec A HA, @SMT_classes.compdec_eq_eqb A HA). *)
+(*   Abort. *)
+(* End Test. *)
+
+(* 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 H. *)
+(*   add_compdecs. *)
+(*   Focus 3. *)
+(*   (* Set Printing All. *) *)
+(*   let cs := collect_compdecs in *)
+(*   let rels := generate_rels cs in *)
+(*   trakt1 rels (Some H). *)
+(* Abort. *)
+
+
+(* Remove quantifications on CompDecs in hypotheses *)
+
+Ltac remove_compdec_hyp H :=
+  let TH := type of H in
+  match TH with
+  | forall p : SMT_classes.CompDec ?A, _ =>
+    match goal with
+    | [ p' : SMT_classes.CompDec A |- _ ] =>
+      let H1 := fresh in
+      assert (H1 := H p'); clear H; assert (H := H1); clear H1;
+      remove_compdec_hyp H
+    | _ =>
+      let c := fresh "c" in
+      assert (c : SMT_classes.CompDec A);
+      [ try (exact _)
+      | let H1 := fresh in
+        assert (H1 := H c); clear H; assert (H := H1); clear H1;
+        remove_compdec_hyp H ]
+    end
+  | _ => idtac
+  end.
+
+Ltac remove_compdec_hyps Hs :=
+  lazymatch Hs with
+  | (?Hs1, ?Hs2) =>
+    remove_compdec_hyps Hs1;
+    remove_compdec_hyps Hs2
+  | ?H => remove_compdec_hyp H
+  end.
+
+Ltac remove_compdec_hyps_option Hs :=
+  lazymatch Hs with
+  | Some ?Hs => remove_compdec_hyps Hs
+  | None => idtac
+  end.
+
+
+(* Perform all the preprocessing *)
+
+Ltac preprocess1 Hs :=
+  add_compdecs;
+  [ .. |
+    remove_compdec_hyps_option Hs;
+    let cpds := collect_compdecs in
+    let rels := generate_rels cpds in
+    trakt1 rels Hs].
+
+
+(* 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) (* /\ 0%N = 0%N *). *)
+(* Proof. *)
+(*   intros A B C HA a1 a2 b1 b2 b3 b4 c1 c2. intros. *)
+(*   assert (H1 := @List.nil_cons positive 5%positive nil). *)
+(*   preprocess1 (Some (H1, H)). *)
+(*   Show 3. *)
+(* Abort. *)
+
+Ltac preprocess2 Hs' :=
+  lazymatch Hs' with
+  | Some ?Hs' => post_trakt Hs'
+  | None => idtac
+  end.
diff --git a/src/preproc/Database_trakt.v b/src/preproc/Database_trakt.v
new file mode 100644
index 0000000..8f3ac34
--- /dev/null
+++ b/src/preproc/Database_trakt.v
@@ -0,0 +1,224 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2021                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+From Trakt Require Import Trakt.
+
+
+(* Boolean equality *)
+
+Lemma eqbool_Booleqb_embedding: forall n m : bool, n = m <-> (Bool.eqb n m) = true.
+Proof. intros n m. now rewrite Bool.eqb_true_iff. Qed.
+Trakt Add Relation (@eq bool) (Bool.eqb) (eqbool_Booleqb_embedding).
+
+
+(* Boolean relations for Z *)
+
+From Coq Require Import ZArith.
+
+
+Lemma eqZ_Zeqb_embedding: forall n m : Z, n = m <-> (Z.eqb n m) = true.
+Proof. intros n m. now rewrite Z.eqb_eq. Qed.
+Trakt Add Relation (@eq Z) (Z.eqb) (eqZ_Zeqb_embedding).
+
+Lemma ltZ_Zltb_embedding: forall n m : Z, (n < m)%Z <-> (Z.ltb n m) = true.
+Proof. intros n m. now rewrite Z.ltb_lt. Qed.
+Trakt Add Relation (@Z.lt) (Z.ltb) (ltZ_Zltb_embedding).
+
+Lemma leZ_Zleb_embedding: forall n m : Z, (n <= m)%Z <-> (Z.leb n m) = true.
+Proof. intros n m. now rewrite Z.leb_le. Qed.
+Trakt Add Relation (@Z.le) (Z.leb) (leZ_Zleb_embedding).
+
+Lemma gtZ_Zgtb_embedding: forall n m : Z, (n > m)%Z <-> (Z.gtb n m) = true.
+Proof. intros n m. rewrite Z.gtb_lt. now apply Z.gt_lt_iff. Qed.
+Trakt Add Relation (@Z.gt) (Z.gtb) (gtZ_Zgtb_embedding).
+
+Lemma geZ_Zgeb_embedding: forall n m : Z, (n >= m)%Z <-> (Z.geb n m) = true.
+Proof. intros n m. rewrite Z.geb_le. now apply Z.ge_le_iff. Qed.
+Trakt Add Relation (@Z.ge) (Z.geb) (geZ_Zgeb_embedding).
+
+Goal forall (x y : Z), ((x < y)%Z \/ x = y \/ (x > y)%Z) /\ ((x <= y)%Z \/ (x >= y)%Z).
+Proof.
+  trakt Z bool.
+Abort.
+
+
+(* Embedding for nat *)
+
+Section Relations_nat.
+
+  (* Embedding *)
+  Lemma nat_Z_FBInverseProof : forall (n : nat), n = Z.to_nat (Z.of_nat n).
+  Proof. intro n; symmetry; apply Nat2Z.id. Qed.
+
+  Lemma nat_Z_BFPartialInverseProof_bool : forall (z : Z), (0 <=? z)%Z = true ->
+                                                           Z.of_nat (Z.to_nat z) = z.
+  Proof. intros Z H; apply Z2Nat.id; apply Zle_is_le_bool; assumption. Qed.
+
+  Lemma nat_Z_ConditionProof_bool : forall (n : nat), (0 <=? Z.of_nat n)%Z = true.
+  Proof. intros n. rewrite <- Zle_is_le_bool. apply Zle_0_nat. Qed.
+
+  (* Addition *)
+  Lemma Natadd_Zadd_embedding_equality : forall (n m : nat),
+      Z.of_nat (n + m)%nat = ((Z.of_nat n) + (Z.of_nat m))%Z.
+  Proof. apply Nat2Z.inj_add. Qed.
+
+  Lemma Natsub_Zsub_embedding_equality : forall (n m : nat),
+    Z.of_nat (n - m)%nat = (if Z.leb (Z.of_nat n) (Z.of_nat m) then 0%Z else (Z.of_nat n) - (Z.of_nat m))%Z.
+  Proof. intros n m. destruct (Z.of_nat n <=? Z.of_nat m)%Z eqn:E.
+      - apply Zle_is_le_bool in E. apply Nat2Z.inj_le in E. rewrite <- Nat.sub_0_le in E.
+      rewrite E. reflexivity.
+      - apply Nat2Z.inj_sub. rewrite Z.leb_nle in E. apply Znot_le_gt in E. apply 
+      Z.gt_lt in E. apply Z.lt_le_incl in E. rewrite Nat2Z.inj_le. assumption. Qed.
+
+  (* Multiplication *)
+  Lemma Natmul_Zmul_embedding_equality : forall (n m : nat),
+      Z.of_nat (n * m)%nat = ((Z.of_nat n) * (Z.of_nat m))%Z.
+  Proof. apply Nat2Z.inj_mul. Qed.
+
+  (* Successor *)
+  Lemma S_Zadd1_embedding_equality : forall (n : nat), Z.of_nat (S n) = Z.add 1%Z (Z.of_nat n).
+  Proof. intros n.
+  rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. reflexivity. Qed.
+
+  (* Zero *)
+  Lemma zero_nat_Z_embedding_equality : Z.of_nat O = 0%Z.
+  Proof. reflexivity. Qed.
+
+  (* Equality *)
+  Lemma eq_Zeqb_embedding : forall (n m : nat),
+      n = m <-> (Z.eqb (Z.of_nat n) (Z.of_nat m)) = true.
+  Proof. intros ; split. 
+    - intros H. apply inj_eq in H. rewrite <- Z.eqb_eq in H. assumption.
+    - intros H. rewrite Z.eqb_eq in H. rewrite <- Nat2Z.inj_iff. 
+    assumption. Qed.
+
+  Lemma Nateqb_Zeqb_embedding_equality : forall (n m : nat),
+      Nat.eqb n m = (Z.eqb (Z.of_nat n) (Z.of_nat m)).
+  Proof.
+  intros n m. destruct (n =? m) eqn:E.
+  rewrite Nat.eqb_eq in E. rewrite eq_Zeqb_embedding in E. symmetry. assumption.
+  apply beq_nat_false in E. rewrite eq_Zeqb_embedding in E. destruct (Z.of_nat n =? Z.of_nat m)%Z.
+  now elim E. reflexivity. Qed.
+
+  (* Less or equal *)
+  Lemma le_Zleb_embedding : forall (n m : nat),
+      n <= m <-> (Z.leb (Z.of_nat n) (Z.of_nat m)) = true.
+  Proof. intros n m. split. 
+    - intros H. apply Zle_imp_le_bool. 
+      apply Nat2Z.inj_le. assumption.
+    - intros H. apply Zle_is_le_bool in H. apply Nat2Z.inj_le in H. assumption. Qed.
+
+  Lemma Natleb_Zleb_embedding_equality : forall (n m : nat),
+      n <=? m = (Z.leb (Z.of_nat n) (Z.of_nat m)).
+  Proof.
+  intros n m. 
+  destruct (n <=? m) eqn:E.
+  - symmetry. apply leb_complete in E. apply Nat2Z.inj_le in E. 
+apply Zle_is_le_bool. assumption.
+  - apply leb_iff_conv in E. symmetry. apply Z.leb_gt. apply inj_lt in E. assumption.
+  Qed.
+
+  (* Less than *)
+  Lemma lt_Zltb_embedding : forall (n m : nat),
+      n < m <-> (Z.ltb (Z.of_nat n) (Z.of_nat m)) = true.
+  Proof. intros n m. rewrite Nat2Z.inj_lt. apply Zlt_is_lt_bool. Qed.
+
+
+  Lemma Natltb_Zltb_embedding_equality : forall (n m : nat),
+      n <? m = (Z.ltb (Z.of_nat n) (Z.of_nat m)).
+  Proof. intros n m. destruct (n<?m) eqn: E.
+  - symmetry. apply Zlt_is_lt_bool. apply Nat.ltb_lt in E. 
+apply Nat2Z.inj_lt. assumption.
+  - symmetry. apply Z.ltb_nlt. apply Nat.ltb_nlt in E.
+unfold not. intro H.
+apply Nat2Z.inj_lt in H. unfold not in E. apply E in H. assumption. Qed.
+
+  (* Greater or equal *)
+  Lemma ge_Zgeb_embedding : forall (n m : nat),
+      n >= m <-> (Z.geb (Z.of_nat n) (Z.of_nat m)) = true.
+   Proof. intros n m. split.
+    - intro H. apply geZ_Zgeb_embedding. apply Nat2Z.inj_ge. assumption.
+    - intro H. apply geZ_Zgeb_embedding in H. apply Nat2Z.inj_ge. assumption.
+  Qed.
+
+  (* Greater than *)
+  Lemma gt_Zgtb_embedding : forall (n m : nat),
+      n > m <-> (Z.gtb (Z.of_nat n) (Z.of_nat m)) = true.
+  Proof. intros n m. split.
+    - intro H. apply Zgt_is_gt_bool. apply Nat2Z.inj_gt. assumption.
+    - intro H. apply Zgt_is_gt_bool in H. apply Nat2Z.inj_gt. assumption.
+  Qed.
+
+End Relations_nat.
+
+Trakt Add Embedding
+      (nat) (Z) (Z.of_nat) (Z.to_nat) (nat_Z_FBInverseProof) (nat_Z_BFPartialInverseProof_bool)
+      (nat_Z_ConditionProof_bool).
+
+Trakt Add Symbol (Init.Nat.add) (Z.add) (Natadd_Zadd_embedding_equality).
+Trakt Add Symbol (Init.Nat.mul) (Z.mul) (Natmul_Zmul_embedding_equality).
+Trakt Add Symbol (S) (Z.add 1%Z) (S_Zadd1_embedding_equality).
+Trakt Add Symbol (O) (0%Z) (zero_nat_Z_embedding_equality).
+Trakt Add Symbol (Nat.eqb) (Z.eqb) (Nateqb_Zeqb_embedding_equality).
+Trakt Add Symbol (Nat.leb) (Z.leb) (Natleb_Zleb_embedding_equality).
+Trakt Add Symbol (Nat.ltb) (Z.ltb) (Natltb_Zltb_embedding_equality).
+
+Trakt Add Relation (@eq nat) (Z.eqb) (eq_Zeqb_embedding).
+Trakt Add Relation (le) (Z.leb) (le_Zleb_embedding).
+Trakt Add Relation (lt) (Z.ltb) (lt_Zltb_embedding).
+Trakt Add Relation (ge) (Z.geb) (ge_Zgeb_embedding).
+Trakt Add Relation (gt) (Z.gtb) (gt_Zgtb_embedding).
+
+(* Goal 3%nat = 3%nat. *)
+(* Proof. trakt Z bool. Abort. *)
+
+(* Goal Nat.eqb 3%nat 3%nat = true. *)
+(* Proof. trakt Z bool. Abort. *)
+
+(* Goal (3+4)%nat = 7%nat. *)
+(* Proof. trakt Z bool. Abort. *)
+
+(* Goal forall (x y:nat), x <= x + y. *)
+(* Proof. trakt Z bool. Abort. *)
+
+
+(* Embedding for N (to be completed) *)
+
+Section Relations_N.
+
+  Lemma N_Z_FBInverseProof : forall (n : N), n = Z.to_N (Z.of_N n).
+  Proof. intros n ; symmetry ; apply N2Z.id. Qed.
+
+  Lemma N_Z_BFPartialInverseProof_bool : forall (z : Z), (0 <=? z)%Z = true ->
+                                                           Z.of_N (Z.to_N z) = z.
+  Proof. intros z H. induction z.
+  - reflexivity.
+  - reflexivity.
+  - assert (H1 : forall p : positive, (Z.neg p < 0)%Z) by apply Pos2Z.neg_is_neg.
+    specialize (H1 p). apply Zle_bool_imp_le in H. apply Zle_not_lt in H. 
+    unfold not in H1. apply H in H1. elim H1. Qed.
+
+  Lemma N_Z_ConditionProof_bool : forall (n : N), (0 <=? Z.of_N n)%Z = true.
+  Proof.  intros n. apply Zle_imp_le_bool. apply N2Z.is_nonneg. Qed. 
+
+End Relations_N.
+
+Trakt Add Embedding
+      (N) (Z) (Z.of_N) (Z.to_N) (N_Z_FBInverseProof) (N_Z_BFPartialInverseProof_bool)
+      (N_Z_ConditionProof_bool).
+
+
+(* This is about Z, but it fails if we put it upper in the file...?? *)
+
+(* Lemma Zneg_Zopp_embedding_equality : forall (x : positive), Zneg x = Z.opp (Zpos x).
+Admitted.
+Trakt Add Symbol (Zneg) (Z.opp) (Zneg_Zopp_embedding_equality). *)