Zeq_bool -> Z.eqb

7 files changed, 38 insertions, 42 deletions

diff --git a/examples/Example.v b/examples/Example.v
index 2f3ca73..fe00931 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -53,7 +53,7 @@ Qed.
 
 
 Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
-  (negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b).
+  negb (f a =? b) || negb (P (f a)) || (P b).
 Proof.
   verit.
 Qed.
@@ -62,9 +62,9 @@ Qed.
 Goal forall b1 b2 x1 x2,
   implb
   (ifb b1
-    (ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2)))
-    (ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2))))
-  ((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)).
+    (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2))
+    (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2)))
+  ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
 Proof.
   verit.
 Qed.
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
index 7109b11..3972ecb 100644
--- a/src/Conversion_tactics.v
+++ b/src/Conversion_tactics.v
@@ -6,14 +6,6 @@ Require Import ZArith.
 (********************************************************************)
 (********************************************************************)
 
-(* SMTCoq utilise Zeq_bool *)
-Lemma Zeq_bool_Zeqb a b : Z.eqb a b = Zeq_bool a b.
-Proof.
-  case_eq (a =? b)%Z.
-  - rewrite Z.eqb_eq. intros ->. symmetry. now rewrite <- Zeq_is_eq_bool.
-  - rewrite Z.eqb_neq. intro H. case_eq (Zeq_bool a b); auto. now rewrite <- Zeq_is_eq_bool.
-Qed.
-
 (* Généralise fun x => f (g x) *)
 Ltac generalize_fun f g :=
   repeat
@@ -92,7 +84,7 @@ Ltac pos_rewriting :=
     | |-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);rewrite Zeq_bool_Zeqb
+    | |-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é *)
@@ -184,7 +176,7 @@ Ltac N_rewriting :=
     | |-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);rewrite Zeq_bool_Zeqb
+    | |-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)
   end.
 
 (* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
@@ -278,7 +270,7 @@ Ltac nat_rewriting :=
     | |-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);rewrite Zeq_bool_Zeqb
+    | |-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.
 
 (* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
diff --git a/src/Misc.v b/src/Misc.v
index 2aa6b0e..889219e 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -1008,3 +1008,9 @@ Implicit Arguments forallb2 [A B].
    coq-load-path: ((rec "." "SMTCoq"))
    End: 
 *)
+
+Lemma neg_eq_true_eq_false b : b = false <-> b <> true.
+Proof. destruct b; intuition. Qed.
+
+Lemma is_true_iff e :  e = true <-> is_true e.
+Proof. now unfold is_true. Qed.
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index a99c158..42b1314 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -302,7 +302,7 @@ Module Typ.
       Definition i_eqb (t:type) : interp t -> interp t -> bool :=
         match t with
         | Tindex i => (t_i.[i]).(te_eqb)
-        | TZ => Zeq_bool
+        | TZ => Z.eqb
         | Tbool => Bool.eqb
         | Tpositive => Peqb
         end.
@@ -311,7 +311,7 @@ Module Typ.
       Proof.
        destruct t;simpl;intros.
        symmetry;apply reflect_iff;apply te_reflect.
-       symmetry;apply Zeq_is_eq_bool.
+       apply Z.eqb_eq.
        apply Bool.eqb_true_iff.
        apply Peqb_eq.
       Qed.
@@ -321,11 +321,11 @@ Module Typ.
         intros;apply iff_reflect;symmetry;apply i_eqb_spec.
       Qed.
 
-      Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x.
-      Proof.
-        intros t x y; case_eq (i_eqb t x y); case_eq (i_eqb t y x); auto.
-        change (i_eqb t x y = true) with (is_true (i_eqb t x y)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H1; discriminate|elim H2; auto].
-        change (i_eqb t y x = true) with (is_true (i_eqb t y x)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H2; discriminate|elim H1; auto].
+     Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x.
+     Proof.
+       intros t x y; case_eq (i_eqb t x y); intro H1; symmetry;
+          [ | rewrite neg_eq_true_eq_false in *; intro H2; apply H1];
+          rewrite is_true_iff in *; now rewrite i_eqb_spec in *.
       Qed.
 
     End Interp_Equality.
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index d8e89f3..dbd3b9c 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -1006,7 +1006,8 @@ Transparent build_z_atom.
       symmetry;apply Zgt_is_gt_bool.
       destruct t0;inversion H13;clear H13;subst.
       simpl.
-      symmetry;apply (Zeq_is_eq_bool (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)).
+      apply (Z.eqb_eq (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)).
+
     Qed.
 
     Lemma build_formula_correct :
