[micromega] Optimised cnf in case an hypothesis is trivially False.

This optimisation reduces (sometimes) the dependencies of a proof.

3 files changed, 29 insertions, 20 deletions

diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index b231779c7b..1556ec31b5 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1384,11 +1384,13 @@ let rxcnf_or unsat deduce rXCNF polarity k e1 e2 =
 let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 =
   let e3,t1 = rXCNF (negb polarity) k e1 in
   if polarity
-  then if is_cnf_ff e3
-       then rXCNF polarity k e2
-       else let e4,t2 = rXCNF polarity k e2 in
-            let f',t' = ror_cnf_opt unsat deduce e3 e4 in
-            f',(rev_append t1 (rev_append t2 t'))
+  then if is_cnf_tt e3
+       then e3,t1
+       else if is_cnf_ff e3
+            then rXCNF polarity k e2
+            else let e4,t2 = rXCNF polarity k e2 in
+                 let f',t' = ror_cnf_opt unsat deduce e3 e4 in
+                 f',(rev_append t1 (rev_append t2 t'))
   else let e4,t2 = rXCNF polarity k e2 in
        (and_cnf_opt e3 e4),(rev_append t1 t2)
 
diff --git a/theories/micromega/MExtraction.v b/theories/micromega/MExtraction.v
index fcb07c4774..a02d7adfa2 100644
--- a/theories/micromega/MExtraction.v
+++ b/theories/micromega/MExtraction.v
@@ -53,12 +53,13 @@ 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. *)
-(*Extraction "micromega.ml"
+(*
+Extraction "micromega.ml"
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
            Tauto.abst_form
            ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
-           denorm Qpower vm_add
+           denorm QArith_base.Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 *)
 (* Local Variables: *)
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index ce12b02359..515372466a 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -611,13 +611,15 @@ Section S.
         let '(e1 , t1) := (RXCNF (negb polarity) e1) in
         if polarity
         then
-          if is_cnf_ff e1
-          then
-            RXCNF polarity e2
-          else (* compute disjunction *)
-            let '(e2 , t2) := (RXCNF polarity e2) in
-            let (f',t') := ror_cnf_opt e1 e2 in
-            (f', t1 +++ t2 +++ t') (* record the hypothesis *)
+          if is_cnf_tt e1
+          then (e1,t1)
+          else if is_cnf_ff e1
+            then
+              RXCNF polarity e2
+            else (* compute disjunction *)
+              let '(e2 , t2) := (RXCNF polarity e2) in
+              let (f',t') := ror_cnf_opt e1 e2 in
+              (f', t1 +++ t2 +++ t') (* record the hypothesis *)
         else
           let '(e2 , t2) := (RXCNF polarity e2) in
           (and_cnf_opt e1 e2, t1 +++ t2).
@@ -1349,6 +1351,7 @@ Section S.
     reflexivity.
   Qed.
 
+
   Lemma rxcnf_impl_xcnf :
     forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
            (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
@@ -1366,9 +1369,15 @@ Section S.
     simpl in *.
     subst.
     destruct pol;auto.
-    generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
+    generalize (is_cnf_tt_inv (xcnf (negb true) f1)).
+    destruct (is_cnf_tt (xcnf (negb true) f1)).
+    + intros.
+      rewrite H by auto.
+      reflexivity.
+    +
+      generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
     destruct (is_cnf_ff (xcnf (negb true) f1)).
-    + intros H.
+    * intros.
       rewrite H by auto.
       unfold or_cnf_opt.
       simpl.
@@ -1377,16 +1386,13 @@ Section S.
       destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
       apply is_cnf_ff_inv in EQ1. congruence.
       reflexivity.
-    +
+    *
       rewrite <- ror_opt_cnf_cnf.
       destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
       intros.
       reflexivity.
   Qed.
 
-
-
-
   Lemma rxcnf_iff_xcnf :
     forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
            (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)