fix according to review by @pi8027

5 files changed, 258 insertions, 48 deletions

diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index c00c9ecad4..80a40c4315 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -50,5 +50,6 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
 |[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
 |[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
 |[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
-|[ "Show" "Zify" "Spec"]    -> { Zify.BinOpSpec.print () ; Zify.UnOpSpec.print()}
+|[ "Show" "Zify" "Spec"] -> { (* This prints both UnOpSpec and BinOpSpec *)
+    Zify.UnOpSpec.print() }
 END
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
new file mode 100644
index 0000000000..8fd7398638
--- /dev/null
+++ b/test-suite/micromega/zify.v
@@ -0,0 +1,229 @@
+Require Import BinNums BinInt ZifyInst Zify.
+
+Definition pos := positive.
+
+Goal forall (x : pos), x = x.
+Proof.
+  intros.
+  zify_op.
+  apply (@eq_refl Z).
+Qed.
+
+Goal (1 <= Pos.to_nat 1)%nat.
+Proof.
+  zify_op.
+  apply Z.le_refl.
+Qed.
+
+Goal forall (x : positive), not (x = x) -> False.
+Proof.
+  intros. zify_op.
+  apply H.
+  apply (@eq_refl Z).
+Qed.
+
+Goal (0 <= 0)%nat.
+Proof.
+  intros.
+  zify_op.
+  apply Z.le_refl.
+Qed.
+
+
+Lemma N : forall x, (0 <= Z.of_nat x)%Z.
+Proof.
+  intros.
+  zify. exact cstr.
+Defined.
+
+Lemma N_eq : N =
+fun x : nat => let cstr : (0 <= Z.of_nat x)%Z := Znat.Nat2Z.is_nonneg x in cstr.
+Proof.
+  reflexivity.
+Qed.
+
+Goal (Z.of_nat 1 * 0 = 0)%Z.
+Proof.
+  intros.
+  zify.
+  match goal with
+  | |- (1 * 0 = 0)%Z => reflexivity
+  end.
+Qed.
+
+Lemma  C : forall p,
+  Z.pos p~1 = Z.pos p~1.
+Proof.
+  intros.
+  zify_op.
+  reflexivity.
+Defined.
+
+Lemma C_eq : C = fun p : positive =>
+let cstr : (0 < Z.pos p)%Z := Pos2Z.pos_is_pos p in eq_refl.
+Proof.
+reflexivity.
+Qed.
+
+
+Goal forall p,
+  (Z.pos p~1 = 2 * Z.pos p + 1)%Z.
+Proof.
+  intros.
+  zify_op.
+  reflexivity.
+Qed.
+
+Goal forall z,
+    (2 * z = 2 * z)%Z.
+Proof.
+  intros.
+  zify_op.
+  reflexivity.
+Qed.
+
+Goal  (-1= Z.opp 1)%Z.
+Proof.
+  intros.
+  zify_op.
+  reflexivity.
+Qed.
+
+Require Import Lia.
+
+Goal forall n n3,
+S n + n3 >= 0 + n.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Open Scope Z_scope.
+
+Goal forall p,
+    False ->
+    (Pos.to_nat p)  = 0%nat.
+Proof.
+  intros.
+  zify_op.
+  match goal with
+  | H : False |- Z.pos p = Z0 => tauto
+  end.
+Qed.
+
+Goal   forall
+    fibonacci
+    (p : positive)
+    (n : nat)
+    (b : Z)
+    (H : 0%nat = (S (Pos.to_nat p) - n)%nat)
+    (H0 : 0 < Z.pos p < b)
+    (H1 : Z.pos p < fibonacci (S n)),
+  Z.abs (Z.pos p) < Z.of_nat n.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
+
+Section S.
+  Variable digits : positive.
+  Hypothesis digits_ne_1 : digits <> 1%positive.
+
+  Lemma spec_more_than_1_digit : (1 < Z.pos digits)%Z.
+  Proof. lia. Qed.
+
+  Let digits_gt_1 := spec_more_than_1_digit.
+
+  Goal True.
+  Proof.
+    intros.
+    zify.
+    exact I.
+  Qed.
+
+End S.
+
+
+Record Bla : Type :=
+  mk
+    {
+      T : Type;
+      zero : T
+    }.
+
+Definition znat := mk nat 0%nat.
+
+Require Import ZifyClasses.
+Require Import ZifyInst.
+
+Instance Zero : CstOp (@zero znat : nat) := Op_O.
+Add CstOp Zero.
+
+
+Goal  @zero znat = 0%nat.
+  zify.
+  reflexivity.
+Qed.
+
+Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
+    (F P + 1 = 1 + F P)%positive.
+Proof.
+  intros.
+  zify_op.
+  apply Z.add_comm.
+Qed.
+
+Goal forall (x y : nat) (F : forall (P: le x y) , nat) (P : le x y),
+    (F P + 1 = 1 + F P)%nat.
+Proof.
+  intros.
+  zify_op.
+  apply Z.add_comm.
+Qed.
+
+Require Import Bool.
+
+Goal true && false = false.
+Proof.
+  lia.
+Qed.
+
+Goal forall p, p || true   = true.
+Proof.
+  lia.
+Qed.
+
+Goal forall x y, Z.eqb x y = true -> x = y.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall x, Z.leb x x = true.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall x, Z.gtb x x = false.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Require Import ZifyBool.
+
+Goal forall x y : nat, Nat.eqb x 1 = true ->
+                       Nat.eqb y 0 = true ->
+                       Nat.eqb (x + y) 1 = true.
+Proof.
+  intros x y.
+  lia.
+Qed.
+
+Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
+Proof.
+  intros. lia.
+Qed.
diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v
index 90ed0ab9d2..1bb016da9a 100644
--- a/theories/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
@@ -1,7 +1,7 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
 (*         *     GNU Lesser General Public License Version 2.1          *)
@@ -10,7 +10,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria)                                       *)
 (*                                                                      *)
 (************************************************************************)
 
diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v
index 09b44f145d..7e2694a519 100644
--- a/theories/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
@@ -1,7 +1,7 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
 (*         *     GNU Lesser General Public License Version 2.1          *)
@@ -10,7 +10,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria)                                       *)
 (*                                                                      *)
 (************************************************************************)
 
diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index 2d2b137117..6c34040155 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -21,18 +21,15 @@ Add InjTyp Inj_bool_bool.
 (** Boolean operators *)
 
 Instance Op_andb : BinOp andb :=
-  { TBOp := andb ;
-    TBOpInj := ltac: (reflexivity)}.
+  { TBOp := andb ; TBOpInj := fun _ _  => eq_refl}.
 Add BinOp Op_andb.
 
 Instance Op_orb : BinOp orb :=
-  { TBOp := orb ;
-    TBOpInj := ltac:(reflexivity)}.
+  { TBOp := orb ; TBOpInj := fun _ _ => eq_refl}.
 Add BinOp Op_orb.
 
 Instance Op_implb : BinOp implb :=
-  { TBOp := implb;
-    TBOpInj := ltac:(reflexivity) }.
+  { TBOp := implb; TBOpInj := fun _ _ => eq_refl }.
 Add BinOp Op_implb.
 
 Definition xorb_eq : forall b1 b2,
@@ -42,16 +39,15 @@ Proof.
 Qed.
 
 Instance Op_xorb : BinOp xorb :=
-  { TBOp := fun x y => andb (orb x y) (negb (eqb x y));
-    TBOpInj := xorb_eq }.
+  { TBOp := fun x y => andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }.
 Add BinOp Op_xorb.
 
 Instance Op_eqb : BinOp eqb :=
-  { TBOp := eqb; TBOpInj := ltac:(reflexivity) }.
+  { TBOp := eqb; TBOpInj := fun _ _ => eq_refl }.
 Add BinOp Op_eqb.
 
 Instance Op_negb : UnOp negb :=
-  { TUOp := negb ; TUOpInj := ltac:(reflexivity)}.
+  { TUOp := negb ; TUOpInj := fun _ => eq_refl}.
 Add UnOp Op_negb.
 
 Instance Op_eq_bool : BinRel (@eq bool) :=
