conversion tactics: with a functor

1 files changed, 274 insertions, 240 deletions

diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
index 3972ecb..515dd47 100644
--- a/src/Conversion_tactics.v
+++ b/src/Conversion_tactics.v
@@ -1,10 +1,58 @@
 Require Import ZArith.
 
-(********************************************************************)
-(********************************************************************)
-(* Ces composants sont communs à toutes les tactiques de conversion *)
-(********************************************************************)
-(********************************************************************)
+(* Ce module représente la structure que l'on souhaite convertir vers Z *)
+Module Type convert_type.
+
+(* Le type que l'on souhaite convertir *)
+Parameter T : Type.
+
+(* Les conversion dans les deux sens *)
+Parameter Z2T : Z -> T.
+Parameter T2Z : T -> Z.
+(* T2Z est une injection *)
+Axiom T2Z_id : forall x : T, Z2T (T2Z x) = x.
+
+(* Une propriété décrivant les éléments de Z qui viennent d'éléments de T.
+   Par exemple, pour nat il s'agit de (0 <=? z)%Z *)
+Parameter inT : Z -> bool.
+(* L'image de l'injection satisfait cette propriété *)
+Axiom T2Z_pres : forall x, inT (T2Z x) = true.
+
+(* Addition *)
+Parameter add : T -> T -> T.
+(* Pour des éléments venant de T, l'addition commute avec Z2T *)
+Axiom add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y).
+(* Pour des éléments venant de T, l'addition vient de T *)
+Axiom add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true.
+
+(* Multiplication *)
+Parameter mul : T -> T -> T.
+(* Pour des éléments venant de T, la multiplication commute avec Z2T *)
+Axiom mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y).
+(* Pour des éléments venant de T, la multiplication vient de T *)
+Axiom mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true.
+
+(* <= *)
+Parameter leb : T -> T -> bool.
+(* Pour des éléments venant de T, <= commute avec Z2T *)
+Axiom leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y).
+
+(* < *)
+Parameter ltb : T -> T -> bool.
+(* Pour des éléments venant de T, < commute avec Z2T *)
+Axiom ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y).
+
+(* = *)
+Parameter eqb : T -> T -> bool.
+(* Pour des éléments venant de T, = commute avec Z2T *)
+Axiom eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y).
+
+End convert_type.
+
+(* Ce foncteur construit une tactique de conversion à partir d'un module du type ci-dessus *)
+Module convert (M : convert_type).
+
+Import M.
 
 (* Généralise fun x => f (g x) *)
 Ltac generalize_fun f g :=
@@ -21,283 +69,269 @@ intros a b H.
 destruct a; destruct b; try reflexivity; discriminate.
 Qed.
 
-(****************************)
-(****************************)
-(* Conversion de pos vers Z *)
-(****************************)
-(****************************)
+Ltac get_head x := lazymatch x with ?x _ => get_head x | _ => x end.
 
-Definition Pos2Z := Zpos.
+(* inverse_tactic tactic réussit là où tactic échoue et inversement *)
+Ltac inverse_tactic tactic := try (tactic; fail 1).
 
-Definition Z2Pos (z : Z) :=
-  match z with
-    | 0%Z => 1%positive
-    | Zpos p => p
-    | Zneg _ => 1%positive
-  end.
+Ltac constr_neq t u := inverse_tactic ltac:(constr_eq t u).
 
-Lemma Pos2Z_id : forall (p : positive), Z2Pos (Pos2Z p) = p.
-Proof. reflexivity. Qed.
+(* is_not_constructor T sym échoue si et seulement si sym est un symbole de constructeur de U *)
+Ltac is_not_constructor T sym :=
+assert (T -> True) 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).
 
