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

1 files changed, 27 insertions, 22 deletions

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.