diff options
Diffstat (limited to 'contrib/micromega/QMicromega.v')
| -rw-r--r-- | contrib/micromega/QMicromega.v | 199 |
1 files changed, 0 insertions, 199 deletions
diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v deleted file mode 100644 index c054f218..00000000 --- a/contrib/micromega/QMicromega.v +++ /dev/null @@ -1,199 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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 *) -(* *) -(************************************************************************) - -Require Import OrderedRing. -Require Import RingMicromega. -Require Import Refl. -Require Import QArith. -Require Import Qfield. - -Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. -Proof. - constructor; intros ; subst ; try (intuition (subst; auto with qarith)). - apply Q_Setoid. - rewrite H ; rewrite H0 ; reflexivity. - rewrite H ; rewrite H0 ; reflexivity. - rewrite H ; auto ; reflexivity. - rewrite <- H ; rewrite <- H0 ; auto. - rewrite H ; rewrite H0 ; auto. - rewrite <- H ; rewrite <- H0 ; auto. - rewrite H ; rewrite H0 ; auto. - apply Qsrt. - apply Qle_refl. - apply Qle_antisym ; auto. - eapply Qle_trans ; eauto. - apply Qlt_le_weak ; auto. - apply (Qlt_not_eq n m H H0) ; auto. - destruct (Qle_lt_or_eq _ _ H0) ; auto. - tauto. - destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto. - apply (Qplus_le_compat p p n m (Qle_refl p) H). - generalize (Qmult_lt_compat_r 0 n m H0 H). - rewrite Qmult_0_l. - auto. - compute in H. - discriminate. -Qed. - - -Lemma QSORaddon : - SORaddon 0 1 Qplus Qmult Qminus Qopp Qeq Qle (* ring elements *) - 0 1 Qplus Qmult Qminus Qopp (* coefficients *) - Qeq_bool Qle_bool - (fun x => x) (fun x => x) (pow_N 1 Qmult). -Proof. - constructor. - constructor ; intros ; try reflexivity. - apply Qeq_bool_eq; auto. - constructor. - reflexivity. - intros x y. - apply Qeq_bool_neq ; auto. - apply Qle_bool_imp_le. -Qed. - - -(*Definition Zeval_expr := eval_pexpr 0 Zplus Zmult Zminus Zopp (fun x => x) (fun x => Z_of_N x) (Zpower).*) -Require Import EnvRing. - -Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := - match e with - | PEc c => c - | PEX j => env j - | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) - | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) - | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) - | PEopp pe1 => - (Qeval_expr env pe1) - | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z_of_N n) - end. - -Lemma Qeval_expr_simpl : forall env e, - Qeval_expr env e = - match e with - | PEc c => c - | PEX j => env j - | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) - | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) - | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) - | PEopp pe1 => - (Qeval_expr env pe1) - | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z_of_N n) - end. -Proof. - destruct e ; reflexivity. -Qed. - -Definition Qeval_expr' := eval_pexpr Qplus Qmult Qminus Qopp (fun x => x) (fun x => x) (pow_N 1 Qmult). - -Lemma QNpower : forall r n, r ^ Z_of_N n = pow_N 1 Qmult r n. -Proof. - destruct n ; reflexivity. -Qed. - - -Lemma Qeval_expr_compat : forall env e, Qeval_expr env e = Qeval_expr' env e. -Proof. - induction e ; simpl ; subst ; try congruence. - rewrite IHe. - apply QNpower. -Qed. - -Definition Qeval_op2 (o : Op2) : Q -> Q -> Prop := -match o with -| OpEq => Qeq -| OpNEq => fun x y => ~ x == y -| OpLe => Qle -| OpGe => fun x y => Qle y x -| OpLt => Qlt -| OpGt => fun x y => Qlt y x -end. - -Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) := - let (lhs,o,rhs) := ff in Qeval_op2 o (Qeval_expr e lhs) (Qeval_expr e rhs). - -Definition Qeval_formula' := - eval_formula Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult). - -Lemma Qeval_formula_compat : forall env f, Qeval_formula env f <-> Qeval_formula' env f. -Proof. - intros. - unfold Qeval_formula. - destruct f. - repeat rewrite Qeval_expr_compat. - unfold Qeval_formula'. - unfold Qeval_expr'. - split ; destruct Fop ; simpl; auto. -Qed. - - - -Definition Qeval_nformula := - eval_nformula 0 Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult). - -Definition Qeval_op1 (o : Op1) : Q -> Prop := -match o with -| Equal => fun x : Q => x == 0 -| NonEqual => fun x : Q => ~ x == 0 -| Strict => fun x : Q => 0 < x -| NonStrict => fun x : Q => 0 <= x -end. - -Lemma Qeval_nformula_simpl : forall env f, Qeval_nformula env f = (let (p, op) := f in Qeval_op1 op (Qeval_expr env p)). -Proof. - intros. - destruct f. - rewrite Qeval_expr_compat. - reflexivity. -Qed. - -Lemma Qeval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d). -Proof. - exact (fun env d =>eval_nformula_dec Qsor (fun x => x) (fun x => x) (pow_N 1 Qmult) env d). -Qed. - -Definition QWitness := ConeMember Q. - -Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool. - -Require Import List. - -Lemma QWeakChecker_sound : forall (l : list (NFormula Q)) (cm : QWitness), - QWeakChecker l cm = true -> - forall env, make_impl (Qeval_nformula env) l False. -Proof. - intros l cm H. - intro. - unfold Qeval_nformula. - apply (checker_nf_sound Qsor QSORaddon l cm). - unfold QWeakChecker in H. - exact H. -Qed. - -Require Import Tauto. - -Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := - @tauto_checker (Formula Q) (NFormula Q) (@cnf_normalise Q) (@cnf_negate Q) QWitness QWeakChecker f w. - -Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_f (Qeval_formula env) f. -Proof. - intros f w. - unfold QTautoChecker. - apply (tauto_checker_sound Qeval_formula Qeval_nformula). - apply Qeval_nformula_dec. - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_normalise_correct Qsor). - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_negate_correct Qsor). - intros t w0. - apply QWeakChecker_sound. -Qed. - - |