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/Refl.v | 49 ++++++++++++++++++++++++++----------------------
 1 file changed, 27 insertions(+), 22 deletions(-)

(limited to 'plugins/micromega/Refl.v')

diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index 63b4d5e8f8..cd759029fa 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -99,8 +99,6 @@ Proof.
   apply IHl; auto.
 Qed.
 
-
-
 Lemma make_conj_app : forall  A eval l1 l2, @make_conj A eval (l1 ++ l2) <-> @make_conj A eval l1 /\ @make_conj A eval l2.
 Proof.
   induction l1.
@@ -114,34 +112,41 @@ Proof.
   tauto.
 Qed.
 
+Infix "+++" := rev_append (right associativity, at level 60) : list_scope.
+
+Lemma make_conj_rapp : forall  A eval l1 l2, @make_conj A eval (l1 +++ l2) <-> @make_conj A eval (l1++l2).
+Proof.
+  induction l1.
+  - simpl. tauto.
+  - intros.
+    simpl rev_append at 1.
+    rewrite IHl1.
+    rewrite make_conj_app.
+    rewrite make_conj_cons.
+    simpl app.
+    rewrite make_conj_cons.
+    rewrite make_conj_app.
+    tauto.
+Qed.
+
 Lemma not_make_conj_cons : forall (A:Type) (t:A) a eval  (no_middle_eval : (eval t) \/ ~ (eval  t)),
-  ~ make_conj  eval (t ::a) -> ~  (eval t) \/ (~ make_conj  eval a).
+  ~ make_conj  eval (t ::a) <-> ~  (eval t) \/ (~ make_conj  eval a).
 Proof.
   intros.
-  simpl in H.
-  destruct a.
-  tauto.
+  rewrite make_conj_cons.
   tauto.
 Qed.
 
 Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval
   (no_middle_eval : forall d, eval d \/ ~ eval d) ,
-  ~ make_conj  eval (t ++ a) -> (~ make_conj  eval t) \/ (~ make_conj eval a).
+  ~ make_conj  eval (t ++ a) <-> (~ make_conj  eval t) \/ (~ make_conj eval a).
 Proof.
   induction t.
-  simpl.
-  tauto.
-  intros.
-  simpl ((a::t)++a0)in H.
-  destruct (@not_make_conj_cons _ _ _ _  (no_middle_eval a) H).
-  left ; red ; intros.
-  apply H0.
-  rewrite  make_conj_cons in H1.
-  tauto.
-  destruct (IHt _ _ no_middle_eval H0).
-  left ; red ; intros.
-  apply H1.
-  rewrite make_conj_cons in H2.
-  tauto.
-  right ; auto.
+  - simpl.
+    tauto.
+  - intros.
+    simpl ((a::t)++a0).
+    rewrite !not_make_conj_cons by auto.
+    rewrite IHt by auto.
+    tauto.
 Qed.
-- 
cgit v1.2.3