1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Micromega: A reflexive tactic using the Positivstellensatz *)
11
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
13
(************************************************************************)
15
Require Import OrderedRing.
16
Require Import RingMicromega.
17
Require Import ZCoeff.
19
Require Import ZArith.
24
repeat match goal with
25
[ id : (_ && _)%bool = true |- _ ] => destruct (andb_prop _ _ id); clear id
26
| [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id
29
Require Import EnvRing.
33
Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt.
35
constructor ; intros ; subst ; try (intuition (auto with zarith)).
38
destruct (Ztrichotomy n m) ; intuition (auto with zarith).
39
apply Zmult_lt_0_compat ; auto.
43
SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *)
44
0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
46
(fun x => x) (fun x => x) (pow_N 1 Zmult).
49
constructor ; intros ; try reflexivity.
50
apply Zeq_bool_eq ; auto.
54
apply Zeq_bool_neq ; auto.
55
apply Zle_bool_imp_le.
59
(*Definition Zeval_expr := eval_pexpr 0 Zplus Zmult Zminus Zopp (fun x => x) (fun x => Z_of_N x) (Zpower).*)
61
Fixpoint Zeval_expr (env: PolEnv Z) (e: PExpr Z) : Z :=
65
| PEadd pe1 pe2 => (Zeval_expr env pe1) + (Zeval_expr env pe2)
66
| PEsub pe1 pe2 => (Zeval_expr env pe1) - (Zeval_expr env pe2)
67
| PEmul pe1 pe2 => (Zeval_expr env pe1) * (Zeval_expr env pe2)
68
| PEopp pe1 => - (Zeval_expr env pe1)
69
| PEpow pe1 n => Zpower (Zeval_expr env pe1) (Z_of_N n)
72
Lemma Zeval_expr_simpl : forall env e,
77
| PEadd pe1 pe2 => (Zeval_expr env pe1) + (Zeval_expr env pe2)
78
| PEsub pe1 pe2 => (Zeval_expr env pe1) - (Zeval_expr env pe2)
79
| PEmul pe1 pe2 => (Zeval_expr env pe1) * (Zeval_expr env pe2)
80
| PEopp pe1 => - (Zeval_expr env pe1)
81
| PEpow pe1 n => Zpower (Zeval_expr env pe1) (Z_of_N n)
84
destruct e ; reflexivity.
88
Definition Zeval_expr' := eval_pexpr Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) (pow_N 1 Zmult).
90
Lemma ZNpower : forall r n, r ^ Z_of_N n = pow_N 1 Zmult r n.
96
replace (pow_pos Zmult r p) with (1 * (pow_pos Zmult r p)) by ring.
98
induction p; simpl ; intros ; repeat rewrite IHp ; ring.
103
Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = Zeval_expr' env e.
105
induction e ; simpl ; subst ; try congruence.
110
Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop :=
113
| OpNEq => fun x y => ~ x = y
120
Definition Zeval_formula (e: PolEnv Z) (ff : Formula Z) :=
121
let (lhs,o,rhs) := ff in Zeval_op2 o (Zeval_expr e lhs) (Zeval_expr e rhs).
123
Definition Zeval_formula' :=
124
eval_formula Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult).
126
Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
129
unfold Zeval_formula.
131
repeat rewrite Zeval_expr_compat.
132
unfold Zeval_formula'.
134
split ; destruct Fop ; simpl; auto with zarith.
139
Definition Zeval_nformula :=
140
eval_nformula 0 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult).
142
Definition Zeval_op1 (o : Op1) : Z -> Prop :=
144
| Equal => fun x : Z => x = 0
145
| NonEqual => fun x : Z => x <> 0
146
| Strict => fun x : Z => 0 < x
147
| NonStrict => fun x : Z => 0 <= x
150
Lemma Zeval_nformula_simpl : forall env f, Zeval_nformula env f = (let (p, op) := f in Zeval_op1 op (Zeval_expr env p)).
154
rewrite Zeval_expr_compat.
158
Lemma Zeval_nformula_dec : forall env d, (Zeval_nformula env d) \/ ~ (Zeval_nformula env d).
160
exact (fun env d =>eval_nformula_dec Zsor (fun x => x) (fun x => x) (pow_N 1%Z Zmult) env d).
163
Definition ZWitness := ConeMember Z.
165
Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult Zminus Zopp Zeq_bool Zle_bool.
167
Lemma ZWeakChecker_sound : forall (l : list (NFormula Z)) (cm : ZWitness),
168
ZWeakChecker l cm = true ->
169
forall env, make_impl (Zeval_nformula env) l False.
173
unfold Zeval_nformula.
174
apply (checker_nf_sound Zsor ZSORaddon l cm).
175
unfold ZWeakChecker in H.
179
Definition xnormalise (t:Formula Z) : list (NFormula Z) :=
180
let (lhs,o,rhs) := t in
183
((PEsub lhs (PEadd rhs (PEc 1))),NonStrict)::((PEsub rhs (PEadd lhs (PEc 1))),NonStrict)::nil
184
| OpNEq => (PEsub lhs rhs,Equal) :: nil
185
| OpGt => (PEsub rhs lhs,NonStrict) :: nil
186
| OpLt => (PEsub lhs rhs,NonStrict) :: nil
187
| OpGe => (PEsub rhs (PEadd lhs (PEc 1)),NonStrict) :: nil
188
| OpLe => (PEsub lhs (PEadd rhs (PEc 1)),NonStrict) :: nil
191
Require Import Tauto.
193
Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
194
List.map (fun x => x::nil) (xnormalise t).
197
Lemma normalise_correct : forall env t, eval_cnf (Zeval_nformula env) (normalise t) <-> Zeval_formula env t.
199
unfold normalise, xnormalise ; simpl ; intros env t.
200
rewrite Zeval_formula_compat.
202
destruct t as [lhs o rhs]; case_eq o ; simpl;
203
generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
204
(fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs);
205
generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
206
(fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
207
intuition (auto with zarith).
210
Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) :=
211
let (lhs,o,rhs) := t in
213
| OpEq => (PEsub lhs rhs,Equal) :: nil
214
| OpNEq => ((PEsub lhs (PEadd rhs (PEc 1))),NonStrict)::((PEsub rhs (PEadd lhs (PEc 1))),NonStrict)::nil
215
| OpGt => (PEsub lhs (PEadd rhs (PEc 1)),NonStrict) :: nil
216
| OpLt => (PEsub rhs (PEadd lhs (PEc 1)),NonStrict) :: nil
217
| OpGe => (PEsub lhs rhs,NonStrict) :: nil
218
| OpLe => (PEsub rhs lhs,NonStrict) :: nil
221
Definition negate (t:RingMicromega.Formula Z) : cnf (NFormula Z) :=
222
List.map (fun x => x::nil) (xnegate t).
224
Lemma negate_correct : forall env t, eval_cnf (Zeval_nformula env) (negate t) <-> ~ Zeval_formula env t.
226
unfold negate, xnegate ; simpl ; intros env t.
227
rewrite Zeval_formula_compat.
229
destruct t as [lhs o rhs]; case_eq o ; simpl ;
230
generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
231
(fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs);
232
generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
233
(fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ;
234
intuition (auto with zarith).
238
Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
239
@tauto_checker (Formula Z) (NFormula Z) normalise negate ZWitness ZWeakChecker f w.
241
(* To get a complete checker, the proof format has to be enriched *)
246
Definition ceiling (a b:Z) : Z :=
247
let (q,r) := Zdiv_eucl a b in
253
Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x >= b -> x >= ceiling b a.
257
generalize (Z_div_mod b a H).
258
destruct (Zdiv_eucl b a).
263
destruct (Ztrichotomy z0 0) as [ HH1 | [HH2 | HH3]]; destruct z0 ; try auto with zarith ; try discriminate.
264
assert (HH :x >= z \/ x < z) by (destruct (Ztrichotomy x z) ; auto with zarith).
266
generalize (Zmult_lt_compat_l _ _ _ H3 H1).
269
assert (HH :x >= z +1 \/ x <= z) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)).
271
assert (0 < a) by auto with zarith.
272
generalize (Zmult_lt_0_le_compat_r _ _ _ H2 H1).
274
rewrite Zmult_comm in H4.
275
rewrite (Zmult_comm z) in H4.
279
Lemma narrow_interval_upper_bound : forall a b x, a > 0 -> a * x <= b -> x <= Zdiv b a.
283
generalize (Z_div_mod b a H).
284
destruct (Zdiv_eucl b a).
289
assert (HH :x <= z \/ z <= x -1) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)).
291
assert (0 < a) by auto with zarith.
292
generalize (Zmult_lt_0_le_compat_r _ _ _ H4 H1).
295
rewrite Zmult_comm in H5.
300
(* In this case, a certificate is made of a pair of inequations, in 1 variable,
301
that do not have an integer solution.
302
=> modify the fourier elimination
304
Require Import QArith.
307
Inductive ProofTerm : Type :=
308
| RatProof : ZWitness -> ProofTerm
309
| CutProof : PExprC Z -> Q -> ZWitness -> ProofTerm -> ProofTerm
310
| EnumProof : Q -> PExprC Z -> Q -> ZWitness -> ZWitness -> list ProofTerm -> ProofTerm.
312
(* n/d <= x -> d*x - n >= 0 *)
314
Definition makeLb (v:PExpr Z) (q:Q) : NFormula Z :=
315
let (n,d) := q in (PEsub (PEmul (PEc (Zpos d)) v) (PEc n),NonStrict).
317
(* x <= n/d -> d * x <= d *)
318
Definition makeUb (v:PExpr Z) (q:Q) : NFormula Z :=
320
(PEsub (PEc n) (PEmul (PEc (Zpos d)) v), NonStrict).
322
Definition qceiling (q:Q) : Z :=
323
let (n,d) := q in ceiling n (Zpos d).
325
Definition qfloor (q:Q) : Z :=
326
let (n,d) := q in Zdiv n (Zpos d).
328
Definition makeLbCut (v:PExprC Z) (q:Q) : NFormula Z :=
329
(PEsub v (PEc (qceiling q)), NonStrict).
331
Definition neg_nformula (f : NFormula Z) :=
333
(PEopp (PEadd e (PEc 1%Z)), o).
335
Lemma neg_nformula_sound : forall env f, snd f = NonStrict ->( ~ (Zeval_nformula env (neg_nformula f)) <-> Zeval_nformula env f).
340
intros ; subst ; simpl in *.
341
split; auto with zarith.
345
Definition cutChecker (l:list (NFormula Z)) (e: PExpr Z) (lb:Q) (pf : ZWitness) : option (NFormula Z) :=
346
let (lb,lc) := (makeLb e lb,makeLbCut e lb) in
347
if ZWeakChecker (neg_nformula lb::l) pf then Some lc else None.
350
Fixpoint ZChecker (l:list (NFormula Z)) (pf : ProofTerm) {struct pf} : bool :=
352
| RatProof pf => ZWeakChecker l pf
353
| CutProof e q pf rst =>
354
match cutChecker l e q pf with
356
| Some c => ZChecker (c::l) rst
358
| EnumProof lb e ub pf1 pf2 rst =>
359
match cutChecker l e lb pf1 , cutChecker l (PEopp e) (Qopp ub) pf2 with
360
| None , _ | _ , None => false
361
| Some _ , Some _ => let (lb',ub') := (qceiling lb, Zopp (qceiling (- ub))) in
362
(fix label (pfs:list ProofTerm) :=
365
| nil => if Z_gt_dec lb ub then true else false
366
| pf::rsr => andb (ZChecker ((PEsub e (PEc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
373
Lemma ZChecker_simpl : forall (pf : ProofTerm) (l:list (NFormula Z)),
376
| RatProof pf => ZWeakChecker l pf
377
| CutProof e q pf rst =>
378
match cutChecker l e q pf with
380
| Some c => ZChecker (c::l) rst
382
| EnumProof lb e ub pf1 pf2 rst =>
383
match cutChecker l e lb pf1 , cutChecker l (PEopp e) (Qopp ub) pf2 with
384
| None , _ | _ , None => false
385
| Some _ , Some _ => let (lb',ub') := (qceiling lb, Zopp (qceiling (- ub))) in
386
(fix label (pfs:list ProofTerm) :=
389
| nil => if Z_gt_dec lb ub then true else false
390
| pf::rsr => andb (ZChecker ((PEsub e (PEc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
396
destruct pf ; reflexivity.
400
Fixpoint depth (n:nat) : ProofTerm -> option nat :=
402
| O => fun pf => None
406
| RatProof _ => Some O
407
| CutProof _ _ _ p => option_map S (depth n p)
408
| EnumProof _ _ _ _ _ l =>
410
match x , depth n pf with
411
| None , _ | _ , None => None
412
| Some n1 , Some n2 => Some (Max.max n1 n2)
414
List.fold_right f (Some O) l
418
Fixpoint bdepth (pf : ProofTerm) : nat :=
421
| CutProof _ _ _ p => S (bdepth p)
422
| EnumProof _ _ _ _ _ l => S (List.fold_right (fun pf x => Max.max (bdepth pf) x) O l)
425
Require Import Wf_nat.
427
Lemma in_bdepth : forall l a b p c c0 y, In y l -> ltof ProofTerm bdepth y (EnumProof a b p c c0 l).
438
generalize ( (fold_right
439
(fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat l)).
441
generalize (bdepth y) ; intros.
442
generalize (Max.max_l n0 n) (Max.max_r n0 n).
444
generalize (IHl a0 b p c c0 y H).
447
generalize ( (fold_right (fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat
450
generalize (Max.max_l (bdepth a) n) (Max.max_r (bdepth a) n).
454
Lemma lb_lbcut : forall env e q, Zeval_nformula env (makeLb e q) -> Zeval_nformula env (makeLbCut e q).
456
unfold makeLb, makeLbCut.
458
rewrite Zeval_nformula_simpl.
459
rewrite Zeval_nformula_simpl.
461
rewrite Zeval_expr_simpl.
462
rewrite Zeval_expr_simpl.
463
rewrite Zeval_expr_simpl.
465
rewrite Zeval_expr_simpl.
467
generalize (Zeval_expr env e).
468
rewrite Zeval_expr_simpl.
469
rewrite Zeval_expr_simpl.
472
assert ( z >= ceiling Qnum (' Qden))%Z.
473
apply narrow_interval_lower_bound.
476
destruct z ; auto with zarith.
480
Lemma cutChecker_sound : forall e lb pf l res, cutChecker l e lb pf = Some res ->
481
forall env, make_impl (Zeval_nformula env) l (Zeval_nformula env res).
486
case_eq (ZWeakChecker (neg_nformula (makeLb e lb) :: l) pf); intros ; [idtac | discriminate].
487
generalize (ZWeakChecker_sound _ _ H env).
489
inversion H0 ; subst ; clear H0.
490
apply -> make_conj_impl.
492
rewrite <- make_conj_impl in H1.
494
apply -> neg_nformula_sound ; auto.
498
generalize (lb_lbcut env e lb).
500
destruct (Zeval_nformula_dec env ((neg_nformula (makeLb e lb)))).
502
rewrite -> neg_nformula_sound in H0.
504
rewrite <- neg_nformula_sound in HH.
513
Lemma cutChecker_sound_bound : forall e lb pf l res, cutChecker l e lb pf = Some res ->
514
forall env, make_conj (Zeval_nformula env) l -> (Zeval_expr env e >= qceiling lb)%Z.
517
generalize (cutChecker_sound _ _ _ _ _ H env).
519
rewrite <- (make_conj_impl) in H1.
521
unfold cutChecker in H.
522
destruct (ZWeakChecker (neg_nformula (makeLb e lb) :: l) pf).
523
unfold makeLbCut in H.
527
rewrite Zeval_expr_compat.
534
Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (Zeval_nformula env) l False.
536
induction w using (well_founded_ind (well_founded_ltof _ bdepth)).
541
eapply ZWeakChecker_sound.
546
case_eq (cutChecker l p q z) ; intros.
547
generalize (cutChecker_sound _ _ _ _ _ H0 env).
549
assert (make_impl (Zeval_nformula env) (n::l) False).
555
rewrite <- make_conj_impl in H2.
556
rewrite <- make_conj_impl in H3.
557
rewrite <- make_conj_impl.
562
rewrite ZChecker_simpl.
563
case_eq (cutChecker l0 p q z).
565
case_eq (cutChecker l0 (PEopp p) (- q0) z0).
568
(* get the bounds of the enum *)
569
rewrite <- make_conj_impl.
571
assert (qceiling llb <= Zeval_expr env p <= - qceiling ( - uub))%Z.
572
generalize (cutChecker_sound_bound _ _ _ _ _ H0 env H3).
573
generalize (cutChecker_sound_bound _ _ _ _ _ H1 env H3).
575
rewrite Zeval_expr_simpl in H5.
579
generalize (qceiling llb) (- qceiling (- uub))%Z.
580
set (FF := (fix label (pfs : list ProofTerm) (lb ub : Z) {struct pfs} : bool :=
582
| nil => if Z_gt_dec lb ub then true else false
584
(ZChecker ((PEsub p (PEc lb), Equal) :: l0) pf &&
585
label rsr (lb + 1)%Z ub)%bool
589
assert (forall x, z1 <= x <= z2 -> exists pr,
591
ZChecker ((PEsub p (PEc x),Equal) :: l0) pr = true))%Z.
596
induction l;simpl ;intros.
597
destruct (Z_gt_dec z1 z2).
599
apply False_ind ; omega.
604
assert (HH:(x = z1 \/ z1 +1 <=x)%Z) by omega.
608
assert (z1 + 1 <= x <= z2)%Z by omega.
609
destruct (IHl _ _ H1 _ H4).
611
exists x0 ; split;auto.
613
destruct (H0 _ H4) as [pr [Hin Hcheker]].
614
assert (make_impl (Zeval_nformula env) ((PEsub p (PEc (Zeval_expr env p)),Equal) :: l0) False).
616
apply in_bdepth ; auto.
617
rewrite <- make_conj_impl in H1.
619
rewrite make_conj_cons.
621
rewrite Zeval_nformula_simpl;
623
rewrite Zeval_expr_simpl.
624
generalize (Zeval_expr env p).
626
rewrite Zeval_expr_simpl.
628
intros ; discriminate.
629
intros ; discriminate.
632
Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ProofTerm): bool :=
633
@tauto_checker (Formula Z) (NFormula Z) normalise negate ProofTerm ZChecker f w.
635
Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (Zeval_formula env) f.
638
unfold ZTautoChecker.
639
apply (tauto_checker_sound Zeval_formula Zeval_nformula).
640
apply Zeval_nformula_dec.
642
rewrite normalise_correct ; auto.
644
rewrite negate_correct ; auto.
646
apply ZChecker_sound.
653
Fixpoint map_cone (f: nat -> nat) (e:ZWitness) : ZWitness :=
655
| S_In n => S_In _ (f n)
656
| S_Ideal e cm => S_Ideal e (map_cone f cm)
658
| S_Monoid l => S_Monoid _ (List.map f l)
659
| S_Mult cm1 cm2 => S_Mult (map_cone f cm1) (map_cone f cm2)
660
| S_Add cm1 cm2 => S_Add (map_cone f cm1) (map_cone f cm2)
664
Fixpoint indexes (e:ZWitness) : list nat :=
667
| S_Ideal e cm => indexes cm
670
| S_Mult cm1 cm2 => (indexes cm1)++ (indexes cm2)
671
| S_Add cm1 cm2 => (indexes cm1)++ (indexes cm2)
675
(** To ease bindings from ml code **)
676
(*Definition varmap := Quote.varmap.*)
677
Definition make_impl := Refl.make_impl.
678
Definition make_conj := Refl.make_conj.
682
(*Definition varmap_type := VarMap.t Z. *)
683
Definition env := PolEnv Z.
684
Definition node := @VarMap.Node Z.
685
Definition empty := @VarMap.Empty Z.
686
Definition leaf := @VarMap.Leaf Z.
688
Definition coneMember := ZWitness.
690
Definition eval := Zeval_formula.
692
Definition prod_pos_nat := prod positive nat.
697
Definition n_of_Z (z:Z) : BinNat.N :=
added
removed
contrib/micromega/ZMicromega.v
