summaryrefslogtreecommitdiff
path: root/plugins/micromega/Tauto.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/Tauto.v')
-rw-r--r--plugins/micromega/Tauto.v248
1 files changed, 220 insertions, 28 deletions
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 0706611c..440070a1 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 *)
(* *)
(************************************************************************)
@@ -41,6 +41,37 @@ Set Implicit Arguments.
| I f1 f2 => (eval_f ev f1) -> (eval_f ev f2)
end.
+ Lemma eval_f_morph : forall A (ev ev' : A -> Prop) (f : BFormula A),
+ (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f).
+ Proof.
+ induction f ; simpl ; try tauto.
+ intros.
+ assert (H' := H a).
+ auto.
+ Qed.
+
+
+
+ Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U :=
+ match f with
+ | TT => TT _
+ | FF => FF _
+ | X p => X _ p
+ | A a => A (fct a)
+ | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2)
+ | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2)
+ | N f => N (map_bformula fct f)
+ | I f1 f2 => I (map_bformula fct f1) (map_bformula fct f2)
+ end.
+
+ Lemma eval_f_map : forall T U (fct: T-> U) env f ,
+ eval_f env (map_bformula fct f) = eval_f (fun x => env (fct x)) f.
+ Proof.
+ induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto.
+ rewrite <- IHf. auto.
+ Qed.
+
+
Lemma map_simpl : forall A B f l, @map A B f l = match l with
| nil => nil
@@ -52,6 +83,7 @@ Set Implicit Arguments.
+
Section S.
Variable Env : Type.
@@ -64,6 +96,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 +117,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 +183,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.
+
+
+ Definition eval_opt_clause (env : Env) (cl: option clause) :=
+ match cl with
+ | None => True
+ | Some cl => eval_clause env cl
+ end.
- Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x++y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y.
+ 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 +342,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 +364,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 +475,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.
@@ -319,7 +512,6 @@ Set Implicit Arguments.
-
End S.
(* Local Variables: *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 14:25:04 +0000