From dfff69ef604e02703575cb1cb15b2f77eda5f0f4 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 28 Mar 2019 15:24:33 +0100
Subject: 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
---
 plugins/micromega/zify.mli | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 plugins/micromega/zify.mli

(limited to 'plugins/micromega/zify.mli')

diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
new file mode 100644
index 0000000000..f7844f53bc
--- /dev/null
+++ b/plugins/micromega/zify.mli
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+open Constrexpr
+
+module type S = sig val register : constr_expr -> unit val print : unit -> unit end
+
+module InjTable : S
+module UnOp     : S
+module BinOp    : S
+module CstOp    : S
+module BinRel   : S
+module PropOp   : S
+module Spec     : S
+module Saturate : S
+
+val zify_tac : unit Proofview.tactic
+val saturate : unit Proofview.tactic
+val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
-- 
cgit v1.2.3