|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* *)
(* 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 Rfunctions RIneq Rpow_def DiscrR.
Require Import QArith.
Require Import Qfield.
Require Import Qreals.
Require Import DeclConstant.
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.
Open Scope R_scope.
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.
now apply Rmult_lt_0_compat.
Qed.
Lemma Rinv_1 : forall x, x * / 1 = x.
Proof.
intro.
rewrite Rinv_1.
apply Rmult_1_r.
Qed.
Lemma Qeq_true : forall x y, Qeq_bool x y = true -> Q2R x = Q2R y.
Proof.
intros.
now apply Qeq_eqR, Qeq_bool_eq.
Qed.
Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y.
Proof.
intros.
apply Qeq_bool_neq in H.
contradict H.
now apply eqR_Qeq.
Qed.
Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y.
Proof.
intros.
now apply Qle_Rle, Qle_bool_imp_le.
Qed.
Lemma Q2R_0 : Q2R 0 = 0.
Proof.
apply Rmult_0_l.
Qed.
Lemma Q2R_1 : Q2R 1 = 1.
Proof.
compute. apply Rinv_1.
Qed.
Lemma Q2R_inv_ext : forall x,
Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x).
Proof.
intros.
case_eq (Qeq_bool x 0).
intros.
apply Qeq_bool_eq in H.
destruct x ; simpl.
unfold Qeq in H.
simpl in H.
rewrite Zmult_1_r in H.
rewrite H.
apply Rmult_0_l.
intros.
now apply Q2R_inv, Qeq_bool_neq.
Qed.
Notation to_nat := N.to_nat.
Lemma QSORaddon :
@SORaddon R
R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *)
Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *)
Qeq_bool Qle_bool
Q2R nat to_nat pow.
Proof.
constructor.
constructor ; intros ; try reflexivity.
apply Q2R_0.
apply Q2R_1.
apply Q2R_plus.
apply Q2R_minus.
apply Q2R_mult.
apply Q2R_opp.
apply Qeq_true ; auto.
apply R_power_theory.
apply Qeq_false.
apply Qle_true.
Qed.
(* Syntactic ring coefficients. *)
Inductive Rcst :=
| C0
| C1
| CQ (r : Q)
| CZ (r : Z)
| CPlus (r1 r2 : Rcst)
| CMinus (r1 r2 : Rcst)
| CMult (r1 r2 : Rcst)
| CPow (r1 : Rcst) (z:Z+nat)
| CInv (r : Rcst)
| COpp (r : Rcst).
Definition z_of_exp (z : Z + nat) :=
match z with
| inl z => z
| inr n => Z.of_nat n
end.
Fixpoint Q_of_Rcst (r : Rcst) : Q :=
match r with
| C0 => 0 # 1
| C1 => 1 # 1
| CZ z => z # 1
| CQ q => q
| CPlus r1 r2 => Qplus (Q_of_Rcst r1) (Q_of_Rcst r2)
| CMinus r1 r2 => Qminus (Q_of_Rcst r1) (Q_of_Rcst r2)
| CMult r1 r2 => Qmult (Q_of_Rcst r1) (Q_of_Rcst r2)
| CPow r1 z => Qpower (Q_of_Rcst r1) (z_of_exp z)
| CInv r => Qinv (Q_of_Rcst r)
| COpp r => Qopp (Q_of_Rcst r)
end.
Definition is_neg (z: Z+nat) :=
match z with
| inl (Zneg _) => true
| _ => false
end.
Lemma is_neg_true : forall z, is_neg z = true -> (z_of_exp z < 0)%Z.
Proof.
destruct z ; simpl ; try congruence.
destruct z ; try congruence.
intros.
reflexivity.
Qed.
Lemma is_neg_false : forall z, is_neg z = false -> (z_of_exp z >= 0)%Z.
Proof.
destruct z ; simpl ; try congruence.
destruct z ; try congruence.
compute. congruence.
compute. congruence.
generalize (Zle_0_nat n). auto with zarith.
Qed.
Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1).
Definition CPowR0 (z : Z) (r : Rcst) :=
Z.ltb z Z0 && Qeq_bool (Q_of_Rcst r) (0 # 1).
Fixpoint R_of_Rcst (r : Rcst) : R :=
match r with
| C0 => R0
| C1 => R1
| CZ z => IZR z
| CQ q => Q2R q
| CPlus r1 r2 => (R_of_Rcst r1) + (R_of_Rcst r2)
| CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2)
| CMult r1 r2 => (R_of_Rcst r1) * (R_of_Rcst r2)
| CPow r1 z =>
match z with
| inl z =>
if CPowR0 z r1
then R0
else powerRZ (R_of_Rcst r1) z
| inr n => pow (R_of_Rcst r1) n
end
| CInv r =>
if CInvR0 r then R0
else Rinv (R_of_Rcst r)
| COpp r => - (R_of_Rcst r)
end.
Add Morphism Q2R with signature Qeq ==> @eq R as Q2R_m.
exact Qeq_eqR.
Qed.
Lemma Q2R_pow_pos : forall q p,
Q2R (pow_pos Qmult q p) = pow_pos Rmult (Q2R q) p.
Proof.
induction p ; simpl;auto;
rewrite <- IHp;
repeat rewrite Q2R_mult;
reflexivity.
Qed.
Lemma Q2R_pow_N : forall q n,
Q2R (pow_N 1%Q Qmult q n) = pow_N 1 Rmult (Q2R q) n.
Proof.
destruct n ; simpl.
- apply Q2R_1.
- apply Q2R_pow_pos.
Qed.
Lemma Qmult_integral : forall q r, q * r == 0 -> q == 0 \/ r == 0.
Proof.
intros.
destruct (Qeq_dec q 0)%Q.
- left ; apply q0.
- apply Qmult_integral_l in H ; tauto.
Qed.
Lemma Qpower_positive_eq_zero : forall q p,
Qpower_positive q p == 0 -> q == 0.
Proof.
unfold Qpower_positive.
induction p ; simpl; intros;
repeat match goal with
| H : _ * _ == 0 |- _ =>
apply Qmult_integral in H; destruct H
end; tauto.
Qed.
Lemma Qpower_positive_zero : forall p,
Qpower_positive 0 p == 0%Q.
Proof.
induction p ; simpl;
try rewrite IHp ; reflexivity.
Qed.
Lemma Q2RpowerRZ :
forall q z
(DEF : not (q == 0)%Q \/ (z >= Z0)%Z),
Q2R (q ^ z) = powerRZ (Q2R q) z.
Proof.
intros.
destruct Qpower_theory.
destruct R_power_theory.
unfold Qpower, powerRZ.
destruct z.
- apply Q2R_1.
-
change (Qpower_positive q p)
with (Qpower q (Zpos p)).
rewrite <- N2Z.inj_pos.
rewrite <- positive_N_nat.
rewrite rpow_pow_N.
rewrite rpow_pow_N0.
apply Q2R_pow_N.
-
rewrite Q2R_inv.
unfold Qpower_positive.
rewrite <- positive_N_nat.
rewrite rpow_pow_N0.
unfold pow_N.
rewrite Q2R_pow_pos.
auto.
intro.
apply Qpower_positive_eq_zero in H.
destruct DEF ; auto with arith.
Qed.
Lemma Qpower0 : forall z, (z <> 0)%Z -> (0 ^ z == 0)%Q.
Proof.
unfold Qpower.
destruct z;intros.
- congruence.
- apply Qpower_positive_zero.
- rewrite Qpower_positive_zero.
reflexivity.
Qed.
Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c.
Proof.
induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2).
- apply Q2R_0.
- apply Q2R_1.
- reflexivity.
- unfold Q2R. simpl. rewrite Rinv_1. reflexivity.
- apply Q2R_plus.
- apply Q2R_minus.
- apply Q2R_mult.
- destruct z.
destruct (CPowR0 z c) eqn:C; unfold CPowR0 in C.
+
rewrite andb_true_iff in C.
destruct C as (C1 & C2).
rewrite Z.ltb_lt in C1.
apply Qeq_bool_eq in C2.
rewrite C2.
simpl.
rewrite Qpower0 by auto with zarith.
apply Q2R_0.
+ rewrite Q2RpowerRZ.
rewrite IHc.
reflexivity.
rewrite andb_false_iff in C.
destruct C.
simpl. apply Z.ltb_ge in H.
auto with zarith.
left ; apply Qeq_bool_neq; auto.
+ simpl.
rewrite <- IHc.
destruct Qpower_theory.
rewrite <- nat_N_Z.
rewrite rpow_pow_N.
destruct R_power_theory.
rewrite <- (Nnat.Nat2N.id n) at 2.
rewrite rpow_pow_N0.
apply Q2R_pow_N.
- rewrite <- IHc.
unfold CInvR0.
apply Q2R_inv_ext.
- rewrite <- IHc.
apply Q2R_opp.
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 R_of_Rcst N.to_nat 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 Rcst) :=
let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
Definition Reval_formula' :=
eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst.
Definition QReval_formula :=
eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat 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 Qeval_nformula :=
eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R.
Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d).
Proof.
exact (fun env d =>eval_nformula_dec Rsor Q2R env d).
Qed.
Definition RWitness := Psatz Q.
Definition RWeakChecker := check_normalised_formulas 0%Q 1%Q Qplus Qmult Qeq_bool Qle_bool.
Require Import List.
Lemma RWeakChecker_sound : forall (l : list (NFormula Q)) (cm : RWitness),
RWeakChecker 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 Rsor QSORaddon l cm).
unfold RWeakChecker in H.
exact H.
Qed.
Require Import Coq.micromega.Tauto.
Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool.
Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool.
Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool :=
@tauto_checker (Formula Q) (NFormula Q)
unit runsat rdeduce
(Rnormalise unit) (Rnegate unit)
RWitness (fun cl => RWeakChecker (List.map fst cl)) (map_bformula (map_Formula Q_of_Rcst) f) w.
Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_bf (Reval_formula env) f.
Proof.
intros f w.
unfold RTautoChecker.
intros TC env.
apply tauto_checker_sound with (eval:=QReval_formula) (eval':= Qeval_nformula) (env := env) in TC.
- change (eval_f (fun x : Prop => x) (QReval_formula env))
with
(eval_bf (QReval_formula env)) in TC.
rewrite eval_bf_map in TC.
unfold eval_bf in TC.
rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto.
intro.
unfold QReval_formula.
rewrite <- eval_formulaSC with (phiS := R_of_Rcst).
rewrite Reval_formula_compat.
tauto.
intro. rewrite Q_of_RcstR. reflexivity.
-
apply Reval_nformula_dec.
- destruct t.
apply (check_inconsistent_sound Rsor QSORaddon) ; auto.
- unfold rdeduce. apply (nformula_plus_nformula_correct Rsor QSORaddon).
- now apply (cnf_normalise_correct Rsor QSORaddon).
- intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto.
- intros t w0.
unfold eval_tt.
intros.
rewrite make_impl_map with (eval := Qeval_nformula env0).
eapply RWeakChecker_sound; eauto.
tauto.
Qed.
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
[ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
]
|
