diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/micromega/RMicromega.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/micromega/RMicromega.v')
-rw-r--r-- | contrib/micromega/RMicromega.v | 148 |
1 files changed, 148 insertions, 0 deletions
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v new file mode 100644 index 00000000..ef28db32 --- /dev/null +++ b/contrib/micromega/RMicromega.v @@ -0,0 +1,148 @@ +(************************************************************************) +(* 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 Raxioms RIneq Rpow_def DiscrR. +Require Setoid. + +Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). +Proof. + constructor. + exact Rplus_0_l. + exact Rplus_comm. + intros. rewrite Rplus_assoc. auto. + exact Rmult_1_l. + exact Rmult_comm. + intros ; rewrite Rmult_assoc ; auto. + intros. rewrite Rmult_comm. rewrite Rmult_plus_distr_l. + rewrite (Rmult_comm z). rewrite (Rmult_comm z). auto. + reflexivity. + exact Rplus_opp_r. +Qed. + +Add Ring Rring : Rsrt. +Open Scope R_scope. + +Lemma Rmult_neutral : forall x:R , 0 * x = 0. +Proof. + intro ; ring. +Qed. + + +Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt. +Proof. + constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)). + constructor. + constructor. + unfold RelationClasses.Symmetric. auto. + unfold RelationClasses.Transitive. intros. subst. reflexivity. + apply Rsrt. + eapply Rle_trans ; eauto. + apply (Rlt_irrefl m) ; auto. + apply Rnot_le_lt. auto with real. + destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto. + intros. + rewrite <- (Rmult_neutral m). + apply (Rmult_lt_compat_r) ; auto. +Qed. + +Require ZMicromega. + +(* R with coeffs in Z *) + +Lemma RZSORaddon : + SORaddon R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) + 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) + Zeq_bool Zle_bool + IZR Nnat.nat_of_N pow. +Proof. + constructor. + constructor ; intros ; try reflexivity. + apply plus_IZR. + symmetry. apply Z_R_minus. + apply mult_IZR. + apply Ropp_Ropp_IZR. + apply IZR_eq. + apply Zeqb_ok ; auto. + apply R_power_theory. + intros x y. + intro. + apply IZR_neq. + apply ZMicromega.Zeq_bool_neq ; auto. + intros. apply IZR_le. apply Zle_bool_imp_le. auto. +Qed. + + +Require Import EnvRing. + +Definition INZ (n:N) : R := + match n with + | N0 => IZR 0%Z + | Npos p => IZR (Zpos p) + end. + +Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow. + + +Definition Reval_formula := + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. + + +Definition Reval_nformula := + eval_nformula 0 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. + + +Lemma Reval_nformula_dec : forall env d, (Reval_nformula env d) \/ ~ (Reval_nformula env d). +Proof. + exact (fun env d =>eval_nformula_dec Rsor IZR Nnat.nat_of_N pow env d). +Qed. + +Definition RWitness := ConeMember Z. + +Definition RWeakChecker := check_normalised_formulas 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Zle_bool. + +Require Import List. + +Lemma RWeakChecker_sound : forall (l : list (NFormula Z)) (cm : RWitness), + RWeakChecker l cm = true -> + forall env, make_impl (Reval_nformula env) l False. +Proof. + intros l cm H. + intro. + unfold Reval_nformula. + apply (checker_nf_sound Rsor RZSORaddon l cm). + unfold RWeakChecker in H. + exact H. +Qed. + +Require Import Tauto. + +Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness) : bool := + @tauto_checker (Formula Z) (NFormula Z) (@cnf_normalise Z) (@cnf_negate Z) RWitness RWeakChecker f w. + +Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_f (Reval_formula env) f. +Proof. + intros f w. + unfold RTautoChecker. + apply (tauto_checker_sound Reval_formula Reval_nformula). + apply Reval_nformula_dec. + intros. unfold Reval_formula. now apply (cnf_normalise_correct Rsor). + intros. unfold Reval_formula. now apply (cnf_negate_correct Rsor). + intros t w0. + apply RWeakChecker_sound. +Qed. + + |