Merge PR #9856: A 'zify' tactic as a ML plugin

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: vbgl

7 files changed, 209 insertions, 29 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index e0324b0232..b3bcb5b056 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v
index ec39209230..2a66cc9a5a 100644
--- a/test-suite/micromega/non_lin_ci.v
+++ b/test-suite/micromega/non_lin_ci.v
@@ -43,18 +43,18 @@ Proof.
 Qed.
 
 Goal
-  forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13
-  __x14 __x15 __x16 : Z)
-         (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2)
-         (H7 : 0 <= __x8)
-         (H12 : 0 <= __x14)
-         (H0 : __x8 = __x15 * __x11 + __x9)
-         (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16)
-         (H17 : __x16 <= 0)
-         (H15 : 0 <= __x9)
-         (H18 : __x9 < __x15)
-         (H16 : 0 <= __x12)
-         (H19 : __x12 < (__x10 * __x15 + __x14) * __x10)
+  forall (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
+  x14 x15 x16 : Z)
+         (H6 : x8 < x10 ^ 2 * x15 ^ 2 + 2 * x10 * x15 * x14 + x14 ^ 2)
+         (H7 : 0 <= x8)
+         (H12 : 0 <= x14)
+         (H0 : x8 = x15 * x11 + x9)
+         (H14 : x10 ^ 2 * x15 + x10 * x14 < x16)
+         (H17 : x16 <= 0)
+         (H15 : 0 <= x9)
+         (H18 : x9 < x15)
+         (H16 : 0 <= x12)
+         (H19 : x12 < (x10 * x15 + x14) * x10)
   , False.
 Proof.
   intros.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 52dc9ed2e0..354c608e23 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -24,6 +24,16 @@ Proof.
   lra.
 Qed.
 
+Goal
+  forall  (a c : R)
+         (Had : a <> a),
+    a > c.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
 (* Other (simple) examples *)
 
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
@@ -32,7 +42,6 @@ Proof.
   lra.
 Qed.
 
-
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
   intros ; lra.
diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v
index f02d93f911..a0afe99181 100644
--- a/test-suite/micromega/rsyntax.v
+++ b/test-suite/micromega/rsyntax.v
@@ -60,7 +60,6 @@ Proof.
   lia. (* exponent is a constant expr *)
 Qed.
 
-
 Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R.
 Proof.
   lra.
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 55691f553c..3d99af95ec 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -1,5 +1,63 @@
 Require Import ZArith.
 Require Import Lia.
+
+Section S.
+  Variables H1 H2 H3 H4 : True.
+
+  Lemma bug_9848 : True.
+  Proof using.
+    lia.
+  Qed.
+End S.
+
+Lemma concl_in_Type : forall   (k : nat)
+             (H : (k < 0)%nat) (F : k < 0 -> Type),
+    F H.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Lemma bug_10707 : forall
+    (T : Type)
+    (t : nat -> Type)
+    (k : nat)
+    (default : T)
+    (arr : t 0 -> T)
+    (H : (k < 0)%nat) of_nat_lt,
+ match k with
+ | 0 | _ => default
+ end = arr (of_nat_lt H).
+Proof.
+  intros.
+  lia.
+Qed.
+
+Axiom decompose_nat : nat -> nat -> nat.
+Axiom inleft : forall {P}, {m : nat & P m} -> nat.
+Axiom foo : nat.
+
+Lemma bug_7886 : forall (x x0 : nat)
+                        (e : 0 = x0 + S x)
+                        (H : decompose_nat x 0 = inleft (existT (fun m : nat => 0 = m + S x) x0 e))
+                        (x1 : nat)
+                        (e0 : 0 = x1 + S (S x))
+                        (H1 : decompose_nat (S x) 0 = inleft (existT (fun m : nat => 0 = m + S (S x)) x1 e0)),
+    False.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
+Lemma bug_8898 : forall (p : 0 < 0) (H: p = p), False.
+Proof.
+  intros p H.
+  lia.
+Qed.
+
+
+
 Open Scope Z_scope.
 
 Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
@@ -34,12 +92,12 @@ Proof.
 Qed.
 
 Lemma compact_proof : forall z,
- (z < 0) ->
- (z >= 0) ->
-  (0 >= z \/ 0 < z) -> False.
+    (z < 0) ->
+    (z >= 0) ->
+    (0 >= z \/ 0 < z) -> False.
 Proof.
- intros.
- lia.
+  intros.
+  lia.
 Qed.
 
 Lemma dummy_ex : exists (x:Z),  x = x.
@@ -74,9 +132,17 @@ Proof.
   lia.
 Qed.
 
+
+Lemma fresh1 : forall (__p1 __p2 __p3 __p5:Prop) (x y z:Z), (x = 0 /\ y = 0) /\ z = 0 -> x = 0.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
 Class Foo {x : Z} := { T : Type ; dec : T -> Z }.
 Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y 
-< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
+                                                                    < bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
 Proof.
   intros.
   lia.
