diff options
Diffstat (limited to 'contrib/micromega/ZMicromega.v')
| -rw-r--r-- | contrib/micromega/ZMicromega.v | 714 |
1 files changed, 714 insertions, 0 deletions
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v new file mode 100644 index 00000000..94c83f73 --- /dev/null +++ b/contrib/micromega/ZMicromega.v @@ -0,0 +1,714 @@ +(************************************************************************) +(* 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 ZCoeff. +Require Import Refl. +Require Import ZArith. +Require Import List. +Require Import Bool. + +Ltac flatten_bool := + repeat match goal with + [ id : (_ && _)%bool = true |- _ ] => destruct (andb_prop _ _ id); clear id + | [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id + end. + +Require Import EnvRing. + +Open Scope Z_scope. + +Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt. +Proof. + constructor ; intros ; subst ; try (intuition (auto with zarith)). + apply Zsth. + apply Zth. + destruct (Ztrichotomy n m) ; intuition (auto with zarith). + apply Zmult_lt_0_compat ; auto. +Qed. + +Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y. +Proof. + red ; intros. + subst. + unfold Zeq_bool in H. + rewrite Zcompare_refl in H. + discriminate. +Qed. + +Lemma ZSORaddon : + SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *) + 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) + Zeq_bool Zle_bool + (fun x => x) (fun x => x) (pow_N 1 Zmult). +Proof. + constructor. + constructor ; intros ; try reflexivity. + apply Zeqb_ok ; auto. + constructor. + reflexivity. + intros x y. + apply Zeq_bool_neq ; auto. + apply Zle_bool_imp_le. +Qed. + + +(*Definition Zeval_expr := eval_pexpr 0 Zplus Zmult Zminus Zopp (fun x => x) (fun x => Z_of_N x) (Zpower).*) + +Fixpoint Zeval_expr (env: PolEnv Z) (e: PExpr Z) : Z := + match e with + | PEc c => c + | PEX j => env j + | PEadd pe1 pe2 => (Zeval_expr env pe1) + (Zeval_expr env pe2) + | PEsub pe1 pe2 => (Zeval_expr env pe1) - (Zeval_expr env pe2) + | PEmul pe1 pe2 => (Zeval_expr env pe1) * (Zeval_expr env pe2) + | PEopp pe1 => - (Zeval_expr env pe1) + | PEpow pe1 n => Zpower (Zeval_expr env pe1) (Z_of_N n) + end. + +Lemma Zeval_expr_simpl : forall env e, + Zeval_expr env e = + match e with + | PEc c => c + | PEX j => env j + | PEadd pe1 pe2 => (Zeval_expr env pe1) + (Zeval_expr env pe2) + | PEsub pe1 pe2 => (Zeval_expr env pe1) - (Zeval_expr env pe2) + | PEmul pe1 pe2 => (Zeval_expr env pe1) * (Zeval_expr env pe2) + | PEopp pe1 => - (Zeval_expr env pe1) + | PEpow pe1 n => Zpower (Zeval_expr env pe1) (Z_of_N n) + end. +Proof. + destruct e ; reflexivity. +Qed. + + +Definition Zeval_expr' := eval_pexpr Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) (pow_N 1 Zmult). + +Lemma ZNpower : forall r n, r ^ Z_of_N n = pow_N 1 Zmult r n. +Proof. + destruct n. + reflexivity. + simpl. + unfold Zpower_pos. + replace (pow_pos Zmult r p) with (1 * (pow_pos Zmult r p)) by ring. + generalize 1. + induction p; simpl ; intros ; repeat rewrite IHp ; ring. +Qed. + + + +Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = Zeval_expr' env e. +Proof. + induction e ; simpl ; subst ; try congruence. + rewrite IHe. + apply ZNpower. +Qed. + +Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop := +match o with +| OpEq => @eq Z +| OpNEq => fun x y => ~ x = y +| OpLe => Zle +| OpGe => Zge +| OpLt => Zlt +| OpGt => Zgt +end. + +Definition Zeval_formula (e: PolEnv Z) (ff : Formula Z) := + let (lhs,o,rhs) := ff in Zeval_op2 o (Zeval_expr e lhs) (Zeval_expr e rhs). + +Definition Zeval_formula' := + eval_formula Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult). + +Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f. +Proof. + intros. + unfold Zeval_formula. + destruct f. + repeat rewrite Zeval_expr_compat. + unfold Zeval_formula'. + unfold Zeval_expr'. + split ; destruct Fop ; simpl; auto with zarith. +Qed. + + + +Definition Zeval_nformula := + eval_nformula 0 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult). + +Definition Zeval_op1 (o : Op1) : Z -> Prop := +match o with +| Equal => fun x : Z => x = 0 +| NonEqual => fun x : Z => x <> 0 +| Strict => fun x : Z => 0 < x +| NonStrict => fun x : Z => 0 <= x +end. + +Lemma Zeval_nformula_simpl : forall env f, Zeval_nformula env f = (let (p, op) := f in Zeval_op1 op (Zeval_expr env p)). +Proof. + intros. + destruct f. + rewrite Zeval_expr_compat. + reflexivity. +Qed. + +Lemma Zeval_nformula_dec : forall env d, (Zeval_nformula env d) \/ ~ (Zeval_nformula env d). +Proof. + exact (fun env d =>eval_nformula_dec Zsor (fun x => x) (fun x => x) (pow_N 1%Z Zmult) env d). +Qed. + +Definition ZWitness := ConeMember Z. + +Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult Zminus Zopp Zeq_bool Zle_bool. + +Lemma ZWeakChecker_sound : forall (l : list (NFormula Z)) (cm : ZWitness), + ZWeakChecker l cm = true -> + forall env, make_impl (Zeval_nformula env) l False. +Proof. + intros l cm H. + intro. + unfold Zeval_nformula. + apply (checker_nf_sound Zsor ZSORaddon l cm). + unfold ZWeakChecker in H. + exact H. +Qed. + +Definition xnormalise (t:Formula Z) : list (NFormula Z) := + let (lhs,o,rhs) := t in + match o with + | OpEq => + ((PEsub lhs (PEadd rhs (PEc 1))),NonStrict)::((PEsub rhs (PEadd lhs (PEc 1))),NonStrict)::nil + | OpNEq => (PEsub lhs rhs,Equal) :: nil + | OpGt => (PEsub rhs lhs,NonStrict) :: nil + | OpLt => (PEsub lhs rhs,NonStrict) :: nil + | OpGe => (PEsub rhs (PEadd lhs (PEc 1)),NonStrict) :: nil + | OpLe => (PEsub lhs (PEadd rhs (PEc 1)),NonStrict) :: nil + end. + +Require Import Tauto. + +Definition normalise (t:Formula Z) : cnf (NFormula Z) := + List.map (fun x => x::nil) (xnormalise t). + + +Lemma normalise_correct : forall env t, eval_cnf (Zeval_nformula env) (normalise t) <-> Zeval_formula env t. +Proof. + unfold normalise, xnormalise ; simpl ; intros env t. + rewrite Zeval_formula_compat. + unfold eval_cnf. + destruct t as [lhs o rhs]; case_eq o ; simpl; + generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) + (fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs); + generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) + (fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst; + intuition (auto with zarith). +Qed. + +Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := + let (lhs,o,rhs) := t in + match o with + | OpEq => (PEsub lhs rhs,Equal) :: nil + | OpNEq => ((PEsub lhs (PEadd rhs (PEc 1))),NonStrict)::((PEsub rhs (PEadd lhs (PEc 1))),NonStrict)::nil + | OpGt => (PEsub lhs (PEadd rhs (PEc 1)),NonStrict) :: nil + | OpLt => (PEsub rhs (PEadd lhs (PEc 1)),NonStrict) :: nil + | OpGe => (PEsub lhs rhs,NonStrict) :: nil + | OpLe => (PEsub rhs lhs,NonStrict) :: nil + end. + +Definition negate (t:RingMicromega.Formula Z) : cnf (NFormula Z) := + List.map (fun x => x::nil) (xnegate t). + +Lemma negate_correct : forall env t, eval_cnf (Zeval_nformula env) (negate t) <-> ~ Zeval_formula env t. +Proof. + unfold negate, xnegate ; simpl ; intros env t. + rewrite Zeval_formula_compat. + unfold eval_cnf. + destruct t as [lhs o rhs]; case_eq o ; simpl ; + generalize ( eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) + (fun x : BinNat.N => x) (pow_N 1 Zmult) env lhs); + generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) + (fun x : BinNat.N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; + intuition (auto with zarith). +Qed. + + +Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := + @tauto_checker (Formula Z) (NFormula Z) normalise negate ZWitness ZWeakChecker f w. + +(* To get a complete checker, the proof format has to be enriched *) + +Require Import Zdiv. +Open Scope Z_scope. + +Definition ceiling (a b:Z) : Z := + let (q,r) := Zdiv_eucl a b in + match r with + | Z0 => q + | _ => q + 1 + end. + +Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x >= b -> x >= ceiling b a. +Proof. + unfold ceiling. + intros. + generalize (Z_div_mod b a H). + destruct (Zdiv_eucl b a). + intros. + destruct H1. + destruct H2. + subst. + destruct (Ztrichotomy z0 0) as [ HH1 | [HH2 | HH3]]; destruct z0 ; try auto with zarith ; try discriminate. + assert (HH :x >= z \/ x < z) by (destruct (Ztrichotomy x z) ; auto with zarith). + destruct HH ;auto. + generalize (Zmult_lt_compat_l _ _ _ H3 H1). + auto with zarith. + clear H2. + assert (HH :x >= z +1 \/ x <= z) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)). + destruct HH ;auto. + assert (0 < a) by auto with zarith. + generalize (Zmult_lt_0_le_compat_r _ _ _ H2 H1). + intros. + rewrite Zmult_comm in H4. + rewrite (Zmult_comm z) in H4. + auto with zarith. +Qed. + +Lemma narrow_interval_upper_bound : forall a b x, a > 0 -> a * x <= b -> x <= Zdiv b a. +Proof. + unfold Zdiv. + intros. + generalize (Z_div_mod b a H). + destruct (Zdiv_eucl b a). + intros. + destruct H1. + destruct H2. + subst. + assert (HH :x <= z \/ z <= x -1) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)). + destruct HH ;auto. + assert (0 < a) by auto with zarith. + generalize (Zmult_lt_0_le_compat_r _ _ _ H4 H1). + intros. + ring_simplify in H5. + rewrite Zmult_comm in H5. + auto with zarith. +Qed. + + +(* In this case, a certificate is made of a pair of inequations, in 1 variable, + that do not have an integer solution. + => modify the fourier elimination + *) +Require Import QArith. + + +Inductive ProofTerm : Type := +| RatProof : ZWitness -> ProofTerm +| CutProof : PExprC Z -> Q -> ZWitness -> ProofTerm -> ProofTerm +| EnumProof : Q -> PExprC Z -> Q -> ZWitness -> ZWitness -> list ProofTerm -> ProofTerm. + +(* n/d <= x -> d*x - n >= 0 *) + +Definition makeLb (v:PExpr Z) (q:Q) : NFormula Z := + let (n,d) := q in (PEsub (PEmul (PEc (Zpos d)) v) (PEc n),NonStrict). + +(* x <= n/d -> d * x <= d *) +Definition makeUb (v:PExpr Z) (q:Q) : NFormula Z := + let (n,d) := q in + (PEsub (PEc n) (PEmul (PEc (Zpos d)) v), NonStrict). + +Definition qceiling (q:Q) : Z := + let (n,d) := q in ceiling n (Zpos d). + +Definition qfloor (q:Q) : Z := + let (n,d) := q in Zdiv n (Zpos d). + +Definition makeLbCut (v:PExprC Z) (q:Q) : NFormula Z := + (PEsub v (PEc (qceiling q)), NonStrict). + +Definition neg_nformula (f : NFormula Z) := + let (e,o) := f in + (PEopp (PEadd e (PEc 1%Z)), o). + +Lemma neg_nformula_sound : forall env f, snd f = NonStrict ->( ~ (Zeval_nformula env (neg_nformula f)) <-> Zeval_nformula env f). +Proof. + unfold neg_nformula. + destruct f. + simpl. + intros ; subst ; simpl in *. + split; auto with zarith. +Qed. + + +Definition cutChecker (l:list (NFormula Z)) (e: PExpr Z) (lb:Q) (pf : ZWitness) : option (NFormula Z) := + let (lb,lc) := (makeLb e lb,makeLbCut e lb) in + if ZWeakChecker (neg_nformula lb::l) pf then Some lc else None. + + +Fixpoint ZChecker (l:list (NFormula Z)) (pf : ProofTerm) {struct pf} : bool := + match pf with + | RatProof pf => ZWeakChecker l pf + | CutProof e q pf rst => + match cutChecker l e q pf with + | None => false + | Some c => ZChecker (c::l) rst + end + | EnumProof lb e ub pf1 pf2 rst => + match cutChecker l e lb pf1 , cutChecker l (PEopp e) (Qopp ub) pf2 with + | None , _ | _ , None => false + | Some _ , Some _ => let (lb',ub') := (qceiling lb, Zopp (qceiling (- ub))) in + (fix label (pfs:list ProofTerm) := + fun lb ub => + match pfs with + | nil => if Z_gt_dec lb ub then true else false + | pf::rsr => andb (ZChecker ((PEsub e (PEc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) + end) + rst lb' ub' + end + end. + + +Lemma ZChecker_simpl : forall (pf : ProofTerm) (l:list (NFormula Z)), + ZChecker l pf = + match pf with + | RatProof pf => ZWeakChecker l pf + | CutProof e q pf rst => + match cutChecker l e q pf with + | None => false + | Some c => ZChecker (c::l) rst + end + | EnumProof lb e ub pf1 pf2 rst => + match cutChecker l e lb pf1 , cutChecker l (PEopp e) (Qopp ub) pf2 with + | None , _ | _ , None => false + | Some _ , Some _ => let (lb',ub') := (qceiling lb, Zopp (qceiling (- ub))) in + (fix label (pfs:list ProofTerm) := + fun lb ub => + match pfs with + | nil => if Z_gt_dec lb ub then true else false + | pf::rsr => andb (ZChecker ((PEsub e (PEc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) + end) + rst lb' ub' + end + end. +Proof. + destruct pf ; reflexivity. +Qed. + +(* +Fixpoint depth (n:nat) : ProofTerm -> option nat := + match n with + | O => fun pf => None + | S n => + fun pf => + match pf with + | RatProof _ => Some O + | CutProof _ _ _ p => option_map S (depth n p) + | EnumProof _ _ _ _ _ l => + let f := fun pf x => + match x , depth n pf with + | None , _ | _ , None => None + | Some n1 , Some n2 => Some (Max.max n1 n2) + end in + List.fold_right f (Some O) l + end + end. +*) +Fixpoint bdepth (pf : ProofTerm) : nat := + match pf with + | RatProof _ => O + | CutProof _ _ _ p => S (bdepth p) + | EnumProof _ _ _ _ _ l => S (List.fold_right (fun pf x => Max.max (bdepth pf) x) O l) + end. + +Require Import Wf_nat. + +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). +Proof. + induction l. + simpl. + tauto. + simpl. + intros. + destruct H. + subst. + unfold ltof. + simpl. + generalize ( (fold_right + (fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat l)). + intros. + generalize (bdepth y) ; intros. + generalize (Max.max_l n0 n) (Max.max_r n0 n). + omega. + generalize (IHl a0 b p c c0 y H). + unfold ltof. + simpl. + generalize ( (fold_right (fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat + l)). + intros. + generalize (Max.max_l (bdepth a) n) (Max.max_r (bdepth a) n). + omega. +Qed. + +Lemma lb_lbcut : forall env e q, Zeval_nformula env (makeLb e q) -> Zeval_nformula env (makeLbCut e q). +Proof. + unfold makeLb, makeLbCut. + destruct q. + rewrite Zeval_nformula_simpl. + rewrite Zeval_nformula_simpl. + unfold Zeval_op1. + rewrite Zeval_expr_simpl. + rewrite Zeval_expr_simpl. + rewrite Zeval_expr_simpl. + intro. + rewrite Zeval_expr_simpl. + revert H. + generalize (Zeval_expr env e). + rewrite Zeval_expr_simpl. + rewrite Zeval_expr_simpl. + unfold qceiling. + intros. + assert ( z >= ceiling Qnum (' Qden))%Z. + apply narrow_interval_lower_bound. + compute. + reflexivity. + destruct z ; auto with zarith. + auto with zarith. +Qed. + +Lemma cutChecker_sound : forall e lb pf l res, cutChecker l e lb pf = Some res -> + forall env, make_impl (Zeval_nformula env) l (Zeval_nformula env res). +Proof. + unfold cutChecker. + intros. + revert H. + case_eq (ZWeakChecker (neg_nformula (makeLb e lb) :: l) pf); intros ; [idtac | discriminate]. + generalize (ZWeakChecker_sound _ _ H env). + intros. + inversion H0 ; subst ; clear H0. + apply -> make_conj_impl. + simpl in H1. + rewrite <- make_conj_impl in H1. + intros. + apply -> neg_nformula_sound ; auto. + red ; intros. + apply H1 ; auto. + clear H H1 H0. + generalize (lb_lbcut env e lb). + intros. + destruct (Zeval_nformula_dec env ((neg_nformula (makeLb e lb)))). + auto. + rewrite -> neg_nformula_sound in H0. + assert (HH := H H0). + rewrite <- neg_nformula_sound in HH. + tauto. + reflexivity. + unfold makeLb. + destruct lb. + reflexivity. +Qed. + + +Lemma cutChecker_sound_bound : forall e lb pf l res, cutChecker l e lb pf = Some res -> + forall env, make_conj (Zeval_nformula env) l -> (Zeval_expr env e >= qceiling lb)%Z. +Proof. + intros. + generalize (cutChecker_sound _ _ _ _ _ H env). + intros. + rewrite <- (make_conj_impl) in H1. + generalize (H1 H0). + unfold cutChecker in H. + destruct (ZWeakChecker (neg_nformula (makeLb e lb) :: l) pf). + unfold makeLbCut in H. + inversion H ; subst. + clear H. + simpl. + rewrite Zeval_expr_compat. + unfold Zeval_expr'. + auto with zarith. + discriminate. +Qed. + + +Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (Zeval_nformula env) l False. +Proof. + induction w using (well_founded_ind (well_founded_ltof _ bdepth)). + destruct w. + (* RatProof *) + simpl. + intros. + eapply ZWeakChecker_sound. + apply H0. + (* CutProof *) + simpl. + intro. + case_eq (cutChecker l p q z) ; intros. + generalize (cutChecker_sound _ _ _ _ _ H0 env). + intro. + assert (make_impl (Zeval_nformula env) (n::l) False). + eapply (H w) ; auto. + unfold ltof. + simpl. + auto with arith. + simpl in H3. + rewrite <- make_conj_impl in H2. + rewrite <- make_conj_impl in H3. + rewrite <- make_conj_impl. + tauto. + discriminate. + (* EnumProof *) + intro. + rewrite ZChecker_simpl. + case_eq (cutChecker l0 p q z). + rename q into llb. + case_eq (cutChecker l0 (PEopp p) (- q0) z0). + intros. + rename q0 into uub. + (* get the bounds of the enum *) + rewrite <- make_conj_impl. + intro. + assert (qceiling llb <= Zeval_expr env p <= - qceiling ( - uub))%Z. + generalize (cutChecker_sound_bound _ _ _ _ _ H0 env H3). + generalize (cutChecker_sound_bound _ _ _ _ _ H1 env H3). + intros. + rewrite Zeval_expr_simpl in H5. + auto with zarith. + clear H0 H1. + revert H2 H3 H4. + generalize (qceiling llb) (- qceiling (- uub))%Z. + set (FF := (fix label (pfs : list ProofTerm) (lb ub : Z) {struct pfs} : bool := + match pfs with + | nil => if Z_gt_dec lb ub then true else false + | pf :: rsr => + (ZChecker ((PEsub p (PEc lb), Equal) :: l0) pf && + label rsr (lb + 1)%Z ub)%bool + end)). + intros z1 z2. + intros. + assert (forall x, z1 <= x <= z2 -> exists pr, + (In pr l /\ + ZChecker ((PEsub p (PEc x),Equal) :: l0) pr = true))%Z. + clear H. + revert H2. + clear H4. + revert z1 z2. + induction l;simpl ;intros. + destruct (Z_gt_dec z1 z2). + intros. + apply False_ind ; omega. + discriminate. + intros. + simpl in H2. + flatten_bool. + assert (HH:(x = z1 \/ z1 +1 <=x)%Z) by omega. + destruct HH. + subst. + exists a ; auto. + assert (z1 + 1 <= x <= z2)%Z by omega. + destruct (IHl _ _ H1 _ H4). + destruct H5. + exists x0 ; split;auto. + (*/asser *) + destruct (H0 _ H4) as [pr [Hin Hcheker]]. + assert (make_impl (Zeval_nformula env) ((PEsub p (PEc (Zeval_expr env p)),Equal) :: l0) False). + apply (H pr);auto. + apply in_bdepth ; auto. + rewrite <- make_conj_impl in H1. + apply H1. + rewrite make_conj_cons. + split ;auto. + rewrite Zeval_nformula_simpl; + unfold Zeval_op1; + rewrite Zeval_expr_simpl. + generalize (Zeval_expr env p). + intros. + rewrite Zeval_expr_simpl. + auto with zarith. + intros ; discriminate. + intros ; discriminate. +Qed. + +Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ProofTerm): bool := + @tauto_checker (Formula Z) (NFormula Z) normalise negate ProofTerm ZChecker f w. + +Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (Zeval_formula env) f. +Proof. + intros f w. + unfold ZTautoChecker. + apply (tauto_checker_sound Zeval_formula Zeval_nformula). + apply Zeval_nformula_dec. + intros env t. + rewrite normalise_correct ; auto. + intros env t. + rewrite negate_correct ; auto. + intros t w0. + apply ZChecker_sound. +Qed. + + +Open Scope Z_scope. + + +Fixpoint map_cone (f: nat -> nat) (e:ZWitness) : ZWitness := + match e with + | S_In n => S_In _ (f n) + | S_Ideal e cm => S_Ideal e (map_cone f cm) + | S_Square _ => e + | S_Monoid l => S_Monoid _ (List.map f l) + | S_Mult cm1 cm2 => S_Mult (map_cone f cm1) (map_cone f cm2) + | S_Add cm1 cm2 => S_Add (map_cone f cm1) (map_cone f cm2) + | _ => e + end. + +Fixpoint indexes (e:ZWitness) : list nat := + match e with + | S_In n => n::nil + | S_Ideal e cm => indexes cm + | S_Square e => nil + | S_Monoid l => l + | S_Mult cm1 cm2 => (indexes cm1)++ (indexes cm2) + | S_Add cm1 cm2 => (indexes cm1)++ (indexes cm2) + | _ => nil + end. + +(** To ease bindings from ml code **) +(*Definition varmap := Quote.varmap.*) +Definition make_impl := Refl.make_impl. +Definition make_conj := Refl.make_conj. + +Require VarMap. + +(*Definition varmap_type := VarMap.t Z. *) +Definition env := PolEnv Z. +Definition node := @VarMap.Node Z. +Definition empty := @VarMap.Empty Z. +Definition leaf := @VarMap.Leaf Z. + +Definition coneMember := ZWitness. + +Definition eval := Zeval_formula. + +Definition prod_pos_nat := prod positive nat. + +Require Import Int. + + +Definition n_of_Z (z:Z) : BinNat.N := + match z with + | Z0 => N0 + | Zpos p => Npos p + | Zneg p => N0 + end. + + + |