Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 259 insertions, 0 deletions

diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
new file mode 100644
index 00000000..9e95f6c4
--- /dev/null
+++ b/contrib/micromega/QMicromega.v
@@ -0,0 +1,259 @@
+(************************************************************************)
+(*  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 Qring.
+
+(* Qsrt has been removed from the library ? *)
+Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
+Proof.
+  constructor.
+  exact Qplus_0_l.
+  exact Qplus_comm.
+  exact Qplus_assoc.
+  exact Qmult_1_l.
+  exact Qmult_comm.
+  exact Qmult_assoc.
+  exact Qmult_plus_distr_l.
+  reflexivity.
+  exact Qplus_opp_r.
+Qed.
+
+
+Add Ring Qring : Qsrt.
+
+Lemma Qmult_neutral : forall x , 0 * x == 0.
+Proof.
+  intros.
+  compute.
+  reflexivity.
+Qed.
+
+(* Is there any qarith database ? *)
+
+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_neutral.
+  auto.
+  compute in H.
+  discriminate.
+Qed.
+
+Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z  (Qnum q * ' Qden p)%Z.
+
+Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z.
+
+Require ZMicromega.
+
+Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y.
+Proof.
+  intros.
+  unfold Qeq_bool in H.
+  unfold Qeq.
+  apply (Zeqb_ok  _ _ H).
+Qed.
+
+
+Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
+Proof.
+  unfold Qeq_bool,Qeq.
+  red ; intros ; subst.
+  rewrite H0 in H.
+  apply  (ZMicromega.Zeq_bool_neq _ _ H).
+  reflexivity.
+Qed.
+
+Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y.
+Proof.
+  unfold Qle_bool, Qle.
+  intros.
+  apply Zle_bool_imp_le ; auto.
+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_ok ; 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 => Qge
+| OpLt => Qlt
+| OpGt => Qgt
+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.
+
+