@@ -98,7 +164,19 @@ Section S.
     lia.
   Qed.
 
-  End S.
+End S.
+
+Section S.
+  Variable x y: Z.
+  Variable H1 : 1 > 0 -> x = 1.
+  Variable H2 : x = y.
+
+  Goal x = y.
+  Proof using H2.
+    lia.
+  Qed.
+
+End S.
 
 (*  Bug 5073 *)
 Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
@@ -122,8 +200,50 @@ Goal forall
     (H5 : - b < r)
     (H6 : r <= 0)
     (H2 : 0 <= b),
-  b = 0 -> False.
+    b = 0 -> False.
 Proof.
   intros b q r.
   lia.
 Qed.
+
+
+Section S.
+  (* From bedrock2, used to be slow *)
+  Variables (x3 q r q2 r3 : Z)
+            (H : 2 ^ 2 <> 0 -> r3 + 3 = 2 ^ 2 * q + r)
+            (H0 : 0 < 2 ^ 2 -> 0 <= r < 2 ^ 2)
+            (H1 : 2 ^ 2 < 0 -> 2 ^ 2 < r <= 0)
+            (H2 : 2 ^ 2 = 0 -> q = 0)
+            (H3 : 2 ^ 2 = 0 -> r = 0)
+            (q0 r0 : Z)
+            (H4 : 4 <> 0 -> 0 = 4 * q0 + r0)
+            (H5 : 0 < 4 -> 0 <= r0 < 4)
+            (H6 : 4 < 0 -> 4 < r0 <= 0)
+            (H7 : 4 = 0 -> q0 = 0)
+            (H8 : 4 = 0 -> r0 = 0)
+            (q1 r1 : Z)
+            (H9 : 4 <> 0 -> q + q + (q + q) = 4 * q1 + r1)
+            (H10 : 0 < 4 -> 0 <= r1 < 4)
+            (H11 : 4 < 0 -> 4 < r1 <= 0)
+            (H12 : 4 = 0 -> q1 = 0)
+            (H13 : 4 = 0 -> r1 = 0)
+            (r2 : Z)
+            (H14 : 2 ^ 16 <> 0 ->  x3 = 2 ^ 16 * q2 + r2)
+            (H15 : 0 < 2 ^ 16 -> 0 <= r2 < 2 ^ 16)
+            (H16 : 2 ^ 16 < 0 -> 2 ^ 16 < r2 <= 0)
+            (H17 : 2 ^ 16 = 0 -> q2 = 0)
+            (H18 : 2 ^ 16 = 0 -> r2 = 0)
+            (q3 : Z)
+            (H19 : 16383 + 1 <> 0 -> q2 = (16383 + 1) * q3 + r3)
+            (H20 : 0 < 16383 + 1 -> 0 <= r3 < 16383 + 1)
+            (H21 : 16383 + 1 < 0 -> 16383 + 1 < r3 <= 0)
+            (H22 : 16383 + 1 = 0 -> q3 = 0)
+            (H23 : 16383 + 1 = 0 -> r3 = 0).
+
+  Goal r0 = r1.
+  Proof using H10 H9 H5 H4.
+    intros.
+    lia.
+  Qed.
+
+End S.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index c0ef9b392d..668be1fdbc 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,14 +1,65 @@
-Require Import micromega.MExtraction.
-Require Import RingMicromega.
-Require Import QArith.
-Require Import VarMap.
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+(* Used to generate micromega.ml *)
+
+Require Extraction.
 Require Import ZMicromega.
 Require Import QMicromega.
 Require Import RMicromega.
+Require Import VarMap.
+Require Import RingMicromega.
+Require Import NArith.
+Require Import QArith.
+
+Extract Inductive prod => "( * )" [ "(,)" ].
+Extract Inductive list => list [ "[]" "(::)" ].
+Extract Inductive bool => bool [ true false ].
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive sumor => option [ Some None ].
+(** Then, in a ternary alternative { }+{ }+{ },
+   -  leftmost choice (Inleft Left) is (Some true),
+   -  middle choice (Inleft Right) is (Some false),
+   -  rightmost choice (Inright) is (None) *)
+
+
+(** To preserve its laziness, andb is normally expanded.
+    Let's rather use the ocaml && *)
+Extract Inlined Constant andb => "(&&)".
+
+Import Reals.Rdefinitions.
+
+Extract Constant R => "int".
+Extract Constant R0 => "0".
+Extract Constant R1 => "1".
+Extract Constant Rplus => "( + )".
+Extract Constant Rmult => "( * )".
+Extract Constant Ropp  => "fun x -> - x".
+Extract Constant Rinv   => "fun x -> 1 / x".
 
+(** In order to avoid annoying build dependencies the actual
+    extraction is only performed as a test in the test suite. *)
 Recursive Extraction
-Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
-           ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           Tauto.abst_form
+           ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 62ecece792..2eac9660b4 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,8 @@ Open Scope Z_scope.
 
 (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations.
+Require  Zify.
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.