Improved lia + experimental nlia

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 187 insertions, 26 deletions

diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index fcbf7f969..ed7a104e8 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-20011                            *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -64,6 +64,15 @@ Set Implicit Arguments.
 
     Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
 
+    Variable unsat : Term'  -> bool.
+
+    Variable unsat_prop : forall t, unsat t  = true ->  
+      forall env, eval' env t -> False. 
+
+    Variable deduce : Term' -> Term' -> option Term'.
+
+    Variable deduce_prop : forall env t t' u,
+      eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u.
 
     Definition clause := list  Term'.
     Definition cnf := list clause.
@@ -76,8 +85,48 @@ Set Implicit Arguments.
     Definition ff : cnf :=  cons (@nil Term') nil.
 
 
+    Fixpoint add_term (t: Term') (cl : clause) : option clause :=
+      match cl with
+        | nil => 
+          match deduce t t with
+            | None =>  Some (t ::nil)
+            | Some u => if unsat u then None else Some (t::nil)
+          end
+        | t'::cl => 
+          match deduce t t' with
+            | None => 
+              match add_term t cl with
+                | None => None
+                | Some cl' => Some (t' :: cl')
+              end
+            | Some u => 
+              if unsat u then None else 
+                match add_term t cl with
+                  | None => None
+                  | Some cl' => Some (t' :: cl')
+                end
+          end
+      end.
+
+    Fixpoint or_clause (cl1 cl2 : clause) : option clause :=
+      match cl1 with
+        | nil => Some cl2
+        | t::cl => match add_term t cl2 with
+                     | None => None
+                     | Some cl' => or_clause cl cl'
+                   end
+      end.
+
+(*    Definition or_clause_cnf (t:clause) (f:cnf) : cnf :=
+      List.map (fun x => (t++x)) f. *)
+
     Definition or_clause_cnf (t:clause) (f:cnf) : cnf :=
-      List.map (fun x => (t++x)) f.
+      List.fold_right (fun e acc => 
+        match or_clause t e with
+          | None => acc
+          | Some cl => cl :: acc
+        end) nil f.
+
 
     Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
       match f with
@@ -102,46 +151,154 @@ Set Implicit Arguments.
         | I e1 e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2)
       end.
 
-  Definition eval_cnf (env : Term' -> Prop) (f:cnf) := make_conj  (fun cl => ~ make_conj  env cl) f.
+    Definition eval_clause (env : Env) (cl : clause) := ~ make_conj  (eval' env) cl.
+
+    Definition eval_cnf (env : Env) (f:cnf) := make_conj  (eval_clause  env) f.
+
+    
+    Lemma eval_cnf_app : forall env x y, eval_cnf env (x++y) -> eval_cnf env x /\ eval_cnf env y.
+    Proof.
+      unfold eval_cnf.
+      intros.
+      rewrite make_conj_app in H ; auto.
+    Qed.
 
 
-  Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x++y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y.
+    Definition eval_opt_clause (env : Env) (cl: option clause) :=
+      match cl with
+        | None => True
+        | Some cl => eval_clause env cl
+      end.
+
+
+    Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) -> eval_clause env (t::cl).
+    Proof.
+      induction cl.
+      (* BC *)
+      simpl.
+      case_eq (deduce t t) ; auto.
+      intros until 0.
+      case_eq (unsat t0) ; auto.
+      unfold eval_clause.
+      rewrite make_conj_cons. 
+      intros. intro.
+      apply unsat_prop with (1:= H) (env := env).
+      apply deduce_prop with (3:= H0) ; tauto.
+      (* IC *)
+      simpl.
+      case_eq (deduce t a).
+      intro u.
+      case_eq (unsat u).
+      simpl. intros.
+      unfold eval_clause.
+      intro.
+      apply unsat_prop  with (1:= H) (env:= env).
+      repeat rewrite make_conj_cons in H2.
+      apply deduce_prop with (3:= H0); tauto.
+      intro.
+      case_eq (add_term t cl) ; intros.
+      simpl in H2.
+      rewrite H0 in IHcl.
+      simpl in IHcl.
+      unfold eval_clause in *.
+      intros.
+      repeat rewrite make_conj_cons in *.
+      tauto.
+      rewrite H0 in IHcl ; simpl in *.
+      unfold eval_clause in *.
+      intros.
+      repeat rewrite make_conj_cons in *.
+      tauto.
+      case_eq (add_term t cl) ; intros.
+      simpl in H1.
+      unfold eval_clause in *.
+      repeat rewrite make_conj_cons in *.
+      rewrite H in IHcl.
+      simpl in IHcl.
+      tauto.
+      simpl in *.
+      rewrite H in IHcl.
+      simpl in IHcl.
+      unfold eval_clause in *.
+      repeat rewrite make_conj_cons in *.    
+      tauto.
+    Qed.
+
+
+  Lemma or_clause_correct : forall cl cl' env,  eval_opt_clause env (or_clause cl cl') -> eval_clause env cl \/ eval_clause env cl'.
   Proof.
-    unfold eval_cnf.
+    induction cl.
+    simpl. tauto.
+    intros until 0.
+    simpl.
+    assert (HH := add_term_correct env a cl').
+    case_eq (add_term a cl').
+    simpl in *.
+    intros.
+    apply IHcl in H0.
+    rewrite H in HH.
+    simpl in HH.
+    unfold eval_clause in *.
+    destruct H0.
+    repeat rewrite make_conj_cons in *.
+    tauto.
+    apply HH in H0.
+    apply not_make_conj_cons in H0 ; auto.
+    repeat rewrite make_conj_cons in *.
+    tauto.
+    simpl.
     intros.
-    rewrite make_conj_app in H ; auto.
+    rewrite H in HH.
+    simpl in HH.
+    unfold eval_clause in *.
+    assert (HH' := HH Coq.Init.Logic.I).
+    apply not_make_conj_cons in HH'; auto.
+    repeat rewrite make_conj_cons in *.
+    tauto.
   Qed.
+    
 
-
-  Lemma or_clause_correct : forall env t f, eval_cnf (eval' env) (or_clause_cnf t f) -> (~ make_conj  (eval' env) t) \/ (eval_cnf (eval' env) f).
+  Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) -> (eval_clause env t) \/ (eval_cnf env f).
   Proof.
     unfold eval_cnf.
     unfold or_clause_cnf.
+    intros until t.
+    set (F := (fun (e : clause) (acc : list clause) =>
+         match or_clause t e with
+         | Some cl => cl :: acc
+         | None => acc
+         end)).
     induction f.
-    simpl.
-    intros ; right;auto.
+    auto.
     (**)
-    rewrite map_simpl.
+    simpl.
     intros.
-    rewrite make_conj_cons in H.
-    destruct H as [HH1 HH2].
-    generalize (IHf HH2) ; clear IHf ; intro.
-    destruct H.
-    left ; auto.
-    rewrite make_conj_cons.
-    destruct (not_make_conj_app _ _ _ (no_middle_eval' env) HH1).
-    tauto.
+    destruct f.
+    simpl in H.
+    simpl in IHf. 
+    unfold F in H.
+    revert H.
+    intros.
+    apply or_clause_correct.
+    destruct (or_clause t a) ; simpl in * ; auto.
+    unfold F in H at 1.
+    revert H.
+    assert (HH := or_clause_correct t a env).
+    destruct (or_clause t a); simpl in HH ;
+    rewrite make_conj_cons in * ; intuition.
+    rewrite make_conj_cons in *.
     tauto.
   Qed.
 
- Lemma eval_cnf_cons : forall env a f,  (~ make_conj  (eval' env) a) -> eval_cnf (eval' env) f -> eval_cnf (eval' env) (a::f).
+
+ Lemma eval_cnf_cons : forall env a f,  (~ make_conj  (eval' env) a) -> eval_cnf env f -> eval_cnf env (a::f).
  Proof.
    intros.
    unfold eval_cnf in *.
    rewrite make_conj_cons ; eauto.
  Qed.
 
-  Lemma or_cnf_correct : forall env f f', eval_cnf (eval' env) (or_cnf f f') -> (eval_cnf (eval' env)  f) \/ (eval_cnf (eval' env) f').
+  Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') -> (eval_cnf env  f) \/ (eval_cnf  env f').
   Proof.
     induction f.
     unfold eval_cnf.
@@ -153,19 +310,19 @@ Set Implicit Arguments.
     destruct (eval_cnf_app _ _ _ H).
     clear H.
     destruct (IHf _ H0).
-    destruct (or_clause_correct _ _ _ H1).
+    destruct (or_clause_cnf_correct _ _ _ H1).
     left.
     apply eval_cnf_cons ; auto.
     right ; auto.
     right ; auto.
   Qed.
 
-  Variable normalise_correct : forall env t, eval_cnf (eval' env) (normalise t) -> eval env t.
+  Variable normalise_correct : forall env t, eval_cnf  env (normalise t) -> eval env t.
 
-  Variable negate_correct : forall env t, eval_cnf  (eval' env) (negate t) -> ~ eval env t.
+  Variable negate_correct : forall env t, eval_cnf env (negate t) -> ~ eval env t.
 
 
-  Lemma xcnf_correct : forall f pol env, eval_cnf (eval' env) (xcnf pol f) -> eval_f (eval env) (if pol then f else N f).
+  Lemma xcnf_correct : forall f pol env, eval_cnf env (xcnf pol f) -> eval_f (eval env) (if pol then f else N f).
   Proof.
     induction f.
     (* TT *)
@@ -175,15 +332,19 @@ Set Implicit Arguments.
     (* FF *)
     unfold eval_cnf.
     destruct pol; simpl ; auto.
+    unfold eval_clause ; simpl.
+    tauto.
     (* P *)
     simpl.
     destruct pol ; intros ;simpl.
     unfold eval_cnf in H.
     (* Here I have to drop the proposition *)
     simpl in H.
+    unfold eval_clause in H ; simpl in H.
     tauto.
     (* Here, I could store P in the clause *)
     unfold eval_cnf in H;simpl in H.
+    unfold eval_clause in H ; simpl in H.
     tauto.
     (* A *)
     simpl.
@@ -282,7 +443,7 @@ Set Implicit Arguments.
                 end
       end.
 
-  Lemma cnf_checker_sound : forall t  w, cnf_checker t w = true -> forall env, eval_cnf  (eval' env)  t.
+  Lemma cnf_checker_sound : forall t  w, cnf_checker t w = true -> forall env, eval_cnf  env  t.
   Proof.
     unfold eval_cnf.
     induction t.