Re-implementation of zify

The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress.  If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.

This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.

The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.)  efficiency impact.

There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite

1 files changed, 90 insertions, 0 deletions

diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v
new file mode 100644
index 0000000000..57d812b0fd
--- /dev/null
+++ b/plugins/micromega/Zify.v
@@ -0,0 +1,90 @@
+(************************************************************************)
+(*         *   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)           *)
+(*   \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)         *)
+(************************************************************************)
+
+Require Import ZifyClasses.
+Require Export ZifyInst.
+Require Import InitialRing.
+
+(** From PreOmega *)
+
+(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *)
+
+Ltac zify_unop_core t thm a :=
+ (* Let's introduce the specification theorem for t *)
+ pose proof (thm a);
+ (* Then we replace (t a) everywhere with a fresh variable *)
+ let z := fresh "z" in set (z:=t a) in *; clearbody z.
+
+Ltac zify_unop_var_or_term t thm a :=
+ (* If a is a variable, no need for aliasing *)
+ let za := fresh "z" in
+ (rename a into za; rename za into a; zify_unop_core t thm a) ||
+ (* Otherwise, a is a complex term: we alias it. *)
+ (remember a as za; zify_unop_core t thm za).
+
+Ltac zify_unop t thm a :=
+ (* If a is a scalar, we can simply reduce the unop. *)
+ (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *)
+ let isz := isZcst a in
+ match isz with
+  | true =>
+    let u := eval compute in (t a) in
+    change (t a) with u in *
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_unop_nored t thm a :=
+ (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *)
+ let isz := isZcst a in
+ match isz with
+  | true => zify_unop_core t thm a
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_binop t thm a b:=
+ (* works as zify_unop, except that we should be careful when
+    dealing with b, since it can be equal to a *)
+ let isza := isZcst a in
+ match isza with
+   | true => zify_unop (t a) (thm a) b
+   | _ =>
+       let za := fresh "z" in
+       (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
+       (remember a as za; match goal with
+         | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
+         | _ => zify_unop_nored (t za) (thm za) b
+        end)
+ end.
+
+(* end from PreOmega *)
+
+Ltac applySpec S :=
+  let t := type of S in
+  match t with
+  | @BinOpSpec _ _ ?Op _ =>
+    let Spec := (eval unfold S, BSpec in (@BSpec _ _ Op _ S)) in
+    repeat
+      match goal with
+      | H : context[Op ?X ?Y] |- _ => zify_binop Op Spec X Y
+      | |- context[Op ?X ?Y]       => zify_binop Op Spec X Y
+      end
+  | @UnOpSpec _ _ ?Op _ =>
+    let Spec := (eval unfold S, USpec in (@USpec _ _ Op _ S)) in
+    repeat
+      match goal with
+      | H : context[Op ?X] |- _ => zify_unop Op Spec X
+      | |- context[Op ?X ]       => zify_unop Op Spec X
+      end
+  end.
+
+(** [zify_post_hook] is there to be redefined. *)
+Ltac zify_post_hook := idtac.
+
+Ltac zify := zify_tac ; (iter_specs applySpec) ; zify_post_hook.