-(* Remplace tous les sous-termes p de type positive par Z2Pos (Pos2Z p) *)
-Ltac pos_converting :=
-  (* On crée une variable fraîche de type positive *)
-  let var := fresh "var" in
-  pose proof xH as var;
+(* is_not_constructor U sym réussit si et seulement si sym est un symbole de constructeur de U *)
+Ltac is_constructor U sym := inverse_tactic ltac:(is_not_constructor U sym).
+
+(* Remplace tous les sous-termes x de type T par Z2T (T2Z p) *)
+Ltac converting :=
   (* Coeur de la tactique *)
   repeat
     match goal with
-    (* On capture chaque sous-terme p avec son contexte, i.e. le but est C[p] *)
-    | |- context C[?p]  =>
-      (* Si p est de type positive *)
-      lazymatch type of p with
-      | positive =>
-        lazymatch p with
-        (* Si p est de la forme Z2Pos (Pos2Z _) on abandonne le match car p est déjà réécrit *)
-        | Z2Pos (Pos2Z _) => fail
+    (* On capture chaque sous-terme x avec son contexte, i.e. le but est C[x] *)
+    | |- appcontext C[?x]  =>
+      (* Si x est de type T *)
+      let U := type of x in
+      lazymatch eval fold T in U with
+      | T =>
+        lazymatch x with
+        (* Si x est de la forme Z2T (T2Z _) on abandonne le match car x est déjà réécrit *)
+        | Z2T (T2Z _) => fail
         (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
-        | Pos.add _ _ => fail
-        | Pos.mul _ _ => fail
+        | add _ _ => fail
+        | mul _ _ => fail
         | _ =>
-          (* Sinon, on analyse la formule obtenue en remplaçant p par notre variable fraîche dans le but *)
+          (* On crée une variable fraîche de type T *)
+          let var := fresh in
+          pose proof x as var;
+          (* Sinon, on analyse la formule obtenue en remplaçant x par notre variable fraîche dans le but *)
           lazymatch context C[var] with
-          (* Si elle contient le terme Z2Pos (Pos2Z var), cela signifie que le contexte C[]
-             est de la forme C'[Z2Pos (Pos2Z [])] et donc on abandonne le match car p est déjà réécrit *)
-          | context [Z2Pos (Pos2Z var)] => fail
-          (* Idem: si le contexte contient xO ou xI, c'est qu'on est à l'intérieur d'une constante *)
-          | context [xO var] => fail
-          | context [xI var] => fail
-          (* Sinon on réécrit *)
-          | _ => replace p with (Z2Pos (Pos2Z p)) by apply Pos2Z_id
-          end
+          (* Si elle contient le terme Z2T (T2Z var), cela signifie que le contexte C[]
+             est de la forme C'[Z2T (T2Z [])] et donc on abandonne le match car x est déjà réécrit *)
+          | appcontext [Z2T (T2Z var)] => fail
+          (* Idem: si le contexte contient un constructeur de Z, c'est qu'on est à l'intérieur d'une constante *)
+          | appcontext [Zpos var] => fail
+          | appcontext [Zneg var] => fail
+          | appcontext [?h var] =>
+            (* Idem: si le contexte contient un constructeur de T et que x commence par un
+               constructeur de T, c'est qu'on est à l'intérieur d'une constante *)
+            let h := get_head h in
+            let hx := get_head x in
+            try (is_constructor T h; is_constructor T hx; fail 1);
+            (* Sinon, on réécrit *)
+            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;
+          (* On efface notre variable fraîche *)
+          clear var
         end
       end
-    end;
-  (* Finalement, on efface notre variable fraîche *)
-  clear var.
+    end.
+
+(* Résoud les hypothèses inT lors de la réécriture des opérations *)
+Ltac solve_inT := repeat (try apply add_pres; try apply mul_pres; try apply T2Z_pres); reflexivity.
 
-(* Réécrit les opérations et relations de positive vers Z *)
-Ltac pos_rewriting :=
+(* Réécrit les opérations et relations de T vers Z *)
+Ltac rewriting :=
   repeat
   match goal with
-    | |-context [Pos.add (Z2Pos ?X) (Z2Pos ?Y) ] =>  change (Pos.add (Z2Pos X) (Z2Pos Y)) with (Z2Pos (X + Y))
-    | |-context [Pos.mul (Z2Pos ?X) (Z2Pos ?Y) ] =>  change (Pos.mul (Z2Pos X) (Z2Pos Y)) with (Z2Pos (X * Y))
-    | |-context [Pos.ltb (Z2Pos ?X) (Z2Pos ?Y) ] =>  change (Pos.ltb (Z2Pos X) (Z2Pos Y)) with (Z.ltb X Y)
-    | |-context [Pos.leb (Z2Pos ?X) (Z2Pos ?Y) ] =>  change (Pos.leb (Z2Pos X) (Z2Pos Y)) with (Z.leb X Y)
-    | |-context [Pos.eqb (Z2Pos ?X) (Z2Pos ?Y) ] =>  change (Pos.eqb (Z2Pos X) (Z2Pos Y)) with (Z.eqb X Y)
-  end.
-
-(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
-Lemma pos_is_ltb : forall p : positive, Z.ltb 0 (Pos2Z p) = true.
-Proof. reflexivity. Qed.
-
-(* Réussit si f est un symbole de fonction non interprété *)
-Ltac pos_is_uninterp_fun f :=
-  lazymatch f with
-    | xI => fail
-    | xO => fail
-    | _ => idtac
+    | |- context [add (Z2T ?X) (Z2T ?Y)] => replace (add (Z2T X) (Z2T Y)) with (Z2T (X + Y)) by (rewrite add_morph; solve_inT)
+    | |- context [mul (Z2T ?X) (Z2T ?Y)] => replace (mul (Z2T X) (Z2T Y)) with (Z2T (X * Y)) by (rewrite mul_morph; solve_inT)
+    | |- context [ltb (Z2T ?X) (Z2T ?Y)] => replace (ltb (Z2T X) (Z2T Y)) with (Z.ltb X Y) by (rewrite ltb_morph; solve_inT)
+    | |- context [leb (Z2T ?X) (Z2T ?Y)] => replace (leb (Z2T X) (Z2T Y)) with (Z.leb X Y) by (rewrite leb_morph; solve_inT)
+    | |- context [eqb (Z2T ?X) (Z2T ?Y)] => replace (eqb (Z2T X) (Z2T Y)) with (Z.eqb X Y) by (rewrite eqb_morph; solve_inT)
   end.
 
 (* Remplace les symbole de fonction et de variables par des versions dans Z
    et ajoute les hypothèses de positivité *)
-Ltac pos_renaming :=
+Ltac renaming :=
   repeat
   match goal with
-    | |-context [Pos2Z ?X] => is_var X; generalize (pos_is_ltb X); apply implb_impl; generalize (Pos2Z X); clear X; intro X
-    | |-context [?X (Z2Pos ?Y)] => pos_is_uninterp_fun X; generalize_fun X Z2Pos; clear X; intro X
-    | |-context [Pos2Z (?X ?Y)] => pos_is_uninterp_fun X; generalize_fun Pos2Z X; clear X; intro X
-  end;
-  unfold Pos2Z.
+    | |-context [T2Z ?X] => is_var X; generalize (T2Z_pres X); apply implb_impl; generalize (T2Z X); clear X; intro X
+    | |-context [?X (Z2T ?Y)] => try (is_constructor T X; fail 1); generalize_fun X Z2T; clear X; intro X
+    | |-context [T2Z (?X ?Y)] => try (is_constructor T X; fail 1); generalize_fun T2Z X; clear X; intro X
+  end.
 
 (* La tactique complète *)
-Ltac pos_convert := intros; pos_converting; pos_rewriting; pos_renaming.
-
-(**************************)
-(**************************)
-(* Conversion de N vers Z *)
-(**************************)
-(**************************)
-
-Definition N2Z := Z.of_N.
-Definition Z2N := Z.to_N.
-
-(* Remplace tous les sous-termes n de type N par Z2N (N2Z n) *)
-Ltac N_converting :=
-  (* On crée une variable fraîche de type N *)
-  let var := fresh "var" in
-  pose proof N0 as var;
-  (* Coeur de la tactique *)
-  repeat
-    match goal with
-    (* On capture chaque sous-terme n avec son contexte, i.e. le but est C[n] *)
-    | |- context C[?n]  =>
-      (* Si n est de type N *)
-      lazymatch type of n with
-      | N =>
-        lazymatch n with
-        (* Si n est de la forme Z2N (N2Z _) on abandonne le match car n est déjà réécrit *)
-        | Z2N (N2Z _) => fail
-        (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
-        | N.add _ _ => fail
-        | N.mul _ _ => fail
-        | _ =>
-          (* Sinon, on analyse la formule obtenue en remplaçant n par notre variable fraîche dans le but *)
-          lazymatch context C[var] with
-          (* Si elle contient le terme Z2N (N2Z var), cela signifie que le contexte C[]
-             est de la forme C'[Z2N (N2Z [])] et donc on abandonne le match car n est déjà réécrit *)
-          | context [Z2N (N2Z var)] => fail
-          (* Sinon on réécrit *)
-          | _ => replace n with (Z2N (N2Z n)) by apply N2Z.id
-          end
-        end
-      end
-    end;
-  (* Finalement, on efface notre variable fraîche *)
-  clear var.
-
-(* Résoud les hypothèses de positivité lors de la réécriture des opérations *)
-Ltac N_solve_pos := repeat (try apply Z.add_nonneg_nonneg; try apply Z.mul_nonneg_nonneg; try apply N2Z.is_nonneg).
+Ltac convert :=
+fold T add mul ltb leb eqb;
+intros;
+converting;
+rewriting;
+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.
 
-Lemma N_inj_leb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.leb x y = N.leb (Z2N x) (Z2N y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.leb_le; rewrite Z.leb_le; apply Z2N.inj_le; assumption. Qed.
+End convert.
 
-Lemma N_inj_ltb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.ltb x y = N.ltb (Z2N x) (Z2N y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.ltb_lt; rewrite Z.ltb_lt; apply Z2N.inj_lt; assumption. Qed.
+Module pos_convert_type <: convert_type.
 
-Lemma N_inj_eqb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.eqb x y = N.eqb (Z2N x) (Z2N y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.eqb_eq; rewrite Z.eqb_eq; symmetry; apply Z2N.inj_iff; assumption. Qed.
+Definition T : Type := positive.
 
-(* Réécrit les opérations et relations de positive vers Z *)
-Ltac N_rewriting :=
-  repeat
-  match goal with
-    | |-context [N.add (Z2N ?X) (Z2N ?Y) ] =>  replace (N.add (Z2N X) (Z2N Y)) with (Z2N (X + Y)) by (apply Z2N.inj_add; N_solve_pos)
-    | |-context [N.mul (Z2N ?X) (Z2N ?Y) ] =>  replace (N.mul (Z2N X) (Z2N Y)) with (Z2N (X * Y)) by (apply Z2N.inj_mul; N_solve_pos)
-    | |-context [N.ltb (Z2N ?X) (Z2N ?Y) ] =>  replace (N.ltb (Z2N X) (Z2N Y)) with (Z.ltb X Y) by (apply N_inj_ltb; N_solve_pos)
-    | |-context [N.leb (Z2N ?X) (Z2N ?Y) ] =>  replace (N.leb (Z2N X) (Z2N Y)) with (Z.leb X Y) by (apply N_inj_leb; N_solve_pos)
-    | |-context [N.eqb (Z2N ?X) (Z2N ?Y) ] =>  replace (N.eqb (Z2N X) (Z2N Y)) with (Z.eqb X Y) by (apply N_inj_eqb; N_solve_pos)
+Definition Z2T : Z -> T := fun z =>
+  match z with
+    | 0%Z => 1%positive
+    | Zpos p => p
+    | Zneg _ => 1%positive
   end.
 
-(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
-Lemma N_is_leb : forall n : N, Z.leb 0 (N2Z n) = true.
-Proof. intro; apply Zle_imp_le_bool; apply N2Z.is_nonneg. Qed.
+Definition T2Z : T -> Z := Zpos.
+Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. reflexivity. Qed.
 
-(* Réussit si f est un symbole de fonction non interprété *)
-Ltac N_is_uninterp_fun f :=
-  lazymatch f with
-    | Npos => fail
-    | _ => idtac
-  end.
+Definition inT : Z -> bool := fun z => Z.ltb 0 z.
+Lemma T2Z_pres : forall x, inT (T2Z x) = true. reflexivity. Qed.
 
-(* Remplace les symbole de fonction et de variables par des versions dans Z
-   et ajoute les hypothèses de positivité *)
-Ltac N_renaming :=
-  repeat
-  match goal with
-    | |-context [N2Z ?X] => is_var X; generalize (N_is_leb X); apply implb_impl; generalize (N2Z X); clear X; intro X
-    | |-context [?X (Z2N ?Y)] => N_is_uninterp_fun X; generalize_fun X Z2N; clear X; intro X
-    | |-context [N2Z (?X ?Y)] => N_is_uninterp_fun X; generalize_fun N2Z X; clear X; intro X
-  end;
-  unfold N2Z; simpl.
+Definition add : T -> T -> T := Pos.add.
+Lemma add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-(* La tactique complète *)
-Ltac N_convert := intros; N_converting; N_rewriting; N_renaming.
+Definition mul : T -> T -> T := Pos.mul.
+Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-(****************************)
-(****************************)
-(* Conversion de nat vers Z *)
-(****************************)
-(****************************)
+Definition leb : T -> T -> bool := Pos.leb.
+Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-(* Nécessaire dans native-coq *)
-Require Import NPeano.
+Definition ltb : T -> T -> bool := Pos.ltb.
+Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-Definition Nat2Z := Z.of_nat.
-Definition Z2Nat := Z.to_nat.
+Definition eqb : T -> T -> bool := Pos.eqb.
+Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-(* Remplace tous les sous-termes n de type nat par Z2Nat (Nat2Z n) *)
-Ltac nat_converting :=
-  (* On crée une variable fraîche de type nat *)
-  let var := fresh "var" in
-  pose proof O as var;
-  (* Coeur de la tactique *)
-  repeat
-    match goal with
-    (* On capture chaque sous-terme n avec son contexte, i.e. le but est C[n] *)
-    | |- context C[?n]  =>
-      (* Si n est de type nat *)
-      lazymatch type of n with
-      | nat =>
-        lazymatch n with
-        (* Si n est de la forme Z2Nat (Nat2Z _) on abandonne le match car n est déjà réécrit *)
-        | Z2Nat (Nat2Z _) => fail
-        (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
-        | Nat.add _ _ => fail
-        | Nat.mul _ _ => fail
-        | _ =>
-          (* Sinon, on analyse la formule obtenue en remplaçant n par notre variable fraîche dans le but *)
-          lazymatch context C[var] with
-          (* Si elle contient le terme Z2Nat (Nat2Z var), cela signifie que le contexte C[]
-             est de la forme C'[Z2Nat (Nat2Z [])] et donc on abandonne le match car n est déjà réécrit *)
-          | context [Z2Nat (Nat2Z var)] => fail
-          (* Sinon on réécrit *)
-          | _ => replace n with (Z2Nat (Nat2Z n)) by apply Nat2Z.id
-          end
-        end
-      end
-    end;
-  (* Finalement, on efface notre variable fraîche *)
-  clear var.
+End pos_convert_type.
 
-(* Résoud les hypothèses de positivité lors de la réécriture des opérations *)
-Ltac nat_solve_pos := repeat (try apply Z.add_nonneg_nonneg; try apply Z.mul_nonneg_nonneg; try apply Nat2Z.is_nonneg).
+Module pos_convert_mod := convert pos_convert_type.
 
-Lemma nat_inj_leb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.leb x y = Nat.leb (Z2Nat x) (Z2Nat y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.leb_le; rewrite Z.leb_le; apply Z2Nat.inj_le; assumption. Qed.
+Ltac pos_convert := pos_convert_mod.convert.
 
-Lemma nat_inj_ltb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.ltb x y = Nat.ltb (Z2Nat x) (Z2Nat y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.ltb_lt; rewrite Z.ltb_lt; apply Z2Nat.inj_lt; assumption. Qed.
+Module N_convert_type <: convert_type.
 
-Lemma nat_inj_eqb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.eqb x y = Nat.eqb (Z2Nat x) (Z2Nat y).
-Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.eqb_eq; rewrite Z.eqb_eq; symmetry; apply Z2Nat.inj_iff; assumption. Qed.
+Definition T : Type := N.
 
-(* Réécrit les opérations et relations de positive vers Z *)
-Ltac nat_rewriting :=
-  repeat
-  match goal with
-    | |-context [Nat.add (Z2Nat ?X) (Z2Nat ?Y) ] =>  replace (Nat.add (Z2Nat X) (Z2Nat Y)) with (Z2Nat (X + Y)) by (apply Z2Nat.inj_add; nat_solve_pos)
-    | |-context [Nat.mul (Z2Nat ?X) (Z2Nat ?Y) ] =>  replace (Nat.mul (Z2Nat X) (Z2Nat Y)) with (Z2Nat (X * Y)) by (apply Z2Nat.inj_mul; nat_solve_pos)
-    | |-context [Nat.ltb (Z2Nat ?X) (Z2Nat ?Y) ] =>  replace (Nat.ltb (Z2Nat X) (Z2Nat Y)) with (Z.ltb X Y) by (apply nat_inj_ltb; nat_solve_pos)
-    | |-context [Nat.leb (Z2Nat ?X) (Z2Nat ?Y) ] =>  replace (Nat.leb (Z2Nat X) (Z2Nat Y)) with (Z.leb X Y) by (apply nat_inj_leb; nat_solve_pos)
-    | |-context [Nat.eqb (Z2Nat ?X) (Z2Nat ?Y) ] =>  replace (Nat.eqb (Z2Nat X) (Z2Nat Y)) with (Z.eqb X Y) by (apply nat_inj_eqb; nat_solve_pos)
-  end.
+Definition Z2T : Z -> T := Z.to_N.
 
-(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
-Lemma nat_is_leb : forall n : nat, Z.leb 0 (Nat2Z n) = true.
-Proof. intro; apply Zle_imp_le_bool; apply Nat2Z.is_nonneg. Qed.
+Definition T2Z : T -> Z := Z.of_N.
+Lemma T2Z_id : forall x : T, Z2T (T2Z x) = x. exact N2Z.id. Qed.
 
-(* Réussit si f est un symbole de fonction non interprété *)
-Ltac nat_is_uninterp_fun f :=
-  lazymatch f with
-    | O => fail
-    | S => fail
-    | _ => idtac
-  end.
+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.
 
-(* Remplace les symbole de fonction et de variables par des versions dans Z
-   et ajoute les hypothèses de positivité *)
-Ltac nat_renaming :=
-  repeat
-  match goal with
-    | |-context [Nat2Z ?X] => is_var X; generalize (nat_is_leb X); apply implb_impl; generalize (Nat2Z X); clear X; intro X
-    | |-context [?X (Z2Nat ?Y)] => nat_is_uninterp_fun X; generalize_fun X Z2Nat; clear X; intro X
-    | |-context [Nat2Z (?X ?Y)] => nat_is_uninterp_fun X; generalize_fun Nat2Z X; clear X; intro X
-  end;
-  unfold Nat2Z; simpl.
+Definition add : T -> T -> T := N.add.
+Lemma add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
 
-(* La tactique complète *)
-(* Les "fold" sont nécessaires car dans les anciennes versions de Coq
-   les notations +, *, <? et <=? se réfèrent à plus, mult, ltb et leb
-   et les Nat._ sont définis à partir de plus, mult, ltb et leb. *)
-Ltac nat_convert := fold Nat.add; fold Nat.mul; fold Nat.ltb; fold Nat.leb; fold Nat.eqb; intros; nat_converting; nat_rewriting; nat_renaming.
+Definition mul : T -> T -> T := N.mul.
+Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+Definition leb : T -> T -> bool := N.leb.
+Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+Definition ltb : T -> T -> bool := N.ltb.
+Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+Definition eqb : T -> T -> bool := N.eqb.
+Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+End N_convert_type.
+
+Module N_convert_mod := convert N_convert_type.
+
+Ltac N_convert := N_convert_mod.convert.
+
+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 add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y).
+intros x y; destruct x, y; try discriminate; try reflexivity.
+intros; apply Nat.add_0_r.
+unfold inT; rewrite 2 Z.leb_le.
+symmetry; apply Z2Nat.inj_add; assumption.
+Qed.
+Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+Definition mul : T -> T -> T := Nat.mul.
+Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y).
+intros x y; destruct x, y; try discriminate; try reflexivity.
+intros; apply Nat.mul_0_r.
+unfold inT; rewrite 2 Z.leb_le.
+symmetry; apply Z2Nat.inj_mul; assumption.
+Qed.
+Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true.
+intros x y; destruct x, y; try discriminate; reflexivity. Qed.
+
+Definition leb : T -> T -> bool := Nat.leb.
+Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; try reflexivity.
+intros H1 H2; clear H1 H2; change (Zpos p <=? 0)%Z with false; unfold Z2T, leb; symmetry.
+apply Bool.not_true_is_false; rewrite Nat.leb_le.
+apply lt_not_le; apply Pos2Nat.is_pos.
+intros H1 H2; unfold Z2T, leb; apply Bool.eq_true_iff_eq.
+rewrite Z.leb_le, Nat.leb_le, Z2Nat.inj_le; try reflexivity; apply Zle_0_pos.
+Qed.
+
+Definition ltb : T -> T -> bool := Nat.ltb.
+Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; try reflexivity.
+intros H1 H2; clear H1 H2; change (0 <? Zpos p)%Z with true.
+unfold Z2T, ltb; symmetry.
+rewrite Nat.ltb_lt, <- Z2Nat.inj_lt; try rewrite <- Z.leb_le; reflexivity.
+intros H1 H2; clear H1 H2; unfold Z2T, ltb.
+apply Bool.eq_true_iff_eq.
+rewrite Z.ltb_lt, Nat.ltb_lt.
+rewrite Z2Nat.inj_lt; try reflexivity; apply Zle_0_pos.
+Qed.
+
+Definition eqb : T -> T -> bool := Nat.eqb.
+Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y).
+intros x y; destruct x, y; try discriminate; try reflexivity; unfold inT, Z2T, eqb.
+intros H1 H2; clear H1 H2; change (0 =? Zpos p)%Z with false; symmetry.
+rewrite Nat.eqb_neq, Z2Nat.inj_iff; discriminate.
+intros H1 H2; clear H1 H2; change (Zpos p =? 0)%Z with false; symmetry.
+rewrite Nat.eqb_neq, Z2Nat.inj_iff; discriminate.
+intros H1 H2; clear H1 H2; apply Bool.eq_true_iff_eq.
+rewrite Z.eqb_eq, Nat.eqb_eq, Z2Nat.inj_iff; try reflexivity; apply Zle_0_pos.
+Qed.
+
+End nat_convert_type.
+
+Module nat_convert_mod := convert nat_convert_type.
+
+Ltac nat_convert := fold Nat.add Nat.mul Nat.leb Nat.ltb Nat.eqb; nat_convert_mod.convert.