@@ -69,31 +65,23 @@ Add CstOp Op_false.
 (** Comparison over Z *)
 
 Instance Op_Zeqb : BinOp Z.eqb :=
-  { TBOp := Z.eqb ; TBOpInj := ltac:(reflexivity)}.
+  { TBOp := Z.eqb ; TBOpInj := fun _ _ => eq_refl }.
 Add BinOp Op_Zeqb.
 
 Instance Op_Zleb : BinOp Z.leb :=
-  { TBOp := Z.leb;
-    TBOpInj :=  ltac: (reflexivity);
-  }.
+  { TBOp := Z.leb; TBOpInj :=  fun _ _ => eq_refl }.
 Add BinOp Op_Zleb.
 
 Instance Op_Zgeb : BinOp Z.geb :=
-  { TBOp := Z.geb;
-    TBOpInj := ltac:(reflexivity)
-  }.
+  { TBOp := Z.geb; TBOpInj := fun _ _ => eq_refl }.
 Add BinOp Op_Zgeb.
 
 Instance Op_Zltb : BinOp Z.ltb :=
-  { TBOp := Z.ltb ;
-    TBOpInj := ltac:(reflexivity)
-  }.
+  { TBOp := Z.ltb ; TBOpInj := fun _ _ => eq_refl }.
 Add BinOp Op_Zltb.
 
 Instance Op_Zgtb : BinOp Z.gtb :=
-  { TBOp := Z.gtb;
-    TBOpInj := ltac:(reflexivity)
-  }.
+  { TBOp := Z.gtb; TBOpInj := fun _ _  => eq_refl }.
 Add BinOp Op_Zgtb.
 
 (** Comparison over nat *)
@@ -129,36 +117,28 @@ Proof.
 Qed.
 
 Instance Op_nat_eqb : BinOp Nat.eqb :=
-   { TBOp := Z.eqb;
-     TBOpInj := Z_of_nat_eqb_iff }.
+  { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }.
 Add BinOp Op_nat_eqb.
 
 Instance Op_nat_leb : BinOp Nat.leb :=
-  { TBOp := Z.leb ;
-    TBOpInj := Z_of_nat_leb_iff
-  }.
+  { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }.
 Add BinOp Op_nat_leb.
 
 Instance Op_nat_ltb : BinOp Nat.ltb :=
-  { TBOp := Z.ltb;
-    TBOpInj := Z_of_nat_ltb_iff
-  }.
+  { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }.
 Add BinOp Op_nat_ltb.
 
 Lemma b2n_b2z :  forall x,  Z.of_nat (Nat.b2n x) = Z.b2z x.
 Proof.
-  intro.
-  destruct x ; reflexivity.
+  intro. destruct x ; reflexivity.
 Qed.
 
 Instance Op_b2n : UnOp Nat.b2n :=
-  { TUOp := Z.b2z;
-    TUOpInj := b2n_b2z }.
+  { TUOp := Z.b2z; TUOpInj := b2n_b2z }.
 Add UnOp Op_b2n.
 
 Instance Op_b2z : UnOp Z.b2z :=
-  { TUOp := Z.b2z;
-    TUOpInj := ltac:(reflexivity) }.
+  { TUOp := Z.b2z; TUOpInj := fun _ => eq_refl }.
 Add UnOp Op_b2z.
 
 Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0).
@@ -167,15 +147,15 @@ Proof.
 Qed.
 
 Instance b2zSpec : UnOpSpec Z.b2z :=
-  {| UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0);
-     USpec := b2z_spec
-  |}.
+  { UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0);
+    USpec := b2z_spec
+  }.
 Add UnOpSpec b2zSpec.
 
 Ltac elim_bool_cstr :=
   repeat match goal with
          | C : ?B = true \/ ?B = false |- _ =>
-           destruct C ; subst
+           destruct C as [C|C]; rewrite C in *
          end.
 
 Ltac Zify.zify_post_hook ::= elim_bool_cstr.