diff options
Diffstat (limited to 'plugins/micromega/CheckerMaker.v')
| -rw-r--r-- | plugins/micromega/CheckerMaker.v | 132 |
1 files changed, 0 insertions, 132 deletions
diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v deleted file mode 100644 index 04336747..00000000 --- a/plugins/micromega/CheckerMaker.v +++ /dev/null @@ -1,132 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* *) -(* Micromega: A reflexive tactic using the Positivstellensatz *) -(* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) -(* *) -(************************************************************************) - -(* FK: scheduled for deletion *) -(* -Require Import Setoid. -Require Import Decidable. -Require Import List. -Require Import Refl. - -Set Implicit Arguments. - -Section CheckerMaker. - -(* 'Formula' is a syntactic representation of a certain kind of propositions. *) -Variable Formula : Type. - -Variable Env : Type. - -Variable eval : Env -> Formula -> Prop. - -Variable Formula' : Type. - -Variable eval' : Env -> Formula' -> Prop. - -Variable normalise : Formula -> Formula'. - -Variable negate : Formula -> Formula'. - -Hypothesis normalise_sound : - forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t). - -Hypothesis negate_correct : - forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)). - -Variable Witness : Type. - -Variable check_formulas' : list Formula' -> Witness -> bool. - -Hypothesis check_formulas'_sound : - forall (l : list Formula') (w : Witness), - check_formulas' l w = true -> - forall env : Env, make_impl (eval' env) l False. - -Definition normalise_list : list Formula -> list Formula' := map normalise. -Definition negate_list : list Formula -> list Formula' := map negate. - -Definition check_formulas (l : list Formula) (w : Witness) : bool := - check_formulas' (map normalise l) w. - -(* Contraposition of normalise_sound for lists *) -Lemma normalise_sound_contr : forall (env : Env) (l : list Formula), - make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False. -Proof. -intros env l; induction l as [| t l IH]; simpl in *. -trivial. -intros H1 H2. apply IH. apply H1. now apply normalise_sound. -Qed. - -Theorem check_formulas_sound : - forall (l : list Formula) (w : Witness), - check_formulas l w = true -> forall env : Env, make_impl (eval env) l False. -Proof. -unfold check_formulas; intros l w H env. destruct l as [| t l]; simpl in *. -pose proof (check_formulas'_sound H env) as H1; now simpl in H1. -intro H1. apply normalise_sound in H1. -pose proof (check_formulas'_sound H env) as H2; simpl in H2. -apply H2 in H1. now apply normalise_sound_contr. -Qed. - -(* In check_conj_formulas', t2 is supposed to be a list of negations of -formulas. If, for example, t1 = [A1, A2] and t2 = [~ B1, ~ B2], then -check_conj_formulas' checks that each of [~ B1, A1, A2] and [~ B2, A1, A2] is -inconsistent. This means that A1 /\ A2 -> B1 and A1 /\ A2 -> B1, i.e., that -A1 /\ A2 -> B1 /\ B2. *) - -Fixpoint check_conj_formulas' - (t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool := -match t2 with -| nil => true -| t':: rt2 => - match wits with - | nil => false - | w :: rwits => - match check_formulas' (t':: t1) w with - | true => check_conj_formulas' t1 rwits rt2 - | false => false - end - end -end. - -(* checks whether the conjunction of t1 implies the conjunction of t2 *) - -Definition check_conj_formulas - (t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool := - check_conj_formulas' (normalise_list t1) wits (negate_list t2). - -Theorem check_conj_formulas_sound : - forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness), - check_conj_formulas t1 wits t2 = true -> - forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2). -Proof. -intro t1; induction t2 as [| a2 t2' IH]. -intros; apply make_impl_true. -intros wits H env. -unfold check_conj_formulas in H; simpl in H. -destruct wits as [| w ws]; simpl in H. discriminate. -case_eq (check_formulas' (negate a2 :: normalise_list t1) w); -intro H1; rewrite H1 in H; [| discriminate]. -assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by -now apply check_formulas'_sound with (w := w). clear H1. -pose proof (IH ws H env) as H1. simpl in H2. -assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False) -by auto using normalise_sound_contr. clear H2. -rewrite <- make_conj_impl in *. -rewrite make_conj_cons. intro H2. split. -apply <- negate_correct. intro; now elim H3. exact (H1 H2). -Qed. - -End CheckerMaker. -*)
\ No newline at end of file |