1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
(************************************************************************)
(* 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.
Declare ML Module "micromega_plugin".
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.
|