@@ -1474,7 +1475,7 @@ Transparent build_z_atom.
      case_eq (vb <=? va); intros; subst.
      apply Zle_bool_imp_le in H2.
      apply Zle_bool_imp_le in H3.
-     apply Zeq_bool_neq in H.
+     apply Z.eqb_neq in H.
      (*pour la beauté du geste!*) lia.
      rewrite H3 in H1; simpl in H1; elim diff_true_false; trivial.
      rewrite H2 in H0; simpl in H1; elim diff_true_false; trivial.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 6c76f9d..1874d5f 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -52,10 +52,7 @@ let cltb = gen_constant z_modules "ltb"
 let cleb = gen_constant z_modules "leb"
 let cgeb = gen_constant z_modules "geb"
 let cgtb = gen_constant z_modules "gtb"
-(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec
-   Z.eqb *)
-(* let ceqbZ = gen_constant z_modules "eqb" *)
-let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool"
+let ceqbZ = gen_constant z_modules "eqb" 
 
 (* Booleans *)
 let bool_modules = [["Coq";"Bool";"Bool"]]
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index af5ba36..33df78b 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -742,7 +742,7 @@ Qed.
 
 (* uf1.smt *)
 
-Goal forall a b c f p, ((Zeq_bool a c) && (Zeq_bool b c) && ((negb (Zeq_bool (f a) (f b))) || ((p a) && (negb (p b))))) = false.
+Goal forall a b c f p, ( (a =? c) && (b =? c) && ((negb (f a =?f b)) || ((p a) && (negb (p b))))) = false.
 Proof.
   verit.
 Qed.
@@ -758,7 +758,7 @@ Qed.
 
 (* uf3.smt *)
 
-Goal forall x y z f, ((Zeq_bool x y) && (Zeq_bool y z) && (negb (Zeq_bool (f x) (f z)))) = false.
+Goal forall x y z f, ((x =? y) && (y =? z) && (negb (f x =? f z))) = false.
 Proof.
   verit.
 Qed.
@@ -766,7 +766,7 @@ Qed.
 
 (* uf4.smt *)
 
-Goal forall x y z f, ((negb (Zeq_bool (f x) (f y))) && (Zeq_bool y z) && (Zeq_bool (f x) (f (f z))) && (Zeq_bool x y)) = false.
+Goal forall x y z f, ((negb (f x =? f y)) && (y =? z) && (f x =? f (f z)) && (x =? y)) = false.
 Proof.
   verit.
 Qed.
@@ -774,7 +774,7 @@ Qed.
 
 (* uf5.smt *)
 
-Goal forall a b c d e f, ((Zeq_bool a b) && (Zeq_bool b c) && (Zeq_bool c d) && (Zeq_bool c e) && (Zeq_bool e f) && (negb (Zeq_bool a f))) = false.
+Goal forall a b c d e f, ((a =? b) && (b =? c) && (c =? d) && (c =? e) && (e =? f) && (negb (a =? f))) = false.
 Proof.
   verit.
 Qed.
@@ -790,7 +790,7 @@ Qed.
 
 (* lia2.smt *)
 
-Goal forall x, implb (Zeq_bool (x - 3) 7) (x >=? 10) = true.
+Goal forall x, implb (x - 3 =? 7) (x >=? 10) = true.
 Proof.
   verit.
 Qed.
@@ -826,7 +826,7 @@ Qed.
 
 (* lia7.smt *)
 
-Goal forall x, implb (Zeq_bool (x - 3) 7) (10 <=? x) = true.
+Goal forall x, implb (x - 3 =? 7) (10 <=? x) = true.
 Proof.
   verit.
 Qed.
@@ -840,18 +840,18 @@ Qed.
 
 
 Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
-  (negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b).
+    (negb (f a =? b)) || (negb (P (f a))) || (P b).
 Proof.
   verit.
 Qed.
 
 
 Goal forall b1 b2 x1 x2,
-  implb
-  (ifb b1
-    (ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2)))
-    (ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2))))
-  ((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)).
+    implb
+      (ifb b1
+           (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2))
+           (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2)))
+      ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
 Proof.
   verit.
 Qed.
@@ -914,13 +914,13 @@ Qed.
 (* Congruence in which some premises are REFL *)
 
 Goal forall (f:Z -> Z -> Z) x y z,
-  implb (Zeq_bool x y) (Zeq_bool (f z x) (f z y)).
+    implb (x =? y) (f z x =? f z y).
 Proof.
   verit.
 Qed.
 
 Goal forall (P:Z -> Z -> bool) x y z,
-  implb (Zeq_bool x y) (implb (P z x) (P z y)).
+    implb (x =? y) (implb (P z x) (P z y)).
 Proof.
   verit.
 Qed.