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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
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.
|
