Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

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

1 files changed, 175 insertions, 0 deletions

diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
new file mode 100644
index 000000000..70786a057
--- /dev/null
+++ b/plugins/micromega/RMicromega.v
@@ -0,0 +1,175 @@
+(************************************************************************)
+(*  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.
+Declare ML Module "micromega_plugin".
+
+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 Zeq_bool_eq ; auto.
+  apply R_power_theory.
+  intros x y.
+  intro.
+  apply IZR_neq.
+  apply 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_op2 (o:Op2) : R -> R -> Prop :=
+    match o with
+      | OpEq =>  @eq R
+      | OpNEq => fun x y  => ~ x = y
+      | OpLe => Rle
+      | OpGe => Rge
+      | OpLt => Rlt
+      | OpGt => Rgt
+    end.
+
+
+Definition Reval_formula (e: PolEnv R) (ff : Formula Z) :=
+  let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
+
+Definition Reval_formula' :=
+  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow.
+
+Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
+Proof.
+  intros.
+  unfold Reval_formula.
+  destruct f.
+  unfold Reval_formula'.
+  unfold Reval_expr.
+  split ; destruct Fop ; simpl ; auto.
+  apply Rge_le.
+  apply Rle_ge.
+Qed.
+
+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. rewrite Reval_formula_compat.
+  unfold Reval_formula'. now apply (cnf_normalise_correct Rsor).
+  intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor).
+  intros t w0.
+  apply RWeakChecker_sound.
+Qed.
+
+