aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-07-30 21:30:12 +0000
committerGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-07-30 21:30:12 +0000
commit91618b50da9508a75c2c43c42a4794a06b83a3ee (patch)
tree46718c951c544063afc0fb9935a992c1dbb285a2
parenta7c0fe84f441c4b624828a2d34459ddf78e216cf (diff)
micromega : Better parsing of formulae - smaller proof terms for Z - redesign of proof cache
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--plugins/micromega/MExtraction.v10
-rw-r--r--plugins/micromega/Psatz.v5
-rw-r--r--plugins/micromega/QMicromega.v38
-rw-r--r--plugins/micromega/RMicromega.v25
-rw-r--r--plugins/micromega/RingMicromega.v854
-rw-r--r--plugins/micromega/Tauto.v2
-rw-r--r--plugins/micromega/ZMicromega.v1053
-rw-r--r--plugins/micromega/certificate.ml122
-rw-r--r--plugins/micromega/coq_micromega.ml446
-rw-r--r--plugins/micromega/csdpcert.ml45
-rw-r--r--plugins/micromega/g_micromega.ml48
-rw-r--r--plugins/micromega/mfourier.ml2
-rw-r--r--plugins/micromega/micromega.ml814
-rw-r--r--plugins/micromega/micromega.mli179
-rw-r--r--plugins/micromega/micromega_plugin.mllib1
-rw-r--r--plugins/micromega/mutils.ml63
-rw-r--r--plugins/micromega/persistent_cache.ml175
-rw-r--r--plugins/micromega/sos.ml15
18 files changed, 2504 insertions, 1353 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index b4b40ca73..7b2c0231f 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -16,6 +16,7 @@
Require Import ZMicromega.
Require Import QMicromega.
+Require Import RMicromega.
Require Import VarMap.
Require Import RingMicromega.
Require Import NArith.
@@ -37,5 +38,10 @@ Extract Inductive sumor => option [ Some None ].
Extract Inlined Constant andb => "(&&)".
Extraction "micromega.ml"
- List.map simpl_cone map_cone indexes
- n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find.
+ List.map simpl_cone (*map_cone indexes*)
+ denorm
+ n_of_Z Nnat.N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a3be56207..9e675165f 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -74,3 +74,8 @@ Ltac lia :=
intros __wit __varmap __ff ;
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index f02209459..b266a1ab8 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -17,7 +17,7 @@ Require Import RingMicromega.
Require Import Refl.
Require Import QArith.
Require Import Qfield.
-Declare ML Module "micromega_plugin".
+(*Declare ML Module "micromega_plugin".*)
Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt.
Proof.
@@ -105,6 +105,7 @@ Qed.
Lemma Qeval_expr_compat : forall env e, Qeval_expr env e = Qeval_expr' env e.
Proof.
induction e ; simpl ; subst ; try congruence.
+ reflexivity.
rewrite IHe.
apply QNpower.
Qed.
@@ -137,9 +138,8 @@ Proof.
Qed.
-
Definition Qeval_nformula :=
- eval_nformula 0 Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult).
+ eval_nformula 0 Qplus Qmult Qeq Qle Qlt (fun x => x) .
Definition Qeval_op1 (o : Op1) : Q -> Prop :=
match o with
@@ -149,22 +149,15 @@ match o with
| 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).
+ exact (fun env d =>eval_nformula_dec Qsor (fun x => x) env d).
Qed.
-Definition QWitness := ConeMember Q.
+Definition QWitness := Psatz Q.
-Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qminus Qopp Qeq_bool Qle_bool.
+Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool.
Require Import List.
@@ -182,8 +175,15 @@ Qed.
Require Import Tauto.
+Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
+Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
+
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.
+ @tauto_checker (Formula Q) (NFormula Q)
+ Qnormalise
+ Qnegate QWitness QWeakChecker f w.
+
+
Lemma QTautoChecker_sound : forall f w, QTautoChecker f w = true -> forall env, eval_f (Qeval_formula env) f.
Proof.
@@ -191,10 +191,12 @@ Proof.
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. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_normalise_correct Qsor QSORaddon).
+ intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_negate_correct Qsor QSORaddon).
intros t w0.
apply QWeakChecker_sound.
Qed.
-
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 70786a057..2e8c3daec 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -17,7 +17,7 @@ Require Import RingMicromega.
Require Import Refl.
Require Import Raxioms RIneq Rpow_def DiscrR.
Require Setoid.
-Declare ML Module "micromega_plugin".
+(*Declare ML Module "micromega_plugin".*)
Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R).
Proof.
@@ -61,7 +61,6 @@ Proof.
Qed.
Require ZMicromega.
-
(* R with coeffs in Z *)
Lemma RZSORaddon :
@@ -128,17 +127,17 @@ Proof.
Qed.
Definition Reval_nformula :=
- eval_nformula 0 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow.
+ eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt IZR.
Lemma Reval_nformula_dec : forall env d, (Reval_nformula env d) \/ ~ (Reval_nformula env d).
Proof.
- exact (fun env d =>eval_nformula_dec Rsor IZR Nnat.nat_of_N pow env d).
+ exact (fun env d =>eval_nformula_dec Rsor IZR env d).
Qed.
-Definition RWitness := ConeMember Z.
+Definition RWitness := Psatz Z.
-Definition RWeakChecker := check_normalised_formulas 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Zle_bool.
+Definition RWeakChecker := check_normalised_formulas 0%Z 1%Z Zplus Zmult Zeq_bool Zle_bool.
Require Import List.
@@ -156,8 +155,13 @@ Qed.
Require Import Tauto.
+Definition Rnormalise := @cnf_normalise Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
+Definition Rnegate := @cnf_negate Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
+
Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness) : bool :=
- @tauto_checker (Formula Z) (NFormula Z) (@cnf_normalise Z) (@cnf_negate Z) RWitness RWeakChecker f w.
+ @tauto_checker (Formula Z) (NFormula Z)
+ Rnormalise Rnegate
+ RWitness RWeakChecker f w.
Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_f (Reval_formula env) f.
Proof.
@@ -166,10 +170,13 @@ Proof.
apply (tauto_checker_sound Reval_formula Reval_nformula).
apply Reval_nformula_dec.
intros. rewrite Reval_formula_compat.
- unfold Reval_formula'. now apply (cnf_normalise_correct Rsor).
- intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor).
+ unfold Reval_formula'. now apply (cnf_normalise_correct Rsor RZSORaddon).
+ intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor RZSORaddon).
intros t w0.
apply RWeakChecker_sound.
Qed.
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index c093d7ca0..5b89579c8 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -20,7 +20,6 @@ Require Import Bool.
Require Import OrderedRing.
Require Import Refl.
-
Set Implicit Arguments.
Import OrderedRingSyntax.
@@ -131,6 +130,7 @@ intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
destruct (ceqb x y); now try discriminate.
Qed.
+
Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
Proof.
intros x y H. unfold cltb in H. apply andb_prop in H. destruct H as [H1 H2].
@@ -139,69 +139,10 @@ Qed.
(* Begin Micromega *)
-Definition PExprC := PExpr C. (* arbitrary expressions built from +, *, - *)
Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
-(*****)
-(*Definition Env := Env R. (* For interpreting PExprC *)*)
Definition PolEnv := Env R. (* For interpreting PolC *)
-(*****)
-(*Definition Env := list R.
-Definition PolEnv := list R.*)
-(*****)
-
-(* What benefit do we get, in the case of EnvRing, from defining eval_pexpr
-explicitely below and not through PEeval, as the following lemma says? The
-function eval_pexpr seems to be a straightforward special case of PEeval
-when the environment (i.e., the second last argument of PEeval) of type
-off_map (which is (option positive * t)) is (None, env). *)
-
-(*****)
-Fixpoint eval_pexpr (l : PolEnv) (pe : PExprC) {struct pe} : R :=
-match pe with
-| PEc c => phi c
-| PEX j => l j
-| PEadd pe1 pe2 => (eval_pexpr l pe1) + (eval_pexpr l pe2)
-| PEsub pe1 pe2 => (eval_pexpr l pe1) - (eval_pexpr l pe2)
-| PEmul pe1 pe2 => (eval_pexpr l pe1) * (eval_pexpr l pe2)
-| PEopp pe1 => - (eval_pexpr l pe1)
-| PEpow pe1 n => rpow (eval_pexpr l pe1) (pow_phi n)
-end.
-
-
-Lemma eval_pexpr_simpl : forall (l : PolEnv) (pe : PExprC),
- eval_pexpr l pe =
- match pe with
- | PEc c => phi c
- | PEX j => l j
- | PEadd pe1 pe2 => (eval_pexpr l pe1) + (eval_pexpr l pe2)
- | PEsub pe1 pe2 => (eval_pexpr l pe1) - (eval_pexpr l pe2)
- | PEmul pe1 pe2 => (eval_pexpr l pe1) * (eval_pexpr l pe2)
- | PEopp pe1 => - (eval_pexpr l pe1)
- | PEpow pe1 n => rpow (eval_pexpr l pe1) (pow_phi n)
- end.
-Proof.
- intros ; destruct pe ; reflexivity.
-Qed.
-
-
-
-Lemma eval_pexpr_PEeval : forall (env : PolEnv) (pe : PExprC),
- eval_pexpr env pe =
- PEeval rplus rtimes rminus ropp phi pow_phi rpow env pe.
-Proof.
-induction pe; simpl; intros.
-reflexivity.
-reflexivity.
-rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
-rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
-rewrite <- IHpe1; rewrite <- IHpe2; reflexivity.
-rewrite <- IHpe; reflexivity.
-rewrite <- IHpe; reflexivity.
-Qed.
-(*****)
-(*Definition eval_pexpr : Env -> PExprC -> R :=
- PEeval 0 rplus rtimes rminus ropp phi pow_phi rpow.*)
-(*****)
+Definition eval_pol (env : PolEnv) (p:PolC) : R :=
+ Pphi 0 rplus rtimes phi env p.
Inductive Op1 : Set := (* relations with 0 *)
| Equal (* == 0 *)
@@ -209,7 +150,7 @@ Inductive Op1 : Set := (* relations with 0 *)
| Strict (* > 0 *)
| NonStrict (* >= 0 *).
-Definition NFormula := (PExprC * Op1)%type. (* normalized formula *)
+Definition NFormula := (PolC * Op1)%type. (* normalized formula *)
Definition eval_op1 (o : Op1) : R -> Prop :=
match o with
@@ -220,341 +161,378 @@ match o with
end.
Definition eval_nformula (env : PolEnv) (f : NFormula) : Prop :=
-let (p, op) := f in eval_op1 op (eval_pexpr env p).
+let (p, op) := f in eval_op1 op (eval_pol env p).
-Definition OpMult (o o' : Op1) : Op1 :=
-match o with
-| Equal => Equal
-| NonStrict => NonStrict (* (OpMult NonStrict Equal) could be defined as Equal *)
-| Strict => o'
-| NonEqual => NonEqual (* does not matter what we return here; see the following lemmas *)
-end.
+(** Rule of "signs" for addition and multiplication.
+ An arbitrary result is coded buy None. *)
-Definition OpAdd (o o': Op1) : Op1 :=
+Definition OpMult (o o' : Op1) : option Op1 :=
match o with
-| Equal => o'
-| NonStrict =>
+| Equal => Some Equal
+| NonStrict =>
match o' with
- | Strict => Strict
- | _ => NonStrict
+ | Equal => Some Equal
+ | NonEqual => None
+ | Strict => Some NonStrict
+ | NonStrict => Some NonStrict
end
-| Strict => Strict
-| NonEqual => NonEqual (* does not matter what we return here *)
+| Strict => match o' with
+ | NonEqual => None
+ | _ => Some o'
+ end
+| NonEqual => match o' with
+ | Equal => Some Equal
+ | NonEqual => Some NonEqual
+ | _ => None
+ end
end.
-Lemma OpMultNonEqual :
- forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpMult o o' <> NonEqual.
-Proof.
-intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
-try (intro H; apply H1; reflexivity);
-try (intro H; apply H2; reflexivity).
-Qed.
+Definition OpAdd (o o': Op1) : option Op1 :=
+ match o with
+ | Equal => Some o'
+ | NonStrict =>
+ match o' with
+ | Strict => Some Strict
+ | NonEqual => None
+ | _ => Some NonStrict
+ end
+ | Strict => match o' with
+ | NonEqual => None
+ | _ => Some Strict
+ end
+ | NonEqual => match o' with
+ | Equal => Some NonEqual
+ | _ => None
+ end
+ end.
-Lemma OpAdd_NonEqual :
- forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpAdd o o' <> NonEqual.
-Proof.
-intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
-try (intro H; apply H1; reflexivity);
-try (intro H; apply H2; reflexivity).
-Qed.
Lemma OpMult_sound :
- forall (o o' : Op1) (x y : R), o <> NonEqual -> o' <> NonEqual ->
- eval_op1 o x -> eval_op1 o' y -> eval_op1 (OpMult o o') (x * y).
+ forall (o o' om: Op1) (x y : R),
+ eval_op1 o x -> eval_op1 o' y -> OpMult o o' = Some om -> eval_op1 om (x * y).
Proof.
-unfold eval_op1; destruct o; simpl; intros o' x y H1 H2 H3 H4.
-rewrite H3; now rewrite (Rtimes_0_l sor).
-elimtype False; now apply H1.
-destruct o'.
-rewrite H4; now rewrite (Rtimes_0_r sor).
-elimtype False; now apply H2.
-now apply (Rtimes_pos_pos sor).
-apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
-destruct o'.
-rewrite H4, (Rtimes_0_r sor); le_equal.
-elimtype False; now apply H2.
-apply (Rtimes_nonneg_nonneg sor); [assumption | le_less].
-now apply (Rtimes_nonneg_nonneg sor).
+unfold eval_op1; destruct o; simpl; intros o' om x y H1 H2 H3.
+(* x == 0 *)
+inversion H3. rewrite H1. now rewrite (Rtimes_0_l sor).
+(* x ~= 0 *)
+destruct o' ; inversion H3.
+ (* y == 0 *)
+ rewrite H2. now rewrite (Rtimes_0_r sor).
+ (* y ~= 0 *)
+ apply (Rtimes_neq_0 sor) ; auto.
+(* 0 < x *)
+destruct o' ; inversion H3.
+ (* y == 0 *)
+ rewrite H2; now rewrite (Rtimes_0_r sor).
+ (* 0 < y *)
+ now apply (Rtimes_pos_pos sor).
+ (* 0 <= y *)
+ apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
+(* 0 <= x *)
+destruct o' ; inversion H3.
+ (* y == 0 *)
+ rewrite H2; now rewrite (Rtimes_0_r sor).
+ (* 0 < y *)
+ apply (Rtimes_nonneg_nonneg sor); [assumption | le_less ].
+ (* 0 <= y *)
+ now apply (Rtimes_nonneg_nonneg sor).
Qed.
Lemma OpAdd_sound :
- forall (o o' : Op1) (e e' : R), o <> NonEqual -> o' <> NonEqual ->
- eval_op1 o e -> eval_op1 o' e' -> eval_op1 (OpAdd o o') (e + e').
-Proof.
-unfold eval_op1; destruct o; simpl; intros o' e e' H1 H2 H3 H4.
-destruct o'.
-now rewrite H3, H4, (Rplus_0_l sor).
-elimtype False; now apply H2.
-now rewrite H3, (Rplus_0_l sor).
-now rewrite H3, (Rplus_0_l sor).
-elimtype False; now apply H1.
-destruct o'.
-now rewrite H4, (Rplus_0_r sor).
-elimtype False; now apply H2.
-now apply (Rplus_pos_pos sor).
-now apply (Rplus_pos_nonneg sor).
-destruct o'.
-now rewrite H4, (Rplus_0_r sor).
-elimtype False; now apply H2.
-now apply (Rplus_nonneg_pos sor).
-now apply (Rplus_nonneg_nonneg sor).
-Qed.
-
-(* We consider a monoid whose generators are polynomials from the
-hypotheses of the form (p ~= 0). Thus it follows from the hypotheses that
-every element of the monoid (i.e., arbitrary product of generators) is ~=
-0. Therefore, the square of every element is > 0. *)
-
-Inductive Monoid (l : list NFormula) : PExprC -> Prop :=
-| M_One : Monoid l (PEc cI)
-| M_In : forall p : PExprC, In (p, NonEqual) l -> Monoid l p
-| M_Mult : forall (e1 e2 : PExprC), Monoid l e1 -> Monoid l e2 -> Monoid l (PEmul e1 e2).
-
-(* Do we really need to rely on the intermediate definition of monoid ?
- InC why the restriction NonEqual ?
- Could not we consider the IsIdeal as a IsMult ?
- The same for IsSquare ?
-*)
-
-Inductive Cone (l : list (NFormula)) : PExprC -> Op1 -> Prop :=
-| InC : forall p op, In (p, op) l -> op <> NonEqual -> Cone l p op
-| IsIdeal : forall p, Cone l p Equal -> forall p', Cone l (PEmul p p') Equal
-| IsSquare : forall p, Cone l (PEmul p p) NonStrict
-| IsMonoid : forall p, Monoid l p -> Cone l (PEmul p p) Strict
-| IsMult : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEmul p q) (OpMult op oq)
-| IsAdd : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEadd p q) (OpAdd op oq)
-| IsPos : forall c : C, cltb cO c = true -> Cone l (PEc c) Strict
-| IsZ : Cone l (PEc cO) Equal.
-
-(* As promised, if all hypotheses are true in some environment, then every
-member of the monoid is nonzero in this environment *)
-
-Lemma monoid_nonzero : forall (l : list NFormula) (env : PolEnv),
- (forall f : NFormula, In f l -> eval_nformula env f) ->
- forall p : PExprC, Monoid l p -> eval_pexpr env p ~= 0.
+ forall (o o' oa : Op1) (e e' : R),
+ eval_op1 o e -> eval_op1 o' e' -> OpAdd o o' = Some oa -> eval_op1 oa (e + e').
Proof.
-intros l env H1 p H2. induction H2 as [| f H | e1 e2 H3 IH1 H4 IH2]; simpl.
-rewrite addon.(SORrm).(morph1). apply (Rneq_symm sor). apply (Rneq_0_1 sor).
-apply H1 in H. now simpl in H.
-simpl in IH1, IH2. apply (Rtimes_neq_0 sor). now split.
+unfold eval_op1; destruct o; simpl; intros o' oa e e' H1 H2 Hoa.
+(* e == 0 *)
+inversion Hoa. rewrite <- H0.
+destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor).
+(* e ~= 0 *)
+ destruct o'.
+ (* e' == 0 *)
+ inversion Hoa.
+ rewrite H2. now rewrite (Rplus_0_r sor).
+ (* e' ~= 0 *)
+ discriminate.
+ (* 0 < e' *)
+ discriminate.
+ (* 0 <= e' *)
+ discriminate.
+(* 0 < e *)
+ destruct o'.
+ (* e' == 0 *)
+ inversion Hoa.
+ rewrite H2. now rewrite (Rplus_0_r sor).
+ (* e' ~= 0 *)
+ discriminate.
+ (* 0 < e' *)
+ inversion Hoa.
+ now apply (Rplus_pos_pos sor).
+ (* 0 <= e' *)
+ inversion Hoa.
+ now apply (Rplus_pos_nonneg sor).
+(* 0 <= e *)
+ destruct o'.
+ (* e' == 0 *)
+ inversion Hoa.
+ now rewrite H2, (Rplus_0_r sor).
+ (* e' ~= 0 *)
+ discriminate.
+ (* 0 < e' *)
+ inversion Hoa.
+ now apply (Rplus_nonneg_pos sor).
+ (* 0 <= e' *)
+ inversion Hoa.
+ now apply (Rplus_nonneg_nonneg sor).
Qed.
-(* If all members of a cone base are true in some environment, then every
-member of the cone is true as well *)
+Inductive Psatz : Type :=
+| PsatzIn : nat -> Psatz
+| PsatzSquare : PolC -> Psatz
+| PsatzMulC : PolC -> Psatz -> Psatz
+| PsatzMulE : Psatz -> Psatz -> Psatz
+| PsatzAdd : Psatz -> Psatz -> Psatz
+| PsatzC : C -> Psatz
+| PsatzZ : Psatz.
+
+(** Given a list [l] of NFormula and an extended polynomial expression
+ [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a
+ logic consequence of the conjunction of the formulae in l.
+ Moreover, the polynomial expression is obtained by replacing the (PsatzIn n)
+ by the nth polynomial expression in [l] and the sign is computed by the "rule of sign" *)
+
+(* Might be defined elsewhere *)
+Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B :=
+ match o with
+ | None => None
+ | Some x => f x
+ end.
-Lemma cone_true :
- forall (l : list NFormula) (env : PolEnv),
- (forall (f : NFormula), In f l -> eval_nformula env f) ->
- forall (p : PExprC) (op : Op1), Cone l p op ->
- op <> NonEqual /\ eval_nformula env (p, op).
-Proof.
-intros l env H1 p op H2. induction H2; simpl in *.
-split. assumption. apply H1 in H. now unfold eval_nformula in H.
-split. discriminate. destruct IHCone as [_ H3]. rewrite H3. now rewrite (Rtimes_0_l sor).
-split. discriminate. apply (Rtimes_square_nonneg sor).
-split. discriminate. apply <- (Rlt_le_neq sor). split. apply (Rtimes_square_nonneg sor).
-apply (Rneq_symm sor). apply (Rtimes_neq_0 sor). split; now apply monoid_nonzero with l.
-destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
-split. now apply OpMultNonEqual. now apply OpMult_sound.
-destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
-split. now apply OpAdd_NonEqual. now apply OpAdd_sound.
-split. discriminate. rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
-split. discriminate. apply addon.(SORrm).(morph0).
-Qed.
+Implicit Arguments map_option [A B].
-(* Every element of a monoid is a product of some generators; therefore,
-to determine an element we can give a list of generators' indices *)
-
-Definition MonoidMember : Set := list nat.
-
-Inductive ConeMember : Type :=
-| S_In : nat -> ConeMember
-| S_Ideal : PExprC -> ConeMember -> ConeMember
-| S_Square : PExprC -> ConeMember
-| S_Monoid : MonoidMember -> ConeMember
-| S_Mult : ConeMember -> ConeMember -> ConeMember
-| S_Add : ConeMember -> ConeMember -> ConeMember
-| S_Pos : C -> ConeMember
-| S_Z : ConeMember.
-
-Definition nformula_times (f f' : NFormula) : NFormula :=
-let (p, op) := f in
- let (p', op') := f' in
- (PEmul p p', OpMult op op').
-
-Definition nformula_plus (f f' : NFormula) : NFormula :=
-let (p, op) := f in
- let (p', op') := f' in
- (PEadd p p', OpAdd op op').
-
-Definition nformula_times_0 (p : PExprC) (f : NFormula) : NFormula :=
-let (q, op) := f in
- match op with
- | Equal => (PEmul q p, Equal)
- | _ => f
+Definition map_option2 (A B C : Type) (f : A -> B -> option C)
+ (o: option A) (o': option B) : option C :=
+ match o , o' with
+ | None , _ => None
+ | _ , None => None
+ | Some x , Some x' => f x x'
end.
-Fixpoint eval_monoid (l : list NFormula) (ns : MonoidMember) {struct ns} : PExprC :=
-match ns with
-| nil => PEc cI
-| n :: ns =>
- let p := match nth n l (PEc cI, NonEqual) with
- | (q, NonEqual) => q
- | _ => PEc cI
- end in
- PEmul p (eval_monoid l ns)
-end.
+Implicit Arguments map_option2 [A B C].
-Theorem eval_monoid_in_monoid :
- forall (l : list NFormula) (ns : MonoidMember), Monoid l (eval_monoid l ns).
-Proof.
-intro l; induction ns; simpl in *.
-constructor.
-apply M_Mult; [| assumption].
-destruct (nth_in_or_default a l (PEc cI, NonEqual)).
-destruct (nth a l (PEc cI, NonEqual)). destruct o; try constructor. assumption.
-rewrite e; simpl. constructor.
-Qed.
+Definition Rops_wd := mk_reqe rplus rtimes ropp req
+ sor.(SORplus_wd)
+ sor.(SORtimes_wd)
+ sor.(SORopp_wd).
-(* Provides the cone member from the witness, i.e., ConeMember *)
-Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
-match cm with
-| S_In n => let f := nth n l (PEc cO, Equal) in
- match f with
- | (_, NonEqual) => (PEc cO, Equal)
- | _ => f
- end
-| S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
-| S_Square p => (PEmul p p, NonStrict)
-| S_Monoid m => let p := eval_monoid l m in (PEmul p p, Strict)
-| S_Mult p q => nformula_times (eval_cone l p) (eval_cone l q)
-| S_Add p q => nformula_plus (eval_cone l p) (eval_cone l q)
-| S_Pos c => if cltb cO c then (PEc c, Strict) else (PEc cO, Equal)
-| S_Z => (PEc cO, Equal)
-end.
+Definition pexpr_times_nformula (e: PolC) (f : NFormula) : option NFormula :=
+ let (ef,o) := f in
+ match o with
+ | Equal => Some (Pmul cO cI cplus ctimes ceqb e ef , Equal)
+ | _ => None
+ end.
+
+Definition nformula_times_nformula (f1 f2 : NFormula) : option NFormula :=
+ let (e1,o1) := f1 in
+ let (e2,o2) := f2 in
+ map_option (fun x => (Some (Pmul cO cI cplus ctimes ceqb e1 e2,x))) (OpMult o1 o2).
+
+ Definition nformula_plus_nformula (f1 f2 : NFormula) : option NFormula :=
+ let (e1,o1) := f1 in
+ let (e2,o2) := f2 in
+ map_option (fun x => (Some (Padd cO cplus ceqb e1 e2,x))) (OpAdd o1 o2).
+
+
+Fixpoint eval_Psatz (l : list NFormula) (e : Psatz) {struct e} : option NFormula :=
+ match e with
+ | PsatzIn n => Some (nth n l (Pc cO, Equal))
+ | PsatzSquare e => Some (Psquare cO cI cplus ctimes ceqb e , NonStrict)
+ | PsatzMulC re e => map_option (pexpr_times_nformula re) (eval_Psatz l e)
+ | PsatzMulE f1 f2 => map_option2 nformula_times_nformula (eval_Psatz l f1) (eval_Psatz l f2)
+ | PsatzAdd f1 f2 => map_option2 nformula_plus_nformula (eval_Psatz l f1) (eval_Psatz l f2)
+ | PsatzC c => if cltb cO c then Some (Pc c, Strict) else None
+(* This could be 0, or <> 0 -- but these cases are useless *)
+ | PsatzZ => Some (Pc cO, Equal) (* Just to make life easier *)
+ end.
-Theorem eval_cone_in_cone :
- forall (l : list NFormula) (cm : ConeMember),
- let (p, op) := eval_cone l cm in Cone l p op.
+Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFormula),
+ eval_nformula env f -> pexpr_times_nformula e f = Some f' ->
+ eval_nformula env f'.
Proof.
-intros l cm; induction cm; simpl.
-destruct (nth_in_or_default n l (PEc cO, Equal)).
-destruct (nth n l (PEc cO, Equal)). destruct o; try (now apply InC). apply IsZ.
-rewrite e. apply IsZ.
-destruct (eval_cone l cm). destruct o; simpl; try assumption. now apply IsIdeal.
-apply IsSquare.
-apply IsMonoid. apply eval_monoid_in_monoid.
-destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_times. now apply IsMult.
-destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_plus. now apply IsAdd.
-case_eq (cO [<] c) ; intros ; [apply IsPos ; auto| apply IsZ].
-apply IsZ.
+ unfold pexpr_times_nformula.
+ destruct f.
+ intros. destruct o ; inversion H0 ; try discriminate.
+ simpl in *. unfold eval_pol in *.
+ rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+ rewrite H. apply (Rtimes_0_r sor).
Qed.
-
-(* (inconsistent_cone_member l p) means (p, op) is in the cone for some op
-(> 0, >= 0, == 0, or ~= 0) and this formula is inconsistent. This fact
-implies that l is inconsistent, as shown by the next lemma. Inconsistency
-of a formula (p, op) can be established by normalizing p and showing that
-it is a constant c for which (c, op) is false. (This is only a sufficient,
-not necessary, condition, of course.) Membership in the cone can be
-verified if we have a certificate. *)
-
-Definition inconsistent_cone_member (l : list NFormula) (p : PExprC) :=
- exists op : Op1, Cone l p op /\
- forall env : PolEnv, ~ eval_op1 op (eval_pexpr env p).
-
-(* If some element of a cone is inconsistent, then the base of the cone
-is also inconsistent *)
-
-Lemma prove_inconsistent :
- forall (l : list NFormula) (p : PExprC),
- inconsistent_cone_member l p -> forall env, make_impl (eval_nformula env) l False.
+
+Lemma nformula_times_nformula_correct : forall (env:PolEnv)
+ (f1 f2 f : NFormula),
+ eval_nformula env f1 -> eval_nformula env f2 ->
+ nformula_times_nformula f1 f2 = Some f ->
+ eval_nformula env f.
Proof.
-intros l p H env.
-destruct H as [o [wit H]].
-apply -> make_conj_impl.
-intro H1. apply H with env.
-pose proof (@cone_true l env) as H2.
-cut (forall f : NFormula, In f l -> eval_nformula env f). intro H3.
-apply (proj2 (H2 H3 p o wit)). intro. now apply make_conj_in.
+ unfold nformula_times_nformula.
+ destruct f1 ; destruct f2.
+ case_eq (OpMult o o0) ; simpl ; try discriminate.
+ intros. inversion H2 ; simpl.
+ unfold eval_pol.
+ destruct o1; simpl;
+ rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ apply OpMult_sound with (3:= H);assumption.
Qed.
-Definition normalise_pexpr : PExprC -> PolC :=
- norm_aux cO cI cplus ctimes cminus copp ceqb.
+Lemma nformula_plus_nformula_correct : forall (env:PolEnv)
+ (f1 f2 f : NFormula),
+ eval_nformula env f1 -> eval_nformula env f2 ->
+ nformula_plus_nformula f1 f2 = Some f ->
+ eval_nformula env f.
+Proof.
+ unfold nformula_plus_nformula.
+ destruct f1 ; destruct f2.
+ case_eq (OpAdd o o0) ; simpl ; try discriminate.
+ intros. inversion H2 ; simpl.
+ unfold eval_pol.
+ destruct o1; simpl;
+ rewrite (Padd_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ apply OpAdd_sound with (3:= H);assumption.
+Qed.
-(* The following definition we don't really need, hence it is commented *)
-(*Definition eval_pol : PolEnv -> PolC -> R := Pphi 0 rplus rtimes phi.*)
+Lemma eval_Psatz_Sound :
+ forall (l : list NFormula) (env : PolEnv),
+ (forall (f : NFormula), In f l -> eval_nformula env f) ->
+ forall (e : Psatz) (f : NFormula), eval_Psatz l e = Some f ->
+ eval_nformula env f.
+Proof.
+ induction e.
+ (* PsatzIn *)
+ simpl ; intros.
+ destruct (nth_in_or_default n l (Pc cO, Equal)).
+ (* index is in bounds *)
+ apply H ; congruence.
+ (* index is out-of-bounds *)
+ inversion H0.
+ rewrite e. simpl.
+ now apply addon.(SORrm).(morph0).
+ (* PsatzSquare *)
+ simpl. intros. inversion H0.
+ simpl. unfold eval_pol.
+ rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ now apply (Rtimes_square_nonneg sor).
+ (* PsatzMulC *)
+ simpl.
+ intro.
+ case_eq (eval_Psatz l e) ; simpl ; intros.
+ apply IHe in H0.
+ apply pexpr_times_nformula_correct with (1:=H0) (2:= H1).
+ discriminate.
+ (* PsatzMulC *)
+ simpl ; intro.
+ case_eq (eval_Psatz l e1) ; simpl ; try discriminate.
+ case_eq (eval_Psatz l e2) ; simpl ; try discriminate.
+ intros.
+ apply IHe1 in H1. apply IHe2 in H0.
+ apply (nformula_times_nformula_correct env n0 n) ; assumption.
+ (* PsatzAdd *)
+ simpl ; intro.
+ case_eq (eval_Psatz l e1) ; simpl ; try discriminate.
+ case_eq (eval_Psatz l e2) ; simpl ; try discriminate.
+ intros.
+ apply IHe1 in H1. apply IHe2 in H0.
+ apply (nformula_plus_nformula_correct env n0 n) ; assumption.
+ (* PsatzC *)
+ simpl.
+ intro. case_eq (cO [<] c).
+ intros. inversion H1. simpl.
+ rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+ discriminate.
+ (* PsatzZ *)
+ simpl. intros. inversion H0.
+ simpl. apply addon.(SORrm).(morph0).
+Qed.
(* roughly speaking, normalise_pexpr_correct is a proof of
forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *)
(*****)
-Definition normalise_pexpr_correct :=
-let Rops_wd := mk_reqe rplus rtimes ropp req
+Definition paddC := PaddC cplus.
+Definition psubC := PsubC cminus.
+
+Definition PsubC_ok : forall c P env, eval_pol env (psubC P c) == eval_pol env P - [c] :=
+ let Rops_wd := mk_reqe rplus rtimes ropp req
sor.(SORplus_wd)
sor.(SORtimes_wd)
sor.(SORopp_wd) in
- norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
- addon.(SORrm) addon.(SORpower).
-(*****)
-(*Definition normalise_pexpr_correct :=
-let Rops_wd := mk_reqe rplus rtimes ropp req
+ PsubC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
+ addon.(SORrm).
+
+Definition PaddC_ok : forall c P env, eval_pol env (paddC P c) == eval_pol env P + [c] :=
+ let Rops_wd := mk_reqe rplus rtimes ropp req
sor.(SORplus_wd)
sor.(SORtimes_wd)
sor.(SORopp_wd) in
- norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth sor.(SORsetoid) Rops_wd sor.(SORrt))
- addon.(SORrm) addon.(SORpower) nil.*)
-(*****)
+ PaddC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
+ addon.(SORrm).
+
(* Check that a formula f is inconsistent by normalizing and comparing the
resulting constant with 0 *)
Definition check_inconsistent (f : NFormula) : bool :=
let (e, op) := f in
- match normalise_pexpr e with
+ match e with
| Pc c =>
match op with
| Equal => cneqb c cO
| NonStrict => c [<] cO
| Strict => c [<=] cO
- | NonEqual => false (* eval_cone never returns (p, NonEqual) *)
+ | NonEqual => c [=] cO
end
| _ => false (* not a constant *)
end.
Lemma check_inconsistent_sound :
- forall (p : PExprC) (op : Op1),
- check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pexpr env p).
+ forall (p : PolC) (op : Op1),
+ check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pol env p).
Proof.
-intros p op H1 env. unfold check_inconsistent, normalise_pexpr in H1.
-destruct op; simpl;
-(*****)
-rewrite eval_pexpr_PEeval;
-(*****)
-(*unfold eval_pexpr;*)
+intros p op H1 env. unfold check_inconsistent in H1.
+destruct op; simpl ;
(*****)
-rewrite normalise_pexpr_correct;
-destruct (norm_aux cO cI cplus ctimes cminus copp ceqb p); simpl; try discriminate H1;
+destruct p ; simpl; try discriminate H1;
try rewrite <- addon.(SORrm).(morph0); trivial.
now apply cneqb_sound.
+apply addon.(SORrm).(morph_eq) in H1. congruence.
apply cleb_sound in H1. now apply -> (Rle_ngt sor).
apply cltb_sound in H1. now apply -> (Rlt_nge sor).
Qed.
-Definition check_normalised_formulas : list NFormula -> ConeMember -> bool :=
- fun l cm => check_inconsistent (eval_cone l cm).
+Definition check_normalised_formulas : list NFormula -> Psatz -> bool :=
+ fun l cm =>
+ match eval_Psatz l cm with
+ | None => false
+ | Some f => check_inconsistent f
+ end.
Lemma checker_nf_sound :
- forall (l : list NFormula) (cm : ConeMember),
+ forall (l : list NFormula) (cm : Psatz),
check_normalised_formulas l cm = true ->
forall env : PolEnv, make_impl (eval_nformula env) l False.
Proof.
intros l cm H env.
unfold check_normalised_formulas in H.
-case_eq (eval_cone l cm). intros p op H1.
-apply prove_inconsistent with p. unfold inconsistent_cone_member. exists op. split.
-pose proof (eval_cone_in_cone l cm) as H2. now rewrite H1 in H2.
-apply check_inconsistent_sound. now rewrite <- H1.
+revert H.
+case_eq (eval_Psatz l cm) ; [|discriminate].
+intros nf. intros.
+rewrite <- make_conj_impl. intro.
+assert (H1' := make_conj_in _ _ H1).
+assert (Hnf := @eval_Psatz_Sound _ _ H1' _ _ H).
+destruct nf.
+apply (@check_inconsistent_sound _ _ H0 env Hnf).
Qed.
(** Normalisation of formulae **)
@@ -577,10 +555,12 @@ match o with
| OpGt => fun x y : R => y < x
end.
+Definition eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe.
+
Record Formula : Type := {
- Flhs : PExprC;
+ Flhs : PExpr C;
Fop : Op2;
- Frhs : PExprC
+ Frhs : PExpr C
}.
Definition eval_formula (env : PolEnv) (f : Formula) : Prop :=
@@ -589,34 +569,66 @@ Definition eval_formula (env : PolEnv) (f : Formula) : Prop :=
(* We normalize Formulas by moving terms to one side *)
+Definition norm := norm_aux cO cI cplus ctimes cminus copp ceqb.
+
+Definition psub := Psub cO cplus cminus copp ceqb.
+
+Definition padd := Padd cO cplus ceqb.
+
Definition normalise (f : Formula) : NFormula :=
let (lhs, op, rhs) := f in
+ let lhs := norm lhs in
+ let rhs := norm rhs in
match op with
- | OpEq => (PEsub lhs rhs, Equal)
- | OpNEq => (PEsub lhs rhs, NonEqual)
- | OpLe => (PEsub rhs lhs, NonStrict)
- | OpGe => (PEsub lhs rhs, NonStrict)
- | OpGt => (PEsub lhs rhs, Strict)
- | OpLt => (PEsub rhs lhs, Strict)
+ | OpEq => (psub lhs rhs, Equal)
+ | OpNEq => (psub lhs rhs, NonEqual)
+ | OpLe => (psub rhs lhs, NonStrict)
+ | OpGe => (psub lhs rhs, NonStrict)
+ | OpGt => (psub lhs rhs, Strict)
+ | OpLt => (psub rhs lhs, Strict)
end.
Definition negate (f : Formula) : NFormula :=
let (lhs, op, rhs) := f in
- match op with
- | OpEq => (PEsub rhs lhs, NonEqual)
- | OpNEq => (PEsub rhs lhs, Equal)
- | OpLe => (PEsub lhs rhs, Strict) (* e <= e' == ~ e > e' *)
- | OpGe => (PEsub rhs lhs, Strict)
- | OpGt => (PEsub rhs lhs, NonStrict)
- | OpLt => (PEsub lhs rhs, NonStrict)
-end.
+ let lhs := norm lhs in
+ let rhs := norm rhs in
+ match op with
+ | OpEq => (psub rhs lhs, NonEqual)
+ | OpNEq => (psub rhs lhs, Equal)
+ | OpLe => (psub lhs rhs, Strict) (* e <= e' == ~ e > e' *)
+ | OpGe => (psub rhs lhs, Strict)
+ | OpGt => (psub rhs lhs, NonStrict)
+ | OpLt => (psub lhs rhs, NonStrict)
+ end.
+
+
+Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) == eval_pol env lhs - eval_pol env rhs.
+Proof.
+ intros.
+ apply (Psub_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+Qed.
+
+Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) == eval_pol env lhs + eval_pol env rhs.
+Proof.
+ intros.
+ apply (Padd_ok sor.(SORsetoid) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+Qed.
+
+Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs).
+Proof.
+ intros.
+ apply (norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm) addon.(SORpower) ).
+Qed.
+
Theorem normalise_sound :
forall (env : PolEnv) (f : Formula),
eval_formula env f -> eval_nformula env (normalise f).
Proof.
intros env f H; destruct f as [lhs op rhs]; simpl in *.
-destruct op; simpl in *.
+destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm.
now apply <- (Rminus_eq_0 sor).
intros H1. apply -> (Rminus_eq_0 sor) in H1. now apply H.
now apply -> (Rle_le_minus sor).
@@ -630,7 +642,7 @@ Theorem negate_correct :
eval_formula env f <-> ~ (eval_nformula env (negate f)).
Proof.
intros env f; destruct f as [lhs op rhs]; simpl.
-destruct op; simpl.
+destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm.
symmetry. rewrite (Rminus_eq_0 sor).
split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)].
rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor).
@@ -644,14 +656,16 @@ Qed.
Definition xnormalise (t:Formula) : list (NFormula) :=
let (lhs,o,rhs) := t in
+ let lhs := norm lhs in
+ let rhs := norm rhs in
match o with
| OpEq =>
- (PEsub lhs rhs, Strict)::(PEsub rhs lhs , Strict)::nil
- | OpNEq => (PEsub lhs rhs,Equal) :: nil
- | OpGt => (PEsub rhs lhs,NonStrict) :: nil
- | OpLt => (PEsub lhs rhs,NonStrict) :: nil
- | OpGe => (PEsub rhs lhs , Strict) :: nil
- | OpLe => (PEsub lhs rhs ,Strict) :: nil
+ (psub lhs rhs, Strict)::(psub rhs lhs , Strict)::nil
+ | OpNEq => (psub lhs rhs,Equal) :: nil
+ | OpGt => (psub rhs lhs,NonStrict) :: nil
+ | OpLt => (psub lhs rhs,NonStrict) :: nil
+ | OpGe => (psub rhs lhs , Strict) :: nil
+ | OpLe => (psub lhs rhs ,Strict) :: nil
end.
Require Import Tauto.
@@ -666,7 +680,8 @@ Lemma cnf_normalise_correct : forall env t, eval_cnf (eval_nformula env) (cnf_no
Proof.
unfold cnf_normalise, xnormalise ; simpl ; intros env t.
unfold eval_cnf.
- destruct t as [lhs o rhs]; case_eq o ; simpl;
+ destruct t as [lhs o rhs]; case_eq o ; simpl;
+ repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
generalize (eval_pexpr env lhs);
generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros.
(**)
@@ -682,13 +697,15 @@ Qed.
Definition xnegate (t:Formula) : list (NFormula) :=
let (lhs,o,rhs) := t in
+ let lhs := norm lhs in
+ let rhs := norm rhs in
match o with
- | OpEq => (PEsub lhs rhs,Equal) :: nil
- | OpNEq => (PEsub lhs rhs ,Strict)::(PEsub rhs lhs,Strict)::nil
- | OpGt => (PEsub lhs rhs,Strict) :: nil
- | OpLt => (PEsub rhs lhs,Strict) :: nil
- | OpGe => (PEsub lhs rhs,NonStrict) :: nil
- | OpLe => (PEsub rhs lhs,NonStrict) :: nil
+ | OpEq => (psub lhs rhs,Equal) :: nil
+ | OpNEq => (psub lhs rhs ,Strict)::(psub rhs lhs,Strict)::nil
+ | OpGt => (psub lhs rhs,Strict) :: nil
+ | OpLt => (psub rhs lhs,Strict) :: nil
+ | OpGe => (psub lhs rhs,NonStrict) :: nil
+ | OpLe => (psub rhs lhs,NonStrict) :: nil
end.
Definition cnf_negate (t:Formula) : cnf (NFormula) :=
@@ -698,10 +715,10 @@ Lemma cnf_negate_correct : forall env t, eval_cnf (eval_nformula env) (cnf_negat
Proof.
unfold cnf_negate, xnegate ; simpl ; intros env t.
unfold eval_cnf.
- destruct t as [lhs o rhs]; case_eq o ; simpl ;
- generalize (eval_pexpr env lhs);
- generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros ;
- intuition.
+ destruct t as [lhs o rhs]; case_eq o ; simpl;
+ repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
+ generalize (eval_pexpr env lhs);
+ generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros ; intuition.
(**)
apply H0.
rewrite H1 ; ring.
@@ -717,12 +734,11 @@ Proof.
apply H0. now rewrite (Rlt_lt_minus sor) in H1.
Qed.
-
Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).
Proof.
intros.
destruct d ; simpl.
- generalize (eval_pexpr env p); intros.
+ generalize (eval_pol env p); intros.
destruct o ; simpl.
apply (Req_em sor r 0).
destruct (Req_em sor r 0) ; tauto.
@@ -730,52 +746,104 @@ Proof.
rewrite <- (Rlt_nge sor r 0). generalize (Rle_gt_cases sor 0 r). tauto.
Qed.
-(** Some syntactic simplifications of expressions and cone elements *)
-
+(** Reverse transformation *)
-Fixpoint simpl_expr (e:PExprC) : PExprC :=
- match e with
- | PEmul y z => let y' := simpl_expr y in let z' := simpl_expr z in
- match y' , z' with
- | PEc c , z' => if ceqb c cI then z' else PEmul y' z'
- | _ , _ => PEmul y' z'
- end
- | PEadd x y => PEadd (simpl_expr x) (simpl_expr y)
- | _ => e
+Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
+ match p with
+ | Pc c => PEc c
+ | Pinj j p => xdenorm (Pplus j jmp ) p
+ | PX p j q => PEadd
+ (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j)))
+ (xdenorm (Psucc jmp) q)
end.
+Lemma xdenorm_correct : forall p i env, eval_pol (jump i env) p == eval_pexpr env (xdenorm (Psucc i) p).
+Proof.
+ unfold eval_pol.
+ induction p.
+ simpl. reflexivity.
+ (* Pinj *)
+ simpl.
+ intros.
+ rewrite Pplus_succ_permute_r.
+ rewrite <- IHp.
+ symmetry.
+ rewrite Pplus_comm.
+ rewrite Pjump_Pplus. reflexivity.
+ (* PX *)
+ simpl.
+ intros.
+ rewrite <- IHp1.
+ rewrite <- IHp2.
+ unfold Env.tail , Env.hd.
+ rewrite <- Pjump_Pplus.
+ rewrite <- Pplus_one_succ_r.
+ unfold Env.nth.
+ unfold jump at 2.
+ rewrite Pplus_one_succ_l.
+ rewrite addon.(SORpower).(rpow_pow_N).
+ unfold pow_N. ring.
+Qed.
+
+Definition denorm (p : Pol C) := xdenorm xH p.
+
+Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
+Proof.
+ unfold denorm.
+ induction p.
+ reflexivity.
+ simpl.
+ rewrite <- Pplus_one_succ_r.
+ apply xdenorm_correct.
+ simpl.
+ intros.
+ rewrite IHp1.
+ unfold Env.tail.
+ rewrite xdenorm_correct.
+ change (Psucc xH) with 2%positive.
+ rewrite addon.(SORpower).(rpow_pow_N).
+ simpl. reflexivity.
+Qed.
+
-Definition simpl_cone (e:ConeMember) : ConeMember :=
+(** Some syntactic simplifications of expressions *)
+
+
+Definition simpl_cone (e:Psatz) : Psatz :=
match e with
- | S_Square t => let x:=simpl_expr t in
- match x with
- | PEc c => if ceqb cO c then S_Z else S_Pos (ctimes c c)
- | _ => S_Square x
+ | PsatzSquare t =>
+ match t with
+ | Pc c => if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
+ | _ => PsatzSquare t
end
- | S_Mult t1 t2 =>
+ | PsatzMulE t1 t2 =>
match t1 , t2 with
- | S_Z , x => S_Z
- | x , S_Z => S_Z
- | S_Pos c , S_Pos c' => S_Pos (ctimes c c')
- | S_Pos p1 , S_Mult (S_Pos p2) x => S_Mult (S_Pos (ctimes p1 p2)) x
- | S_Pos p1 , S_Mult x (S_Pos p2) => S_Mult (S_Pos (ctimes p1 p2)) x
- | S_Mult (S_Pos p2) x , S_Pos p1 => S_Mult (S_Pos (ctimes p1 p2)) x
- | S_Mult x (S_Pos p2) , S_Pos p1 => S_Mult (S_Pos (ctimes p1 p2)) x
- | S_Pos x , S_Add y z => S_Add (S_Mult (S_Pos x) y) (S_Mult (S_Pos x) z)
- | S_Pos c , _ => if ceqb cI c then t2 else S_Mult t1 t2
- | _ , S_Pos c => if ceqb cI c then t1 else S_Mult t1 t2
+ | PsatzZ , x => PsatzZ
+ | x , PsatzZ => PsatzZ
+ | PsatzC c , PsatzC c' => PsatzC (ctimes c c')
+ | PsatzC p1 , PsatzMulE (PsatzC p2) x => PsatzMulE (PsatzC (ctimes p1 p2)) x
+ | PsatzC p1 , PsatzMulE x (PsatzC p2) => PsatzMulE (PsatzC (ctimes p1 p2)) x
+ | PsatzMulE (PsatzC p2) x , PsatzC p1 => PsatzMulE (PsatzC (ctimes p1 p2)) x
+ | PsatzMulE x (PsatzC p2) , PsatzC p1 => PsatzMulE (PsatzC (ctimes p1 p2)) x
+ | PsatzC x , PsatzAdd y z => PsatzAdd (PsatzMulE (PsatzC x) y) (PsatzMulE (PsatzC x) z)
+ | PsatzC c , _ => if ceqb cI c then t2 else PsatzMulE t1 t2
+ | _ , PsatzC c => if ceqb cI c then t1 else PsatzMulE t1 t2
| _ , _ => e
end
- | S_Add t1 t2 =>
+ | PsatzAdd t1 t2 =>
match t1 , t2 with
- | S_Z , x => x
- | x , S_Z => x
- | x , y => S_Add x y
+ | PsatzZ , x => x
+ | x , PsatzZ => x
+ | x , y => PsatzAdd x y
end
| _ => e
end.
+
End Micromega.
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *) \ No newline at end of file
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index ef48efa6d..a23671fde 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -8,7 +8,7 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
-(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
+(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 2b63c88f9..65ea366fd 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -19,7 +19,7 @@ Require Import Refl.
Require Import ZArith.
Require Import List.
Require Import Bool.
-Declare ML Module "micromega_plugin".
+(*Declare ML Module "micromega_plugin".*)
Ltac flatten_bool :=
repeat match goal with
@@ -27,6 +27,9 @@ Ltac flatten_bool :=
| [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id
end.
+Ltac inv H := inversion H ; try subst ; clear H.
+
+
Require Import EnvRing.
Open Scope Z_scope.
@@ -56,37 +59,18 @@ Proof.
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 :=
+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)
+ | PEc c => c
+ | PEX x => env x
+ | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
+ | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
+ | PEpow e1 n => Zpower (Zeval_expr env e1) (Z_of_N n)
+ | PEsub e1 e2 => (Zeval_expr env e1) - (Zeval_expr env e2)
+ | PEopp e => Zopp (Zeval_expr env e)
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).
+Definition eval_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.
@@ -99,13 +83,11 @@ Proof.
induction p; simpl ; intros ; repeat rewrite IHp ; ring.
Qed.
-
-
-Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = Zeval_expr' env e.
+Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.
Proof.
- induction e ; simpl ; subst ; try congruence.
- rewrite IHe.
- apply ZNpower.
+ induction e ; simpl ; try congruence.
+ reflexivity.
+ rewrite ZNpower. congruence.
Qed.
Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop :=
@@ -118,27 +100,28 @@ match o with
| 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 (env : PolEnv Z) (f : Formula Z):=
+ let (lhs, op, rhs) := f in
+ (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env 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.
+ destruct f ; simpl.
+ rewrite Zeval_expr_compat. rewrite Zeval_expr_compat.
+ unfold eval_expr.
+ generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
+ (fun x : N => x) (pow_N 1 Zmult) env Flhs).
+ generalize ((eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
+ (fun x : N => x) (pow_N 1 Zmult) env Frhs)).
+ destruct Fop ; simpl; intros ; intuition (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 eval_nformula :=
+ eval_nformula 0 Zplus Zmult (@eq Z) Zle Zlt (fun x => x) .
Definition Zeval_op1 (o : Op1) : Z -> Prop :=
match o with
@@ -148,45 +131,67 @@ match o with
| 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).
+Lemma Zeval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_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).
+ intros.
+ apply (eval_nformula_dec Zsor).
Qed.
-Definition ZWitness := ConeMember Z.
+Definition ZWitness := Psatz Z.
-Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult Zminus Zopp Zeq_bool Zle_bool.
+Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult 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.
+ forall env, make_impl (eval_nformula env) l False.
Proof.
intros l cm H.
intro.
- unfold Zeval_nformula.
+ unfold eval_nformula.
apply (checker_nf_sound Zsor ZSORaddon l cm).
unfold ZWeakChecker in H.
exact H.
Qed.
+Definition psub := psub Z0 Zplus Zminus Zopp Zeq_bool.
+
+Definition padd := padd Z0 Zplus Zeq_bool.
+
+Definition norm := norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool.
+
+Definition eval_pol := eval_pol 0 Zplus Zmult (fun x => x).
+
+Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) = eval_pol env lhs - eval_pol env rhs.
+Proof.
+ intros.
+ apply (eval_pol_sub Zsor ZSORaddon).
+Qed.
+
+Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) = eval_pol env lhs + eval_pol env rhs.
+Proof.
+ intros.
+ apply (eval_pol_add Zsor ZSORaddon).
+Qed.
+
+Lemma eval_pol_norm : forall env e, eval_expr env e = eval_pol env (norm e) .
+Proof.
+ intros.
+ apply (eval_pol_norm Zsor ZSORaddon).
+Qed.
+
Definition xnormalise (t:Formula Z) : list (NFormula Z) :=
let (lhs,o,rhs) := t in
+ let lhs := norm lhs in
+ let rhs := norm rhs 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
+ ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
+ | OpNEq => (psub lhs rhs,Equal) :: nil
+ | OpGt => (psub rhs lhs,NonStrict) :: nil
+ | OpLt => (psub lhs rhs,NonStrict) :: nil
+ | OpGe => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
+ | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
end.
Require Import Tauto.
@@ -195,47 +200,64 @@ 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.
+Lemma normalise_correct : forall env t, eval_cnf (eval_nformula env) (normalise t) <-> Zeval_formula env t.
Proof.
- unfold normalise, xnormalise ; simpl ; intros env t.
+ Opaque padd.
+ 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;
+ destruct t as [lhs o rhs]; case_eq o; simpl;
+ repeat rewrite eval_pol_sub;
+ repeat rewrite eval_pol_add;
+ repeat rewrite <- eval_pol_norm ; simpl in *;
+ unfold eval_expr;
+ 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).
+ Transparent padd.
Qed.
Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) :=
let (lhs,o,rhs) := t in
+ let lhs := norm lhs in
+ let rhs := norm rhs 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
+ | OpEq => (psub lhs rhs,Equal) :: nil
+ | OpNEq => ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
+ | OpGt => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
+ | OpLt => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
+ | OpGe => (psub lhs rhs,NonStrict) :: nil
+ | OpLe => (psub 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.
+Lemma negate_correct : forall env t, eval_cnf (eval_nformula env) (negate t) <-> ~ Zeval_formula env t.
+Proof.
Proof.
- unfold negate, xnegate ; simpl ; intros env t.
+ Opaque padd.
+ intros env t.
rewrite Zeval_formula_compat.
+ unfold negate, xnegate ; simpl.
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 ;
+ destruct t as [lhs o rhs]; case_eq o; simpl;
+ repeat rewrite eval_pol_sub;
+ repeat rewrite eval_pol_add;
+ repeat rewrite <- eval_pol_norm ; simpl in *;
+ unfold eval_expr;
+ 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).
+ Transparent padd.
Qed.
+
Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
@tauto_checker (Formula Z) (NFormula Z) normalise negate ZWitness ZWeakChecker f w.
@@ -297,21 +319,16 @@ Proof.
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.
+Inductive ZArithProof : Type :=
+| DoneProof
+| RatProof : ZWitness -> ZArithProof -> ZArithProof
+| CutProof : ZWitness -> ZArithProof -> ZArithProof
+| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof.
(* 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).
@@ -341,95 +358,380 @@ Proof.
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.
+(* In order to compute the 'cut', we need to express a polynomial P as a * Q + b.
+ - b is the constant
+ - a is the gcd of the other coefficient.
+*)
+Require Import Znumtheory.
+Definition isZ0 (x:Z) :=
+ match x with
+ | Z0 => true
+ | _ => false
+ end.
-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
+Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.
+Proof.
+ destruct x ; simpl ; intuition congruence.
+Qed.
+
+Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0.
+Proof.
+ destruct x ; simpl ; intuition congruence.
+Qed.
+
+Definition ZgcdM (x y : Z) := Zmax (Zgcd x y) 1.
+
+
+Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) :=
+ match p with
+ | Pc c => (0,c)
+ | Pinj _ p => Zgcd_pol p
+ | PX p _ q =>
+ let (g1,c1) := Zgcd_pol p in
+ let (g2,c2) := Zgcd_pol q in
+ (ZgcdM (ZgcdM g1 c1) g2 , c2)
end.
+(*Eval compute in (Zgcd_pol ((PX (Pc (-2)) 1 (Pc 4)))).*)
-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
+
+Fixpoint Zdiv_pol (p:PolC Z) (x:Z) : PolC Z :=
+ match p with
+ | Pc c => Pc (Zdiv c x)
+ | Pinj j p => Pinj j (Zdiv_pol p x)
+ | PX p j q => PX (Zdiv_pol p x) j (Zdiv_pol q x)
end.
+
+Inductive Zdivide_pol (x:Z): PolC Z -> Prop :=
+| Zdiv_Pc : forall c, (x | c) -> Zdivide_pol x (Pc c)
+| Zdiv_Pinj : forall p, Zdivide_pol x p -> forall j, Zdivide_pol x (Pinj j p)
+| Zdiv_PX : forall p q, Zdivide_pol x p -> Zdivide_pol x q -> forall j, Zdivide_pol x (PX p j q).
+
+
+Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p ->
+ forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a).
Proof.
- destruct pf ; reflexivity.
+ intros until 2.
+ induction H0.
+ (* Pc *)
+ simpl.
+ intros.
+ apply Zdivide_Zdiv_eq ; auto.
+ (* Pinj *)
+ simpl.
+ intros.
+ apply IHZdivide_pol.
+ (* PX *)
+ simpl.
+ intros.
+ rewrite IHZdivide_pol1.
+ rewrite IHZdivide_pol2.
+ ring.
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
+Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
+Proof.
+ induction p.
+ simpl. auto with zarith.
+ simpl. auto.
+ simpl.
+ case_eq (Zgcd_pol p1).
+ case_eq (Zgcd_pol p3).
+ intros.
+ simpl.
+ unfold ZgcdM.
+ generalize (Zgcd_is_pos z1 z2).
+ generalize (Zmax_spec (Zgcd z1 z2) 1).
+ generalize (Zgcd_is_pos (Zmax (Zgcd z1 z2) 1) z).
+ generalize (Zmax_spec (Zgcd (Zmax (Zgcd z1 z2) 1) z) 1).
+ auto with zarith.
+Qed.
+
+Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p.
+Proof.
+ intros.
+ induction H.
+ constructor.
+ apply Zdivide_trans with (1:= H0) ; assumption.
+ constructor. auto.
+ constructor ; auto.
+Qed.
+
+Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
+Proof.
+ induction p ; constructor ; auto.
+ exists c. ring.
+Qed.
+
+
+Lemma Zgcd_minus : forall a b c, 0 < Zgcd a b -> (a | c - b ) -> (Zgcd a b | c).
+Proof.
+ intros.
+ destruct H0.
+ exists (q * (a / (Zgcd a b)) + (b / (Zgcd a b))).
+ rewrite Zmult_comm.
+ rewrite Zmult_plus_distr_r.
+ replace (Zgcd a b * (q * (a / Zgcd a b))) with (q * ((Zgcd a b) * (a / Zgcd a b))) by ring.
+ rewrite <- Zdivide_Zdiv_eq ; auto.
+ rewrite <- Zdivide_Zdiv_eq ; auto.
+ auto with zarith.
+ destruct (Zgcd_is_gcd a b) ; auto.
+ destruct (Zgcd_is_gcd a b) ; auto.
+Qed.
+
+Lemma Zdivide_pol_sub : forall p a b,
+ 0 < Zgcd a b ->
+ Zdivide_pol a (PsubC Zminus p b) ->
+ Zdivide_pol (Zgcd a b) p.
+Proof.
+ induction p.
+ simpl.
+ intros. inversion H0.
+ constructor.
+ apply Zgcd_minus ; auto.
+ intros.
+ constructor.
+ simpl in H0. inversion H0 ; subst; clear H0.
+ apply IHp ; auto.
+ simpl. intros.
+ inv H0.
+ constructor.
+ apply Zdivide_pol_Zdivide with (1:= H3).
+ destruct (Zgcd_is_gcd a b) ; assumption.
+ apply IHp2 ; assumption.
+Qed.
+
+Lemma Zgcd_com : forall a b, Zgcd a b = Zgcd b a.
+Proof.
+ intros.
+ apply Zis_gcd_gcd.
+ apply Zgcd_is_pos.
+ destruct (Zgcd_is_gcd b a).
+ constructor ; auto.
+Qed.
+
+Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
+Proof.
+ intros.
+ apply Zis_gcd_gcd.
+ apply (Zgcd_is_pos a (Zgcd b c)).
+ constructor ; auto.
+ destruct (Zgcd_is_gcd a b).
+ apply H1.
+ destruct (Zgcd_is_gcd a (Zgcd b c)) ; auto.
+ destruct (Zgcd_is_gcd a (Zgcd b c)) ; auto.
+ destruct (Zgcd_is_gcd b c) ; auto.
+ apply Zdivide_trans with (2:= H5);auto.
+ destruct (Zgcd_is_gcd b c).
+ destruct (Zgcd_is_gcd a (Zgcd b c)).
+ apply Zdivide_trans with (2:= H0);auto.
+ (* 3 *)
+ intros.
+ destruct (Zgcd_is_gcd a (Zgcd b c)).
+ apply H3.
+ destruct (Zgcd_is_gcd a b).
+ apply Zdivide_trans with (2:= H4) ; auto.
+ destruct (Zgcd_is_gcd b c).
+ apply H6.
+ destruct (Zgcd_is_gcd a b).
+ apply Zdivide_trans with (2:= H8) ; auto.
+ auto.
+Qed.
+
+
+Lemma Zdivide_pol_sub_0 : forall p a,
+ Zdivide_pol a (PsubC Zminus p 0) ->
+ Zdivide_pol a p.
+Proof.
+ induction p.
+ simpl.
+ intros. inversion H.
+ constructor. replace (c - 0) with c in H1 ; auto with zarith.
+ intros.
+ constructor.
+ simpl in H. inversion H ; subst; clear H.
+ apply IHp ; auto.
+ simpl. intros.
+ inv H.
+ constructor. auto.
+ apply IHp2 ; assumption.
+Qed.
+
+
+Lemma Zgcd_pol_div : forall p g c,
+ Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Zminus p c).
+Proof.
+ induction p ; simpl.
+ (* Pc *)
+ intros. inv H.
+ constructor.
+ exists 0. now ring.
+ (* Pinj *)
+ intros.
+ constructor. apply IHp ; auto.
+ (* PX *)
+ intros g c.
+ case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros.
+ inv H1.
+ unfold ZgcdM at 1.
+ destruct (Zmax_spec (Zgcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
+ destruct HH1 as [HH1 HH1'] ; rewrite HH1'.
+ constructor.
+ apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2).
+ unfold ZgcdM.
+ destruct (Zmax_spec (Zgcd z1 z2) 1) as [HH2 | HH2].
+ destruct HH2.
+ rewrite H2.
+ apply Zdivide_pol_sub ; auto.
+ auto with zarith.
+ destruct HH2. rewrite H2.
+ apply Zdivide_pol_one.
+ unfold ZgcdM in HH1. unfold ZgcdM.
+ destruct (Zmax_spec (Zgcd z1 z2) 1) as [HH2 | HH2].
+ destruct HH2. rewrite H2 in *.
+ destruct (Zgcd_is_gcd (Zgcd z1 z2) z); auto.
+ destruct HH2. rewrite H2.
+ destruct (Zgcd_is_gcd 1 z); auto.
+ apply Zdivide_pol_Zdivide with (x:= z).
+ apply (IHp2 _ _ H); auto.
+ destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto.
+ constructor. apply Zdivide_pol_one.
+ apply Zdivide_pol_one.
+Qed.
+
+
+
+
+Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) + c.
+Proof.
+ intros.
+ rewrite <- Zdiv_pol_correct ; auto.
+ rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
+ unfold eval_pol. ring.
+ (**)
+ apply Zgcd_pol_div ; auto.
+Qed.
+
+
+
+Definition makeCuttingPlane (p : PolC Z) : PolC Z * Z :=
+ let (g,c) := Zgcd_pol p in
+ if Zgt_bool g Z0
+ then (Zdiv_pol (PsubC Zminus p c) g , Zopp (ceiling (Zopp c) g))
+ else (p,Z0).
+
+
+Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) :=
+ let (e,op) := f in
+ match op with
+ | Equal => let (g,c) := Zgcd_pol e in
+ if andb (Zgt_bool g Z0) (andb (Zgt_bool c Z0) (negb (Zeq_bool (Zgcd g c) g)))
+ then None (* inconsistent *)
+ else Some (e, Z0,op) (* It could still be inconsistent -- but not a cut *)
+ | NonEqual => Some (e,Z0,op)
+ | Strict => let (p,c) := makeCuttingPlane (PsubC Zminus e 1) in
+ Some (p,c,NonStrict)
+ | NonStrict => let (p,c) := makeCuttingPlane e in
+ Some (p,c,NonStrict)
+ end.
+
+Definition nformula_of_cutting_plane (t : PolC Z * Z * Op1) : NFormula Z :=
+ let (e_z, o) := t in
+ let (e,z) := e_z in
+ (padd e (Pc z) , o).
+
+Definition is_pol_Z0 (p : PolC Z) : bool :=
+ match p with
+ | Pc Z0 => true
+ | _ => false
end.
-*)
-Fixpoint bdepth (pf : ProofTerm) : nat :=
+
+Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0.
+Proof.
+ unfold is_pol_Z0.
+ destruct p ; try discriminate.
+ destruct z ; try discriminate.
+ reflexivity.
+Qed.
+
+
+
+
+
+Definition eval_Psatz : list (NFormula Z) -> ZWitness -> option (NFormula Z) :=
+ eval_Psatz 0 1 Zplus Zmult Zeq_bool Zle_bool.
+
+
+Definition check_inconsistent := check_inconsistent 0 Zeq_bool Zle_bool.
+
+
+
+Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool :=
+ match pf with
+ | DoneProof => false
+ | RatProof w pf =>
+ match eval_Psatz l w with
+ | None => false
+ | Some f =>
+ if check_inconsistent f then true
+ else ZChecker (f::l) pf
+ end
+ | CutProof w pf =>
+ match eval_Psatz l w with
+ | None => false
+ | Some f =>
+ match genCuttingPlane f with
+ | None => true
+ | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf
+ end
+ end
+ | EnumProof w1 w2 pf =>
+ match eval_Psatz l w1 , eval_Psatz l w2 with
+ | Some f1 , Some f2 =>
+ match genCuttingPlane f1 , genCuttingPlane f2 with
+ |Some (e1,z1,op1) , Some (e2,z2,op2) =>
+ match op1 , op2 with
+ | NonStrict , NonStrict =>
+ if is_pol_Z0 (padd e1 e2)
+ then
+ (fix label (pfs:list ZArithProof) :=
+ fun lb ub =>
+ match pfs with
+ | nil => if Zgt_bool lb ub then true else false
+ | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
+ end)
+ pf (Zopp z1) z2
+ else false
+ | _ , _ => false
+ end
+ | _ , _ => false
+ end
+ | _ , _ => false
+ end
+ end.
+
+
+
+Fixpoint bdepth (pf : ZArithProof) : 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)
+ | DoneProof => O
+ | RatProof _ p => S (bdepth p)
+ | 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).
+Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l).
Proof.
induction l.
+ (* nil *)
simpl.
tauto.
+ (* cons *)
simpl.
intros.
destruct H.
@@ -437,207 +739,339 @@ Proof.
unfold ltof.
simpl.
generalize ( (fold_right
- (fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat l)).
+ (fun (pf : ZArithProof) (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).
+ auto with zarith.
+ generalize (IHl a0 b y H).
unfold ltof.
simpl.
- generalize ( (fold_right (fun (pf : ProofTerm) (x : nat) => Max.max (bdepth pf) x) 0%nat
+ generalize ( (fold_right (fun (pf : ZArithProof) (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.
+ auto with zarith.
Qed.
-Lemma lb_lbcut : forall env e q, Zeval_nformula env (makeLb e q) -> Zeval_nformula env (makeLbCut e q).
+
+Lemma eval_Psatz_sound : forall env w l f',
+ make_conj (eval_nformula env) l ->
+ eval_Psatz l w = Some f' -> eval_nformula env f'.
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.
+ intros.
+ apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto.
+ apply make_conj_in ; auto.
+Qed.
+
+Lemma makeCuttingPlane_sound : forall env e e' c,
+ eval_nformula env (e, NonStrict) ->
+ makeCuttingPlane e = (e',c) ->
+ eval_nformula env (nformula_of_cutting_plane (e', c, NonStrict)).
+Proof.
+ unfold nformula_of_cutting_plane.
+ unfold eval_nformula. unfold RingMicromega.eval_nformula.
+ unfold eval_op1.
+ intros.
+ rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
+ simpl.
+ (**)
+ unfold makeCuttingPlane in H0.
+ revert H0.
+ case_eq (Zgcd_pol e) ; intros g c0.
+ generalize (Zgt_cases g 0) ; destruct (Zgt_bool g 0).
+ intros.
+ inv H2.
+ change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in *.
+ apply Zgcd_pol_correct_lt with (env:=env) in H1.
+ generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Zminus e c0) g)) H0).
auto with zarith.
+ auto with zarith.
+ (* g <= 0 *)
+ intros. inv H2. 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).
+Lemma cutting_plane_sound : forall env f p,
+ eval_nformula env f ->
+ genCuttingPlane f = Some p ->
+ eval_nformula env (nformula_of_cutting_plane p).
Proof.
- unfold cutChecker.
+ unfold genCuttingPlane.
+ destruct f as [e op].
+ destruct op.
+ (* Equal *)
+ destruct p as [[e' z] op].
+ case_eq (Zgcd_pol e) ; intros g c.
+ destruct (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))) ; [discriminate|].
+ intros. inv H1. unfold nformula_of_cutting_plane.
+ unfold eval_nformula in *.
+ unfold RingMicromega.eval_nformula in *.
+ unfold eval_op1 in *.
+ rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
+ simpl. rewrite H0. reflexivity.
+ (* NonEqual *)
intros.
- revert H.
- case_eq (ZWeakChecker (neg_nformula (makeLb e lb) :: l) pf); intros ; [idtac | discriminate].
- generalize (ZWeakChecker_sound _ _ H env).
+ inv H0.
+ unfold eval_nformula in *.
+ unfold RingMicromega.eval_nformula in *.
+ unfold nformula_of_cutting_plane.
+ unfold eval_op1 in *.
+ rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
+ simpl. auto with zarith.
+ (* Strict *)
+ destruct p as [[e' z] op].
+ case_eq (makeCuttingPlane (PsubC Zminus e 1)).
intros.
- inversion H0 ; subst ; clear H0.
- apply -> make_conj_impl.
- simpl in H1.
- rewrite <- make_conj_impl in H1.
+ inv H1.
+ apply makeCuttingPlane_sound with (env:=env) (2:= H).
+ simpl in *.
+ rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
+ auto with zarith.
+ (* NonStrict *)
+ destruct p as [[e' z] op].
+ case_eq (makeCuttingPlane e).
intros.
- apply -> neg_nformula_sound ; auto.
- red ; intros.
- apply H1 ; auto.
- clear H H1 H0.
- generalize (lb_lbcut env e lb).
+ inv H1.
+ apply makeCuttingPlane_sound with (env:=env) (2:= H).
+ assumption.
+Qed.
+
+Lemma negb_true : forall x, negb x = true <-> x = false.
+Proof.
+ destruct x ; simpl; intuition.
+Qed.
+
+
+Lemma Zgcd_not_max : forall a b, 0 <= a -> Zgcd a b <> a -> ~ (a | b).
+Proof.
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.
+ intro. apply H0.
+ apply Zis_gcd_gcd; auto.
+ constructor ; auto.
+ exists 1. ring.
Qed.
+Lemma Zmod_Zopp_Zdivide : forall a b , a <> 0 -> (- b) mod a = 0 -> (a | b).
+Proof.
+ unfold Zmod.
+ intros a b.
+ generalize (Z_div_mod_full (-b) a).
+ destruct (Zdiv_eucl (-b) a).
+ intros.
+ subst.
+ exists (-z).
+ apply H in H0. destruct H0.
+ rewrite <- Zopp_mult_distr_l.
+ rewrite Zmult_comm. auto with zarith.
+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.
+Lemma ceiling_not_div : forall a b, a <> 0 -> ~ (a | b) -> ceiling (- b) a = Zdiv (-b) a + 1.
Proof.
+ unfold ceiling.
intros.
- generalize (cutChecker_sound _ _ _ _ _ H env).
+ assert ((-b) mod a <> 0).
+ generalize (Zmod_Zopp_Zdivide a b) ; tauto.
+ revert H1.
+ unfold Zdiv, Zmod.
+ generalize (Z_div_mod_full (-b) a).
+ destruct (Zdiv_eucl (-b) a).
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'.
+ destruct z0 ; congruence.
+Qed.
+
+
+Lemma genCuttingPlaneNone : forall env f,
+ genCuttingPlane f = None ->
+ eval_nformula env f -> False.
+Proof.
+ unfold genCuttingPlane.
+ destruct f.
+ destruct o.
+ case_eq (Zgcd_pol p) ; intros g c.
+ case_eq (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))).
+ intros.
+ flatten_bool.
+ rewrite negb_true in H5.
+ apply Zeq_bool_neq in H5.
+ rewrite <- Zgt_is_gt_bool in H3.
+ rewrite <- Zgt_is_gt_bool in H.
+ simpl in H2.
+ change (RingMicromega.eval_pol 0 Zplus Zmult (fun z => z)) with eval_pol in H2.
+ rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith.
+ revert H2.
+ generalize (eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) ; intro x.
+ intros.
+ assert (g * x >= -c) by auto with zarith.
+ assert (g * x <= -c) by auto with zarith.
+ apply narrow_interval_lower_bound in H4 ; auto.
+ apply narrow_interval_upper_bound in H6 ; auto.
+ apply Zgcd_not_max in H5; auto with zarith.
+ rewrite ceiling_not_div in H4.
auto with zarith.
+ auto with zarith.
+ auto.
+ (**)
discriminate.
+ discriminate.
+ destruct (makeCuttingPlane (PsubC Zminus p 1)) ; discriminate.
+ destruct (makeCuttingPlane p) ; discriminate.
Qed.
-Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (Zeval_nformula env) l False.
+
+Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False.
Proof.
induction w using (well_founded_ind (well_founded_ltof _ bdepth)).
- destruct w.
+ destruct w as [ | w pf | w pf | w1 w2 pf].
+ (* DoneProof *)
+ simpl. discriminate.
(* RatProof *)
simpl.
+ intro l. case_eq (eval_Psatz l w) ; [| discriminate].
+ intros f Hf.
+ case_eq (check_inconsistent f).
intros.
- eapply ZWeakChecker_sound.
- apply H0.
+ apply (checker_nf_sound Zsor ZSORaddon l w).
+ unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf.
+ unfold check_inconsistent in H0. assumption.
+ intros.
+ assert (make_impl (eval_nformula env) (f::l) False).
+ apply H with (2:= H1).
+ unfold ltof.
+ simpl.
+ auto with arith.
+ destruct f.
+ rewrite <- make_conj_impl in H2.
+ rewrite make_conj_cons in H2.
+ rewrite <- make_conj_impl.
+ intro.
+ apply H2.
+ split ; auto.
+ apply eval_Psatz_sound with (2:= Hf) ; assumption.
(* 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.
+ intro l.
+ case_eq (eval_Psatz l w) ; [ | discriminate].
+ intros f' Hlc.
+ case_eq (genCuttingPlane f').
+ intros.
+ assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
+ eapply (H pf) ; auto.
+ unfold ltof.
+ simpl.
+ auto with arith.
rewrite <- make_conj_impl in H2.
- rewrite <- make_conj_impl in H3.
+ rewrite make_conj_cons in H2.
rewrite <- make_conj_impl.
- tauto.
- discriminate.
+ intro.
+ apply H2.
+ split ; auto.
+ apply eval_Psatz_sound with (env:=env) in Hlc.
+ apply cutting_plane_sound with (1:= Hlc) (2:= H0).
+ auto.
+ (* genCuttingPlane = None *)
+ intros.
+ rewrite <- make_conj_impl.
+ intros.
+ apply eval_Psatz_sound with (2:= Hlc) in H2.
+ apply genCuttingPlaneNone with (2:= H2) ; auto.
(* EnumProof *)
intro.
- rewrite ZChecker_simpl.
- case_eq (cutChecker l0 p q z).
- rename q into llb.
- case_eq (cutChecker l0 (PEopp p) (- q0) z0).
+ simpl.
+ case_eq (eval_Psatz l w1) ; [ | discriminate].
+ case_eq (eval_Psatz l w2) ; [ | discriminate].
+ intros f1 Hf1 f2 Hf2.
+ case_eq (genCuttingPlane f2) ; [ | discriminate].
+ destruct p as [ [p1 z1] op1].
+ case_eq (genCuttingPlane f1) ; [ | discriminate].
+ destruct p as [ [p2 z2] op2].
+ case_eq op1 ; case_eq op2 ; try discriminate.
+ case_eq (is_pol_Z0 (padd p1 p2)) ; try discriminate.
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 :=
+ assert (-z1 <= eval_pol env p1 <= z2).
+ split.
+ apply eval_Psatz_sound with (env:=env) in Hf2 ; auto.
+ apply cutting_plane_sound with (1:= Hf2) in H4.
+ unfold nformula_of_cutting_plane in H4.
+ unfold eval_nformula in H4.
+ unfold RingMicromega.eval_nformula in H4.
+ change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H4.
+ unfold eval_op1 in H4.
+ rewrite eval_pol_add in H4. simpl in H4.
+ auto with zarith.
+ (**)
+ apply is_pol_Z0_eval_pol with (env := env) in H0.
+ rewrite eval_pol_add in H0.
+ replace (eval_pol env p1) with (- eval_pol env p2) by omega.
+ apply eval_Psatz_sound with (env:=env) in Hf1 ; auto.
+ apply cutting_plane_sound with (1:= Hf1) in H3.
+ unfold nformula_of_cutting_plane in H3.
+ unfold eval_nformula in H3.
+ unfold RingMicromega.eval_nformula in H3.
+ change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H3.
+ unfold eval_op1 in H3.
+ rewrite eval_pol_add in H3. simpl in H3.
+ omega.
+ revert H5.
+ set (FF := (fix label (pfs : list ZArithProof) (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 &&
+ (ZChecker ((PsubC Zminus p1 lb, Equal) :: l) 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.
+ assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
+ (In pr pf /\
+ ZChecker ((PsubC Zminus p1 x,Equal) :: l) pr = true)%Z).
clear H.
- revert H2.
- clear H4.
+ clear H0 H1 H2 H3 H4 H7.
+ revert H5.
+ generalize (-z1). clear z1. intro z1.
revert z1 z2.
- induction l;simpl ;intros.
- destruct (Z_gt_dec z1 z2).
+ induction pf;simpl ;intros.
+ generalize (Zgt_cases z1 z2).
+ destruct (Zgt_bool 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.
+ destruct (IHpf _ _ H1 _ H3).
+ destruct H4.
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.
+ destruct (HH _ H7) as [pr [Hin Hcheker]].
+ assert (make_impl (eval_nformula env) ((PsubC Zminus p1 (eval_pol env p1),Equal) :: l) False).
+ apply (H pr);auto.
+ apply in_bdepth ; auto.
+ rewrite <- make_conj_impl in H8.
+ apply H8.
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.
+ unfold eval_nformula.
+ unfold RingMicromega.eval_nformula.
+ simpl.
+ rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
+ unfold eval_pol. ring.
Qed.
-Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ProofTerm): bool :=
- @tauto_checker (Formula Z) (NFormula Z) normalise negate ProofTerm ZChecker f w.
+Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool :=
+ @tauto_checker (Formula Z) (NFormula Z) normalise negate ZArithProof 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 (tauto_checker_sound Zeval_formula eval_nformula).
apply Zeval_nformula_dec.
intros env t.
rewrite normalise_correct ; auto.
@@ -650,28 +1084,6 @@ 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.*)
@@ -688,7 +1100,7 @@ Definition leaf := @VarMap.Leaf Z.
Definition coneMember := ZWitness.
-Definition eval := Zeval_formula.
+Definition eval := eval_formula.
Definition prod_pos_nat := prod positive nat.
@@ -699,5 +1111,8 @@ Definition n_of_Z (z:Z) : BinNat.N :=
| Zneg p => N0
end.
-
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
+
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 5cce8ff97..229b1d0e1 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -263,10 +263,10 @@ let rec_simpl_cone n_spec e =
Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in
let rec rec_simpl_cone = function
- | Mc.S_Mult(t1, t2) ->
- simpl_cone (Mc.S_Mult (rec_simpl_cone t1, rec_simpl_cone t2))
- | Mc.S_Add(t1,t2) ->
- simpl_cone (Mc.S_Add (rec_simpl_cone t1, rec_simpl_cone t2))
+ | Mc.PsatzMulE(t1, t2) ->
+ simpl_cone (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2))
+ | Mc.PsatzAdd(t1,t2) ->
+ simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2))
| x -> simpl_cone x in
rec_simpl_cone e
@@ -286,28 +286,28 @@ let factorise_linear_cone c =
let rec cone_list c l =
match c with
- | Mc.S_Add (x,r) -> cone_list r (x::l)
+ | Mc.PsatzAdd (x,r) -> cone_list r (x::l)
| _ -> c :: l in
let factorise c1 c2 =
match c1 , c2 with
- | Mc.S_Ideal(x,y) , Mc.S_Ideal(x',y') ->
- if x = x' then Some (Mc.S_Ideal(x, Mc.S_Add(y,y'))) else None
- | Mc.S_Mult(x,y) , Mc.S_Mult(x',y') ->
- if x = x' then Some (Mc.S_Mult(x, Mc.S_Add(y,y'))) else None
+ | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') ->
+ if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
+ | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') ->
+ if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
| _ -> None in
let rec rebuild_cone l pending =
match l with
| [] -> (match pending with
- | None -> Mc.S_Z
+ | None -> Mc.PsatzZ
| Some p -> p
)
| e::l ->
(match pending with
| None -> rebuild_cone l (Some e)
| Some p -> (match factorise p e with
- | None -> Mc.S_Add(p, rebuild_cone l (Some e))
+ | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e))
| Some f -> rebuild_cone l (Some f) )
) in
@@ -405,34 +405,34 @@ let big_int_to_z = Ml2C.bigint
(* For Q, this is a pity that the certificate has been scaled
-- at a lower layer, certificates are using nums... *)
-let make_certificate n_spec cert li =
+let make_certificate n_spec (cert,li) =
let bint_to_cst = n_spec.bigint_to_number in
match cert with
- | [] -> None
+ | [] -> failwith "empty_certificate"
| e::cert' ->
let cst = match compare_big_int e zero_big_int with
- | 0 -> Mc.S_Z
- | 1 -> Mc.S_Pos (bint_to_cst e)
+ | 0 -> Mc.PsatzZ
+ | 1 -> Mc.PsatzC (bint_to_cst e)
| _ -> failwith "positivity error"
in
let rec scalar_product cert l =
match cert with
- | [] -> Mc.S_Z
+ | [] -> Mc.PsatzZ
| c::cert -> match l with
| [] -> failwith "make_certificate(1)"
| i::l ->
let r = scalar_product cert l in
match compare_big_int c zero_big_int with
- | -1 -> Mc.S_Add (
- Mc.S_Ideal (Mc.PEc ( bint_to_cst c), Mc.S_In (Ml2C.nat i)),
+ | -1 -> Mc.PsatzAdd (
+ Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)),
r)
| 0 -> r
- | _ -> Mc.S_Add (
- Mc.S_Mult (Mc.S_Pos (bint_to_cst c), Mc.S_In (Ml2C.nat i)),
+ | _ -> Mc.PsatzAdd (
+ Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)),
r) in
- Some ((factorise_linear_cone
- (simplify_cone n_spec (Mc.S_Add (cst, scalar_product cert' li)))))
+ ((factorise_linear_cone
+ (simplify_cone n_spec (Mc.PsatzAdd (cst, scalar_product cert' li)))))
exception Found of Monomial.t
@@ -494,11 +494,11 @@ let raw_certificate l =
dual_raw_certificate l
-let simple_linear_prover to_constant l =
+let simple_linear_prover (*to_constant*) l =
let (lc,li) = List.split l in
match raw_certificate lc with
| None -> None (* No certificate *)
- | Some cert -> make_certificate to_constant cert li
+ | Some cert -> (* make_certificate to_constant*)Some (cert,li)
@@ -511,13 +511,20 @@ let linear_prover n_spec l =
Mc.NonEqual -> failwith "cannot happen"
| y -> ((dev_form n_spec x, y),i)) l' in
- simple_linear_prover n_spec l'
+ simple_linear_prover (*n_spec*) l'
let linear_prover n_spec l =
try linear_prover n_spec l with
x -> (print_string (Printexc.to_string x); None)
+let linear_prover_with_cert spec l =
+ match linear_prover spec l with
+ | None -> None
+ | Some cert -> Some (make_certificate spec cert)
+
+
+
(* zprover.... *)
(* I need to gather the set of variables --->
@@ -560,7 +567,7 @@ let eq x y = Vect.compare x y = 0
let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l
-(* The prover is (probably) incomplete --
+(* The prover is (probably) incomplete --
only searching for naive cutting planes *)
let candidates sys =
@@ -581,9 +588,11 @@ let candidates sys =
else (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars
+
+
let rec xzlinear_prover planes sys =
match linear_prover z_spec sys with
- | Some prf -> Some (Mc.RatProof prf)
+ | Some prf -> Some (Mc.RatProof (make_certificate z_spec prf,Mc.DoneProof))
| None -> (* find the candidate with the smallest range *)
(* Grrr - linear_prover is also calling 'make_linear_system' *)
let ll = List.fold_right (fun (e,k) r -> match k with
@@ -635,7 +644,9 @@ let rec xzlinear_prover planes sys =
with
| None -> None
| Some prf ->
- Some (Mc.EnumProof(Ml2C.q lb,expr,Ml2C.q ub,clb,cub,prf)))
+ let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in
+
+ Some (Mc.EnumProof((*Ml2C.q lb,expr,Ml2C.q ub,*) bound_proof clb, bound_proof cub,prf)))
| _ -> None
)
| _ -> None
@@ -739,19 +750,29 @@ open Micromega
| Sub(t1,t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2)
| _ -> failwith "term_to_q_expr: not implemented"
+ let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e)
+
+
+ let rec product l =
+ match l with
+ | [] -> Mc.PsatzZ
+ | [i] -> Mc.PsatzIn (Ml2C.nat i)
+ | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l)
+
+
let q_cert_of_pos pos =
let rec _cert_of_pos = function
- Axiom_eq i -> Mc.S_In (Ml2C.nat i)
- | Axiom_le i -> Mc.S_In (Ml2C.nat i)
- | Axiom_lt i -> Mc.S_In (Ml2C.nat i)
- | Monoid l -> Mc.S_Monoid (List.map Ml2C.nat l)
+ Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i)
+ | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i)
+ | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i)
+ | Monoid l -> product l
| Rational_eq n | Rational_le n | Rational_lt n ->
- if compare_num n (Int 0) = 0 then Mc.S_Z else
- Mc.S_Pos (Ml2C.q n)
- | Square t -> Mc.S_Square (term_to_q_expr t)
- | Eqmul (t, y) -> Mc.S_Ideal(term_to_q_expr t, _cert_of_pos y)
- | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z)
- | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
+ if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+ Mc.PsatzC (Ml2C.q n)
+ | Square t -> Mc.PsatzSquare (term_to_q_pol t)
+ | Eqmul (t, y) -> Mc.PsatzMulC(term_to_q_pol t, _cert_of_pos y)
+ | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z)
+ | Product (y, z) -> Mc.PsatzMulE (_cert_of_pos y, _cert_of_pos z) in
simplify_cone q_spec (_cert_of_pos pos)
@@ -767,19 +788,24 @@ let q_cert_of_pos pos =
| Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2)
| _ -> failwith "term_to_z_expr: not implemented"
+ let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e)
+
let z_cert_of_pos pos =
let s,pos = (scale_certificate pos) in
let rec _cert_of_pos = function
- Axiom_eq i -> Mc.S_In (Ml2C.nat i)
- | Axiom_le i -> Mc.S_In (Ml2C.nat i)
- | Axiom_lt i -> Mc.S_In (Ml2C.nat i)
- | Monoid l -> Mc.S_Monoid (List.map Ml2C.nat l)
+ Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i)
+ | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i)
+ | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i)
+ | Monoid l -> product l
| Rational_eq n | Rational_le n | Rational_lt n ->
- if compare_num n (Int 0) = 0 then Mc.S_Z else
- Mc.S_Pos (Ml2C.bigint (big_int_of_num n))
- | Square t -> Mc.S_Square (term_to_z_expr t)
- | Eqmul (t, y) -> Mc.S_Ideal(term_to_z_expr t, _cert_of_pos y)
- | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z)
- | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
+ if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+ Mc.PsatzC (Ml2C.bigint (big_int_of_num n))
+ | Square t -> Mc.PsatzSquare (term_to_z_pol t)
+ | Eqmul (t, y) -> Mc.PsatzMulC(term_to_z_pol t, _cert_of_pos y)
+ | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z)
+ | Product (y, z) -> Mc.PsatzMulE (_cert_of_pos y, _cert_of_pos z) in
simplify_cone z_spec (_cert_of_pos pos)
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2d9dc781f..66fe5335c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -24,7 +24,7 @@ let time str f x =
res
-type tag = int
+type tag = Tag.t
type 'cst atom = 'cst Micromega.formula
type 'cst formula =
@@ -43,7 +43,7 @@ let rec pp_formula o f =
| TT -> output_string o "tt"
| FF -> output_string o "ff"
| X c -> output_string o "X "
- | A(_,t,_) -> Printf.fprintf o "A(%i)" t
+ | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t
| C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2
| D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2
| I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)"
@@ -58,12 +58,15 @@ let rec ids_of_formula f =
| I(f1,Some id,f2) -> id::(ids_of_formula f2)
| _ -> []
-(* obsolete *)
+module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
-let tag_formula t f = f (* to be removed *)
-(* obsolete *)
+let selecti s m =
+ let rec xselect i m =
+ match m with
+ | [] -> []
+ | e::m -> if ISet.mem i s then e:: (xselect (i+1) m) else xselect (i+1) m in
+ xselect 0 m
-module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
type 'cst clause = ('cst Micromega.nFormula * tag) list
@@ -107,6 +110,7 @@ let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf)
xcnf true f
+
module M =
struct
open Coqlib
@@ -191,7 +195,8 @@ struct
let coq_R1 = lazy (constant "R1")
- let coq_proofTerm = lazy (constant "ProofTerm")
+ let coq_proofTerm = lazy (constant "ZArithProof")
+ let coq_doneProof = lazy (constant "DoneProof")
let coq_ratProof = lazy (constant "RatProof")
let coq_cutProof = lazy (constant "CutProof")
let coq_enumProof = lazy (constant "EnumProof")
@@ -245,6 +250,10 @@ struct
let coq_PEsub = lazy (constant "PEsub")
let coq_PEpow = lazy (constant "PEpow")
+ let coq_PX = lazy (constant "PX" )
+ let coq_Pc = lazy (constant"Pc")
+ let coq_Pinj = lazy (constant "Pinj")
+
let coq_OpEq = lazy (constant "OpEq")
let coq_OpNEq = lazy (constant "OpNEq")
@@ -254,14 +263,13 @@ struct
let coq_OpGt = lazy (constant "OpGt")
- let coq_S_In = lazy (constant "S_In")
- let coq_S_Square = lazy (constant "S_Square")
- let coq_S_Monoid = lazy (constant "S_Monoid")
- let coq_S_Ideal = lazy (constant "S_Ideal")
- let coq_S_Mult = lazy (constant "S_Mult")
- let coq_S_Add = lazy (constant "S_Add")
- let coq_S_Pos = lazy (constant "S_Pos")
- let coq_S_Z = lazy (constant "S_Z")
+ let coq_PsatzIn = lazy (constant "PsatzIn")
+ let coq_PsatzSquare = lazy (constant "PsatzSquare")
+ let coq_PsatzMulE = lazy (constant "PsatzMulE")
+ let coq_PsatzMultC = lazy (constant "PsatzMulC")
+ let coq_PsatzAdd = lazy (constant "PsatzAdd")
+ let coq_PsatzC = lazy (constant "PsatzC")
+ let coq_PsatzZ = lazy (constant "PsatzZ")
let coq_coneMember = lazy (constant "coneMember")
@@ -465,47 +473,64 @@ let parse_q term =
in
dump_expr e
- let rec dump_monoid l = dump_list (Lazy.force coq_nat) dump_nat l
- let rec dump_cone typ dump_z e =
+ let dump_pol typ dump_c e =
+ let rec dump_pol e =
+ match e with
+ | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
+ | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
+ | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
+ dump_pol e
+
+ let pp_pol pp_c o e =
+ let rec pp_pol o e =
+ match e with
+ | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
+ | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
+ | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
+ pp_pol o e
+
+
+ let pp_cnf pp_c o f =
+ let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) l in
+ List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f
+
+
+ let dump_psatz typ dump_z e =
let z = Lazy.force typ in
let rec dump_cone e =
match e with
- | Mc.S_In n -> mkApp(Lazy.force coq_S_In,[| z; dump_nat n |])
- | Mc.S_Ideal(e,c) -> mkApp(Lazy.force coq_S_Ideal,
- [| z; dump_expr z dump_z e ; dump_cone c |])
- | Mc.S_Square e -> mkApp(Lazy.force coq_S_Square,
- [| z;dump_expr z dump_z e|])
- | Mc.S_Monoid l -> mkApp (Lazy.force coq_S_Monoid,
- [|z; dump_monoid l|])
- | Mc.S_Add(e1,e2) -> mkApp(Lazy.force coq_S_Add,
+ | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
+ | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC,
+ [| z; dump_pol z dump_z e ; dump_cone c |])
+ | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare,
+ [| z;dump_pol z dump_z e|])
+ | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd,
[| z; dump_cone e1; dump_cone e2|])
- | Mc.S_Mult(e1,e2) -> mkApp(Lazy.force coq_S_Mult,
+ | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE,
[| z; dump_cone e1; dump_cone e2|])
- | Mc.S_Pos p -> mkApp(Lazy.force coq_S_Pos,[| z; dump_z p|])
- | Mc.S_Z -> mkApp( Lazy.force coq_S_Z,[| z|]) in
+ | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
+ | Mc.PsatzZ -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in
dump_cone e
- let pp_cone pp_z o e =
+ let pp_psatz pp_z o e =
let rec pp_cone o e =
match e with
- | Mc.S_In n ->
- Printf.fprintf o "(S_In %a)%%nat" pp_nat n
- | Mc.S_Ideal(e,c) ->
- Printf.fprintf o "(S_Ideal %a %a)" (pp_expr pp_z) e pp_cone c
- | Mc.S_Square e ->
- Printf.fprintf o "(S_Square %a)" (pp_expr pp_z) e
- | Mc.S_Monoid l ->
- Printf.fprintf o "(S_Monoid %a)" (pp_list "[" "]" pp_nat) l
- | Mc.S_Add(e1,e2) ->
- Printf.fprintf o "(S_Add %a %a)" pp_cone e1 pp_cone e2
- | Mc.S_Mult(e1,e2) ->
- Printf.fprintf o "(S_Mult %a %a)" pp_cone e1 pp_cone e2
- | Mc.S_Pos p ->
- Printf.fprintf o "(S_Pos %a)%%positive" pp_z p
- | Mc.S_Z ->
- Printf.fprintf o "S_Z" in
+ | Mc.PsatzIn n ->
+ Printf.fprintf o "(In %a)%%nat" pp_nat n
+ | Mc.PsatzMulC(e,c) ->
+ Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
+ | Mc.PsatzSquare e ->
+ Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
+ | Mc.PsatzAdd(e1,e2) ->
+ Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
+ | Mc.PsatzMulE(e1,e2) ->
+ Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
+ | Mc.PsatzC p ->
+ Printf.fprintf o "(%a)%%positive" pp_z p
+ | Mc.PsatzZ ->
+ Printf.fprintf o "0" in
pp_cone o e
@@ -651,6 +676,7 @@ let parse_q term =
let (expr1,env) = parse_expr env t1 in
let (expr2,env) = parse_expr env t2 in
(op expr1 expr2,env) in
+
match kind_of_term term with
| App(t,args) ->
(
@@ -661,9 +687,14 @@ let parse_q term =
| Opp -> let (expr,env) = parse_expr env args.(0) in
(Mc.PEopp expr, env)
| Power ->
- let (expr,env) = parse_expr env args.(0) in
- let exp = (parse_exp args.(1)) in
- (Mc.PEpow(expr, exp) , env)
+ begin
+ try
+ let (expr,env) = parse_expr env args.(0) in
+ let exp = (parse_exp args.(1)) in
+ (Mc.PEpow(expr, exp) , env)
+ with _ -> (* if the exponent is a variable *)
+ let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
+ end
| Ukn s ->
if debug
then (Printf.printf "unknown op: %s\n" s; flush stdout;);
@@ -784,7 +815,7 @@ let parse_rexpr =
let parse_formula parse_atom env term =
let parse_atom env tg t = try let (at,env) = parse_atom env t in
- (A(at,tg,t), env,tg+1) with _ -> (X(t),env,tg) in
+ (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
let rec xparse_formula env tg term =
match kind_of_term term with
@@ -877,11 +908,11 @@ open M
let rec sig_of_cone = function
- | Mc.S_In n -> [CoqToCaml.nat n]
- | Mc.S_Ideal(e,w) -> sig_of_cone w
- | Mc.S_Mult(w1,w2) ->
+ | Mc.PsatzIn n -> [CoqToCaml.nat n]
+ | Mc.PsatzMulE(w1,w2) ->
(sig_of_cone w1)@(sig_of_cone w2)
- | Mc.S_Add(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2)
+ | Mc.PsatzMulC(w1,w2) -> (sig_of_cone w2)
+ | Mc.PsatzAdd(w1,w2) -> (sig_of_cone w1)@(sig_of_cone w2)
| _ -> []
let same_proof sg cl1 cl2 =
@@ -897,10 +928,10 @@ let same_proof sg cl1 cl2 =
let tags_of_clause tgs wit clause =
let rec xtags tgs = function
- | Mc.S_In n -> Names.Idset.union tgs
+ | Mc.PsatzIn n -> Names.Idset.union tgs
(snd (List.nth clause (CoqToCaml.nat n) ))
- | Mc.S_Ideal(e,w) -> xtags tgs w
- | Mc.S_Mult (w1,w2) | Mc.S_Add(w1,w2) -> xtags (xtags tgs w1) w2
+ | Mc.PsatzMulC(e,w) -> xtags tgs w
+ | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2
| _ -> tgs in
xtags tgs wit
@@ -975,29 +1006,28 @@ let rec pp_varmap o vm =
let rec dump_proof_term = function
- | Micromega.RatProof cone ->
- Term.mkApp(Lazy.force coq_ratProof, [|dump_cone coq_Z dump_z cone|])
- | Micromega.CutProof(e,q,cone,prf) ->
+ | Micromega.DoneProof -> Lazy.force coq_doneProof
+ | Micromega.RatProof(cone,rst) ->
+ Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|])
+ | Micromega.CutProof(cone,prf) ->
Term.mkApp(Lazy.force coq_cutProof,
- [| dump_expr (Lazy.force coq_Z) dump_z e ;
- dump_q q ;
- dump_cone coq_Z dump_z cone ;
+ [| dump_psatz coq_Z dump_z cone ;
dump_proof_term prf|])
- | Micromega.EnumProof( q1,e1,q2,c1,c2,prfs) ->
+ | Micromega.EnumProof(c1,c2,prfs) ->
Term.mkApp (Lazy.force coq_enumProof,
- [| dump_q q1 ; dump_expr (Lazy.force coq_Z) dump_z e1 ; dump_q q2;
- dump_cone coq_Z dump_z c1 ; dump_cone coq_Z dump_z c2 ;
+ [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ;
dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |])
let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden
let rec pp_proof_term o = function
- | Micromega.RatProof cone -> Printf.fprintf o "R[%a]" (pp_cone pp_z) cone
- | Micromega.CutProof(e,q,_,p) -> failwith "not implemented"
- | Micromega.EnumProof(q1,e1,q2,c1,c2,rst) ->
- Printf.fprintf o "EP[%a,%a,%a,%a,%a,%a]"
- pp_q q1 (pp_expr pp_z) e1 pp_q q2 (pp_cone pp_z) c1 (pp_cone pp_z) c2
+ | Micromega.DoneProof -> Printf.fprintf o "D"
+ | Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+ | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+ | Micromega.EnumProof(c1,c2,rst) ->
+ Printf.fprintf o "EP[%a,%a,%a]"
+ (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
(pp_list "[" "]" pp_proof_term) rst
let rec parse_hyps parse_arith env tg hyps =
@@ -1016,7 +1046,7 @@ exception ParseError
let parse_goal parse_arith env hyps term =
(* try*)
- let (f,env,tg) = parse_formula parse_arith env 0 term in
+ let (f,env,tg) = parse_formula parse_arith env (Tag.from 0) term in
let (lhyps,env,tg) = parse_hyps parse_arith env tg hyps in
(lhyps,f,env)
(* with Failure x -> raise ParseError*)
@@ -1043,7 +1073,7 @@ let qq_domain_spec = lazy {
coeff = Lazy.force coq_Q;
dump_coeff = dump_q ;
proof_typ = Lazy.force coq_QWitness ;
- dump_proof = dump_cone coq_Q dump_q
+ dump_proof = dump_psatz coq_Q dump_q
}
let rz_domain_spec = lazy {
@@ -1051,7 +1081,7 @@ let rz_domain_spec = lazy {
coeff = Lazy.force coq_Z;
dump_coeff = dump_z;
proof_typ = Lazy.force coq_ZWitness ;
- dump_proof = dump_cone coq_Z dump_z
+ dump_proof = dump_psatz coq_Z dump_z
}
@@ -1060,7 +1090,7 @@ let abstract_formula hyps f =
let rec xabs f =
match f with
| X c -> X c
- | A(a,t,term) -> if ISet.mem t hyps then A(a,t,term) else X(term)
+ | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
| C(f1,f2) ->
(match xabs f1 , xabs f2 with
| X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|]))
@@ -1079,8 +1109,10 @@ let abstract_formula hyps f =
| X a1 , None , X a2 -> X (Term.mkArrow a1 a2)
| af1 , _ , af2 -> I(af1,hyp,af2)
)
- | x -> x in
- xabs f
+ | FF -> FF
+ | TT -> TT
+
+ in xabs f
@@ -1125,21 +1157,6 @@ let find_witness provers polys1 =
try_any provers (List.map fst polys1)
-let witness_list_tags prover l =
-
- let rec xwitness_list l =
- match l with
- | [] -> Some([])
- | e::l ->
- match find_witness prover e with
- | None -> None
- | Some w ->
- (match xwitness_list l with
- | None -> None
- | Some l -> Some (w::l)
- ) in
- xwitness_list l
-
let witness_list prover l =
let rec xwitness_list l =
match l with
@@ -1155,6 +1172,8 @@ let witness_list prover l =
xwitness_list l
+let witness_list_tags = witness_list
+
let is_singleton = function [] -> true | [e] -> true | _ -> false
let pp_ml_list pp_elt o l =
@@ -1167,7 +1186,6 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
let new_cl = Mutils.mapi (fun (f,_) i -> (f,i)) new_cl in
let remap i =
- (*Printf.printf "nth (len:%i) %i\n" (List.length old_cl) i;*)
let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in
List.assoc formula new_cl in
@@ -1179,12 +1197,13 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
(pp_ml_list prover.pp_f) (List.map fst new_cl) ;
flush stdout
end ;
- let res = try prover.compact prf remap with x ->
+ let res = try prover.compact prf remap with x ->
+ if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
+
match prover.prover (List.map fst new_cl) with
- | None -> failwith "prover error"
+ | None -> failwith "proof compaction error"
| Some p -> p
in
-
if debug then
begin
Printf.printf " -> %a\n"
@@ -1194,11 +1213,19 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
;
res in
+
+
+ let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
+ let hyps_idx = prover.hyps prf in
+ let hyps = selecti hyps_idx old_cl in
+ is_sublist hyps new_cl in
+
let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
- let l = (* This is not the right criterion for matching clauses *)
- List.map (fun x -> let (o,p) = List.find (fun lp -> is_sublist x (fst lp)) cnf_res in (o,p,x)) cnf_ff' in
- List.map (fun (o,p,n) -> compact_proof o p n) l
+ List.map (fun x ->
+ let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res
+ in compact_proof o p x) cnf_ff'
+
@@ -1220,33 +1247,47 @@ let micromega_tauto negate normalise spec prover env polys1 polys2 gl =
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ()
+ Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
match witness_list_tags prover cnf_ff with
| None -> Tacticals.tclFAIL 0 (Pp.str "Cannot find witness") gl
- | Some res -> (*Printf.printf "\nList %i" (List.length res); *)
+ | Some res -> (*Printf.printf "\nList %i" (List.length `res); *)
+
let hyps = List.fold_left (fun s (cl,(prf,p)) ->
- let tags = ISet.fold (fun i s -> try ISet.add (snd (List.nth cl i)) s with Invalid_argument _ -> s) (p.hyps prf) ISet.empty in
- ISet.union s tags) ISet.empty (List.combine cnf_ff res) in
+ let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in
+ if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ;
+ (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in
+ TagSet.union s tags) TagSet.empty (List.combine cnf_ff res) in
if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout;
- Printf.printf "Hyps : %a\n" (fun o s -> ISet.fold (fun i _ -> Printf.fprintf o "%i " i) s ()) hyps) ;
+ Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;
let ff' = abstract_formula hyps ff in
+ let cnf_ff' = cnf negate normalise ff' in
+
if debug then
begin
Pp.pp (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ()
+ Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
-
- let cnf_ff' = cnf negate normalise ff' in
- let res' = compact_proofs cnf_ff res cnf_ff' in
+ (* Even if it does not work, this does not mean it is not provable
+ -- the prover is REALLY incomplete *)
+(* if debug then
+ begin
+ (* recompute the proofs *)
+ match witness_list_tags prover cnf_ff' with
+ | None -> failwith "abstraction is wrong"
+ | Some res -> ()
+ end ; *)
+ let res' = compact_proofs cnf_ff res cnf_ff' in
let (ff',res',ids) = (ff',res',List.map Term.mkVar (ids_of_formula ff')) in
@@ -1276,41 +1317,65 @@ let micromega_gen
| ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
-let lift_ratproof prover l =
+let lift_ratproof prover l =
match prover l with
| None -> None
- | Some c -> Some (Mc.RatProof c)
-
+ | Some c -> Some (Mc.RatProof( c,Mc.DoneProof))
type csdpcert = Sos.positivstellensatz option
-type micromega_polys = (Micromega.q Mc.pExpr * Mc.op1) list
+type micromega_polys = (Mc.q Mc.pol * Mc.op1) list
type provername = string * int option
-let call_csdpcert provername poly =
- let tmp_to,ch_to = Filename.open_temp_file "csdpcert" ".in" in
- let tmp_from = Filename.temp_file "csdpcert" ".out" in
- output_value ch_to (provername,poly : provername * micromega_polys);
- close_out ch_to;
+open Persistent_cache
+
+module Cache = PHashtable(struct
+ type t = (provername * micromega_polys)
+ let equal = (=)
+ let hash = Hashtbl.hash
+end)
+
+let cache_name = "csdp.cache"
+
+let cache = lazy (Cache.open_in cache_name)
+
+
+let really_call_csdpcert : provername -> micromega_polys -> csdpcert =
+ fun provername poly ->
+
let cmdname =
List.fold_left Filename.concat (Envars.coqlib ())
["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
- let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
- (try Sys.remove tmp_to with _ -> ());
- if c <> 0 then Util.error ("Failed to call csdp certificate generator");
- let ch_from = open_in tmp_from in
- let cert = (input_value ch_from : csdpcert) in
- close_in ch_from; Sys.remove tmp_from;
- cert
-
-let rec z_to_q_expr e =
+
+ command cmdname [| cmdname |] (provername,poly)
+
+
+
+let call_csdpcert prover pb =
+
+ let cache = Lazy.force cache in
+ try
+ Cache.find cache (prover,pb)
+ with Not_found ->
+ let cert = really_call_csdpcert prover pb in
+ Cache.add cache (prover,pb) cert ;
+ cert
+
+
+
+
+
+
+
+
+
+
+
+
+let rec z_to_q_pol e =
match e with
- | Mc.PEc z -> Mc.PEc {Mc.qnum = z ; Mc.qden = Mc.XH}
- | Mc.PEX x -> Mc.PEX x
- | Mc.PEadd(e1,e2) -> Mc.PEadd(z_to_q_expr e1, z_to_q_expr e2)
- | Mc.PEsub(e1,e2) -> Mc.PEsub(z_to_q_expr e1, z_to_q_expr e2)
- | Mc.PEmul(e1,e2) -> Mc.PEmul(z_to_q_expr e1, z_to_q_expr e2)
- | Mc.PEopp(e) -> Mc.PEopp(z_to_q_expr e)
- | Mc.PEpow(e,n) -> Mc.PEpow(z_to_q_expr e,n)
+ | Mc.Pc z -> Mc.Pc {Mc.qnum = z ; Mc.qden = Mc.XH}
+ | Mc.Pinj(p,pol) -> Mc.Pinj(p,z_to_q_pol pol)
+ | Mc.PX(pol1,p,pol2) -> Mc.PX(z_to_q_pol pol1, p, z_to_q_pol pol2)
let call_csdpcert_q provername poly =
@@ -1324,7 +1389,7 @@ let call_csdpcert_q provername poly =
let call_csdpcert_z provername poly =
- let l = List.map (fun (e,o) -> (z_to_q_expr e,o)) poly in
+ let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
match call_csdpcert provername l with
| None -> None
| Some cert ->
@@ -1334,45 +1399,51 @@ let call_csdpcert_z provername poly =
else ((print_string "buggy certificate" ; flush stdout) ;None)
-let hyps_of_cone prf =
+let xhyps_of_cone base acc prf =
let rec xtract e acc =
match e with
- | Mc.S_Pos _ | Mc.S_Z | Mc.S_Square _ -> acc
- | Mc.S_In n -> ISet.add (CoqToCaml.nat n) acc
- | Mc.S_Ideal(_,c) -> xtract c acc
- | Mc.S_Monoid [] -> acc
- | Mc.S_Monoid (i::l) -> xtract (Mc.S_Monoid l) (ISet.add (CoqToCaml.nat i) acc)
- | Mc.S_Add(e1,e2) | Mc.S_Mult(e1,e2) -> xtract e1 (xtract e2 acc) in
+ | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc
+ | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in
+ if n >= base
+ then ISet.add (n-base) acc
+ else acc
+ | Mc.PsatzMulC(_,c) -> xtract c acc
+ | Mc.PsatzAdd(e1,e2) | Mc.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in
+
+ xtract prf acc
- xtract prf ISet.empty
+let hyps_of_cone prf = xhyps_of_cone 0 ISet.empty prf
let compact_cone prf f =
let np n = CamlToCoq.nat (f (CoqToCaml.nat n)) in
let rec xinterp prf =
match prf with
- | Mc.S_Pos _ | Mc.S_Z | Mc.S_Square _ -> prf
- | Mc.S_In n -> Mc.S_In (np n)
- | Mc.S_Ideal(e,c) -> Mc.S_Ideal(e,xinterp c)
- | Mc.S_Monoid l -> Mc.S_Monoid (Mc.map np l)
- | Mc.S_Add(e1,e2) -> Mc.S_Add(xinterp e1,xinterp e2)
- | Mc.S_Mult(e1,e2) -> Mc.S_Mult(xinterp e1,xinterp e2) in
+ | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> prf
+ | Mc.PsatzIn n -> Mc.PsatzIn (np n)
+ | Mc.PsatzMulC(e,c) -> Mc.PsatzMulC(e,xinterp c)
+ | Mc.PsatzAdd(e1,e2) -> Mc.PsatzAdd(xinterp e1,xinterp e2)
+ | Mc.PsatzMulE(e1,e2) -> Mc.PsatzMulE(xinterp e1,xinterp e2) in
xinterp prf
-
let hyps_of_pt pt =
- let translate x s = ISet.fold (fun i s -> ISet.add (i - x) s) s ISet.empty in
-
- let rec xhyps ofset pt acc =
+ let rec xhyps base pt acc =
match pt with
- | Mc.RatProof p -> ISet.union acc (translate ofset (hyps_of_cone p))
- | Mc.CutProof(_,_,c,pt) -> xhyps (ofset+1) pt (ISet.union (translate (ofset+1) (hyps_of_cone c)) acc)
- | Mc.EnumProof(_,_,_,c1,c2,l) ->
- let s = ISet.union acc (translate (ofset +1) (ISet.union (hyps_of_cone c1) (hyps_of_cone c2))) in
- List.fold_left (fun s x -> xhyps (ofset + 1) x s) s l in
+ | Mc.DoneProof -> acc
+ | Mc.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
+ | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
+ | Mc.EnumProof(c1,c2,l) ->
+ let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
+ List.fold_left (fun s x -> xhyps (base + 1) x s) s l in
xhyps 0 pt ISet.empty
+
+let hyps_of_pt pt =
+ let res = hyps_of_pt pt in
+ if debug
+ then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res);
+ res
let compact_pt pt f =
@@ -1382,39 +1453,44 @@ let compact_pt pt f =
let rec compact_pt ofset pt =
match pt with
- | Mc.RatProof p -> Mc.RatProof (compact_cone p (translate ofset))
- | Mc.CutProof(x,y,c,pt) -> Mc.CutProof(x,y,compact_cone c (translate (ofset+1)), compact_pt (ofset+1) pt )
- | Mc.EnumProof(a,b,c,c1,c2,l) -> Mc.EnumProof(a,b,c,compact_cone c1 (translate (ofset+1)), compact_cone c2 (translate (ofset+1)),
+ | Mc.DoneProof -> Mc.DoneProof
+ | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+ | Mc.CutProof(c,pt) -> Mc.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+ | Mc.EnumProof(c1,c2,l) -> Mc.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)),
Mc.map (fun x -> compact_pt (ofset+1) x) l) in
compact_pt 0 pt
+
+
(** Definition of provers *)
-
+
+let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l)
+
let linear_prover_Z = {
name = "linear prover" ;
- prover = lift_ratproof (Certificate.linear_prover Certificate.z_spec) ;
+ prover = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ;
hyps = hyps_of_pt ;
compact = compact_pt ;
pp_prf = pp_proof_term;
- pp_f = fun o x -> pp_expr pp_z o (fst x)
+ pp_f = fun o x -> pp_pol pp_z o (fst x)
}
let linear_prover_Q = {
name = "linear prover";
- prover = (Certificate.linear_prover Certificate.q_spec) ;
+ prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
hyps = hyps_of_cone ;
compact = compact_cone ;
- pp_prf = pp_cone pp_q ;
- pp_f = fun o x -> pp_expr pp_q o (fst x)
+ pp_prf = pp_psatz pp_q ;
+ pp_f = fun o x -> pp_pol pp_q o (fst x)
}
let linear_prover_R = {
name = "linear prover";
- prover = (Certificate.linear_prover Certificate.z_spec) ;
+ prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec) ;
hyps = hyps_of_cone ;
compact = compact_cone ;
- pp_prf = pp_cone pp_z ;
- pp_f = fun o x -> pp_expr pp_z o (fst x)
+ pp_prf = pp_psatz pp_z ;
+ pp_f = fun o x -> pp_pol pp_z o (fst x)
}
let non_linear_prover_Q str o = {
@@ -1422,8 +1498,8 @@ let non_linear_prover_Q str o = {
prover = call_csdpcert_q (str, o);
hyps = hyps_of_cone;
compact = compact_cone ;
- pp_prf = pp_cone pp_q ;
- pp_f = fun o x -> pp_expr pp_q o (fst x)
+ pp_prf = pp_psatz pp_q ;
+ pp_f = fun o x -> pp_pol pp_q o (fst x)
}
let non_linear_prover_R str o = {
@@ -1431,8 +1507,8 @@ let non_linear_prover_R str o = {
prover = call_csdpcert_z (str, o);
hyps = hyps_of_cone;
compact = compact_cone;
- pp_prf = pp_cone pp_z;
- pp_f = fun o x -> pp_expr pp_z o (fst x)
+ pp_prf = pp_psatz pp_z;
+ pp_f = fun o x -> pp_pol pp_z o (fst x)
}
let non_linear_prover_Z str o = {
@@ -1441,16 +1517,19 @@ let non_linear_prover_Z str o = {
hyps = hyps_of_pt;
compact = compact_pt;
pp_prf = pp_proof_term;
- pp_f = fun o x -> pp_expr pp_z o (fst x)
+ pp_f = fun o x -> pp_pol pp_z o (fst x)
}
+
+
+
let linear_Z = {
name = "lia";
- prover = Certificate.zlinear_prover ;
+ prover = lift_pexpr_prover Certificate.zlinear_prover ;
hyps = hyps_of_pt;
compact = compact_pt;
pp_prf = pp_proof_term;
- pp_f = fun o x -> pp_expr pp_z o (fst x)
+ pp_f = fun o x -> pp_pol pp_z o (fst x)
}
@@ -1461,22 +1540,23 @@ let psatzl_Z gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
[linear_prover_Z ] gl
+
let psatzl_Q gl =
- micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
[ linear_prover_Q ] gl
let psatz_Q i gl =
- micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
[ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl
let psatzl_R gl =
- micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+ micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
[ linear_prover_R ] gl
let psatz_R i gl =
- micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+ micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
[ non_linear_prover_R "real_nonlinear_prover" (Some i)] gl
@@ -1490,12 +1570,12 @@ let sos_Z gl =
[non_linear_prover_Z "pure_sos" None] gl
let sos_Q gl =
- micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
[non_linear_prover_Q "pure_sos" None] gl
let sos_R gl =
- micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+ micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
[non_linear_prover_R "pure_sos" None] gl
@@ -1503,3 +1583,7 @@ let sos_R gl =
let xlia gl =
micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
[linear_Z] gl
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 38810b2c5..3bc81c576 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -40,16 +40,6 @@ struct
| PEopp p -> Opp (expr_to_term p)
-
-
-(* let term_to_expr e =
- let e' = term_to_expr e in
- if debug
- then Printf.printf "term_to_expr : %s - %s\n"
- (string_of_poly (poly_of_term e))
- (string_of_poly (poly_of_term (expr_to_term e')));
- e' *)
-
end
open M
@@ -98,6 +88,7 @@ let rec sets_of_list l =
(* The exploration is probably not complete - for simple cases, it works... *)
let real_nonlinear_prover d l =
+ let l = List.map (fun (e,op) -> (Mc.denorm e,op)) l in
try
let (eq,ge,neq) = partition_expr l in
@@ -151,6 +142,8 @@ let real_nonlinear_prover d l =
(* This is somewhat buggy, over Z, strict inequality vanish... *)
let pure_sos l =
+ let l = List.map (fun (e,o) -> Mc.denorm e, o) l in
+
(* If there is no strict inequality,
I should nonetheless be able to try something - over Z > is equivalent to -1 >= *)
try
@@ -172,26 +165,26 @@ let pure_sos l =
| x -> None
-type micromega_polys = (Micromega.q Mc.pExpr * Mc.op1) list
+type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
type csdp_certificate = Sos.positivstellensatz option
type provername = string * int option
-let main () =
- if Array.length Sys.argv <> 3 then
- (Printf.printf "Usage: csdpcert inputfile outputfile\n"; exit 1);
- let input_file = Sys.argv.(1) in
- let output_file = Sys.argv.(2) in
- let inch = open_in input_file in
- let (prover,poly) = (input_value inch : provername * micromega_polys) in
- close_in inch;
- let cert =
+
+let run_prover prover pb =
match prover with
- | "real_nonlinear_prover", Some d -> real_nonlinear_prover d poly
- | "pure_sos", None -> pure_sos poly
- | prover, _ -> (Printf.printf "unknown prover: %s\n" prover; exit 1) in
- let outch = open_out output_file in
- output_value outch (cert:csdp_certificate);
- close_out outch;
+ | "real_nonlinear_prover", Some d -> real_nonlinear_prover d pb
+ | "pure_sos", None -> pure_sos pb
+ | prover, _ -> (Printf.printf "unknown prover: %s\n" prover; exit 1)
+
+
+let main () =
+ let (prover,poly) = (input_value stdin : provername * micromega_polys) in
+ let cert = run_prover prover poly in
+ output_value stdout (cert:csdp_certificate);
exit 0;;
let _ = main () in ()
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 23ae3bd0e..f4d04e5d4 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -31,6 +31,11 @@ TACTIC EXTEND PsatzZ
| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ]
END
+TACTIC EXTEND ZOmicron
+[ "xlia" ] -> [ Coq_micromega.xlia]
+END
+
+
TACTIC EXTEND Sos_Z
| [ "sos_Z" ] -> [ Coq_micromega.sos_Z]
END
@@ -53,9 +58,6 @@ TACTIC EXTEND QOmicron
END
-TACTIC EXTEND ZOmicron
-[ "xlia" ] -> [ Coq_micromega.xlia]
-END
TACTIC EXTEND ROmicron
[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R]
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index c2eb572c9..c547b3d4a 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -831,8 +831,6 @@ struct
end
open EstimateElimEq
-
-
module Fourier =
struct
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index db339ff0d..d884f2659 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1,6 +1,3 @@
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
(** val negb : bool -> bool **)
let negb = function
@@ -23,6 +20,13 @@ let compOpp = function
| Lt -> Gt
| Gt -> Lt
+(** val plus : nat -> nat -> nat **)
+
+let rec plus n0 m =
+ match n0 with
+ | O -> m
+ | S p -> S (plus p m)
+
(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
let rec app l m =
@@ -205,6 +209,13 @@ let rec pcompare x y r =
| XH -> r
| _ -> Lt)
+(** val psize : positive -> nat **)
+
+let rec psize = function
+ | XI p2 -> S (psize p2)
+ | XO p2 -> S (psize p2)
+ | XH -> S O
+
type n =
| N0
| Npos of positive
@@ -323,25 +334,19 @@ let zcompare x y =
| Zneg y' -> compOpp (pcompare x' y' Eq)
| _ -> Lt)
-(** val dcompare_inf : comparison -> bool option **)
-
-let dcompare_inf = function
- | Eq -> Some true
- | Lt -> Some false
- | Gt -> None
+(** val zabs : z -> z **)
-(** val zcompare_rec :
- z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
-
-let zcompare_rec x y h1 h2 h3 =
- match dcompare_inf (zcompare x y) with
- | Some x0 -> if x0 then h1 __ else h2 __
- | None -> h3 __
+let zabs = function
+ | Z0 -> Z0
+ | Zpos p -> Zpos p
+ | Zneg p -> Zpos p
(** val z_gt_dec : z -> z -> bool **)
let z_gt_dec x y =
- zcompare_rec x y (fun _ -> false) (fun _ -> false) (fun _ -> true)
+ match zcompare x y with
+ | Gt -> true
+ | _ -> false
(** val zle_bool : z -> z -> bool **)
@@ -421,6 +426,11 @@ let zdiv_eucl a b =
| Zneg b' ->
let q0 , r = zdiv_eucl_POS a' (Zpos b') in q0 , (zopp r))
+(** val zdiv : z -> z -> z **)
+
+let zdiv a b =
+ let q0 , x = zdiv_eucl a b in q0
+
type 'c pol =
| Pc of 'c
| Pinj of positive * 'c pol
@@ -800,6 +810,25 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with
pmul cO cI cadd cmul ceqb x x0) q' XH p2) i
(pmul cO cI cadd cmul ceqb q0 q')))
+(** val psquare :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> bool) -> 'a1 pol -> 'a1 pol **)
+
+let rec psquare cO cI cadd cmul ceqb = function
+ | Pc c -> Pc (cmul c c)
+ | Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0))
+ | PX (p2, i, q0) ->
+ mkPX cO ceqb
+ (padd cO cadd ceqb
+ (mkPX cO ceqb (psquare cO cI cadd cmul ceqb p2) i (p0 cO))
+ (pmul cO cI cadd cmul ceqb p2
+ (let p3 = pmulC cO cI cmul ceqb q0 (cadd cI cI) in
+ match p3 with
+ | Pc c -> p3
+ | Pinj (j', q1) -> Pinj ((pplus XH j'), q1)
+ | PX (p4, p5, p6) -> Pinj (XH, p3)))) i
+ (psquare cO cI cadd cmul ceqb q0)
+
type 'c pExpr =
| PEc of 'c
| PEX of positive
@@ -961,8 +990,6 @@ let rec cnf_checker checker f l =
let tauto_checker normalise0 negate0 checker f w =
cnf_checker checker (xcnf normalise0 negate0 true f) w
-type 'c pExprC = 'c pExpr
-
type 'c polC = 'c pol
type op1 =
@@ -971,119 +998,137 @@ type op1 =
| Strict
| NonStrict
-type 'c nFormula = 'c pExprC * op1
-
-type monoidMember = nat list
-
-type 'c coneMember =
- | S_In of nat
- | S_Ideal of 'c pExprC * 'c coneMember
- | S_Square of 'c pExprC
- | S_Monoid of monoidMember
- | S_Mult of 'c coneMember * 'c coneMember
- | S_Add of 'c coneMember * 'c coneMember
- | S_Pos of 'c
- | S_Z
-
-(** val nformula_times : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula **)
-
-let nformula_times f f' =
- let p , op = f in
- let p' , op' = f' in
- (PEmul (p, p')) ,
- (match op with
- | Equal -> Equal
- | NonEqual -> NonEqual
- | Strict -> op'
- | NonStrict -> NonStrict)
-
-(** val nformula_plus : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula **)
-
-let nformula_plus f f' =
- let p , op = f in
- let p' , op' = f' in
- (PEadd (p, p')) ,
- (match op with
- | Equal -> op'
- | NonEqual -> NonEqual
- | Strict -> Strict
- | NonStrict -> (match op' with
- | Strict -> Strict
- | _ -> NonStrict))
-
-(** val eval_monoid :
- 'a1 -> 'a1 nFormula list -> monoidMember -> 'a1 pExprC **)
-
-let rec eval_monoid cI l = function
- | [] -> PEc cI
- | n0 :: ns0 -> PEmul
- ((let q0 , o = nth n0 l ((PEc cI) , NonEqual) in
- (match o with
- | NonEqual -> q0
- | _ -> PEc cI)), (eval_monoid cI l ns0))
-
-(** val eval_cone :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
- nFormula list -> 'a1 coneMember -> 'a1 nFormula **)
-
-let rec eval_cone cO cI ceqb cleb l = function
- | S_In n0 ->
- let f = nth n0 l ((PEc cO) , Equal) in
- let p , o = f in
+type 'c nFormula = 'c polC * op1
+
+(** val opAdd : op1 -> op1 -> op1 option **)
+
+let opAdd o o' =
+ match o with
+ | Equal -> Some o'
+ | NonEqual -> (match o' with
+ | Equal -> Some NonEqual
+ | _ -> None)
+ | Strict -> (match o' with
+ | NonEqual -> None
+ | _ -> Some Strict)
+ | NonStrict ->
+ (match o' with
+ | NonEqual -> None
+ | Strict -> Some Strict
+ | _ -> Some NonStrict)
+
+type 'c psatz =
+ | PsatzIn of nat
+ | PsatzSquare of 'c polC
+ | PsatzMulC of 'c polC * 'c psatz
+ | PsatzMulE of 'c psatz * 'c psatz
+ | PsatzAdd of 'c psatz * 'c psatz
+ | PsatzC of 'c
+ | PsatzZ
+
+(** val pexpr_times_nformula :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **)
+
+let pexpr_times_nformula cO cI cplus ctimes ceqb e = function
+ | ef , o ->
(match o with
- | NonEqual -> (PEc cO) , Equal
- | _ -> f)
- | S_Ideal (p, cm') ->
- let f = eval_cone cO cI ceqb cleb l cm' in
- let q0 , op = f in
- (match op with
- | Equal -> (PEmul (q0, p)) , Equal
- | _ -> f)
- | S_Square p -> (PEmul (p, p)) , NonStrict
- | S_Monoid m -> let p = eval_monoid cI l m in (PEmul (p, p)) , Strict
- | S_Mult (p, q0) ->
- nformula_times (eval_cone cO cI ceqb cleb l p)
- (eval_cone cO cI ceqb cleb l q0)
- | S_Add (p, q0) ->
- nformula_plus (eval_cone cO cI ceqb cleb l p)
- (eval_cone cO cI ceqb cleb l q0)
- | S_Pos c ->
- if (&&) (cleb cO c) (negb (ceqb cO c))
- then (PEc c) , Strict
- else (PEc cO) , Equal
- | S_Z -> (PEc cO) , Equal
+ | Equal -> Some ((pmul cO cI cplus ctimes ceqb e ef) , Equal)
+ | _ -> None)
-(** val normalise_pexpr :
+(** val nformula_times_nformula :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
- -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 polC **)
-
-let normalise_pexpr cO cI cplus ctimes cminus copp ceqb x =
- norm_aux cO cI cplus ctimes cminus copp ceqb x
+ -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **)
+
+let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 =
+ let e1 , o1 = f1 in
+ let e2 , o2 = f2 in
+ (match o1 with
+ | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal)
+ | NonEqual ->
+ (match o2 with
+ | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal)
+ | NonEqual -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) ,
+ NonEqual)
+ | _ -> None)
+ | Strict ->
+ (match o2 with
+ | NonEqual -> None
+ | _ -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , o2))
+ | NonStrict ->
+ (match o2 with
+ | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal)
+ | NonEqual -> None
+ | _ -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , NonStrict)))
+
+(** val nformula_plus_nformula :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1
+ nFormula -> 'a1 nFormula option **)
+
+let nformula_plus_nformula cO cplus ceqb f1 f2 =
+ let e1 , o1 = f1 in
+ let e2 , o2 = f2 in
+ (match opAdd o1 o2 with
+ | Some x -> Some ((padd cO cplus ceqb e1 e2) , x)
+ | None -> None)
+
+(** val eval_Psatz :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
+ nFormula option **)
+
+let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function
+ | PsatzIn n0 -> Some (nth n0 l ((Pc cO) , Equal))
+ | PsatzSquare e0 -> Some ((psquare cO cI cplus ctimes ceqb e0) , NonStrict)
+ | PsatzMulC (re, e0) ->
+ (match eval_Psatz cO cI cplus ctimes ceqb cleb l e0 with
+ | Some x -> pexpr_times_nformula cO cI cplus ctimes ceqb re x
+ | None -> None)
+ | PsatzMulE (f1, f2) ->
+ (match eval_Psatz cO cI cplus ctimes ceqb cleb l f1 with
+ | Some x ->
+ (match eval_Psatz cO cI cplus ctimes ceqb cleb l f2 with
+ | Some x' ->
+ nformula_times_nformula cO cI cplus ctimes ceqb x x'
+ | None -> None)
+ | None -> None)
+ | PsatzAdd (f1, f2) ->
+ (match eval_Psatz cO cI cplus ctimes ceqb cleb l f1 with
+ | Some x ->
+ (match eval_Psatz cO cI cplus ctimes ceqb cleb l f2 with
+ | Some x' -> nformula_plus_nformula cO cplus ceqb x x'
+ | None -> None)
+ | None -> None)
+ | PsatzC c ->
+ if (&&) (cleb cO c) (negb (ceqb cO c))
+ then Some ((Pc c) , Strict)
+ else None
+ | PsatzZ -> Some ((Pc cO) , Equal)
(** val check_inconsistent :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
- -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool)
- -> 'a1 nFormula -> bool **)
+ 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula ->
+ bool **)
-let check_inconsistent cO cI cplus ctimes cminus copp ceqb cleb = function
+let check_inconsistent cO ceqb cleb = function
| e , op ->
- (match normalise_pexpr cO cI cplus ctimes cminus copp ceqb e with
+ (match e with
| Pc c ->
(match op with
| Equal -> negb (ceqb c cO)
- | NonEqual -> false
+ | NonEqual -> ceqb c cO
| Strict -> cleb c cO
| NonStrict -> (&&) (cleb c cO) (negb (ceqb c cO)))
| _ -> false)
(** val check_normalised_formulas :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
- -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool)
- -> 'a1 nFormula list -> 'a1 coneMember -> bool **)
+ -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz ->
+ bool **)
-let check_normalised_formulas cO cI cplus ctimes cminus copp ceqb cleb l cm =
- check_inconsistent cO cI cplus ctimes cminus copp ceqb cleb
- (eval_cone cO cI ceqb cleb l cm)
+let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm =
+ match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with
+ | Some f -> check_inconsistent cO ceqb cleb f
+ | None -> false
type op2 =
| OpEq
@@ -1093,9 +1138,9 @@ type op2 =
| OpLt
| OpGt
-type 'c formula = { flhs : 'c pExprC; fop : op2; frhs : 'c pExprC }
+type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr }
-(** val flhs : 'a1 formula -> 'a1 pExprC **)
+(** val flhs : 'a1 formula -> 'a1 pExpr **)
let flhs x = x.flhs
@@ -1103,120 +1148,164 @@ let flhs x = x.flhs
let fop x = x.fop
-(** val frhs : 'a1 formula -> 'a1 pExprC **)
+(** val frhs : 'a1 formula -> 'a1 pExpr **)
let frhs x = x.frhs
-(** val xnormalise : 'a1 formula -> 'a1 nFormula list **)
+(** val norm :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
+
+let norm cO cI cplus ctimes cminus copp ceqb pe =
+ norm_aux cO cI cplus ctimes cminus copp ceqb pe
+
+(** val psub0 :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
+ -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
+
+let psub0 cO cplus cminus copp ceqb p p' =
+ psub cO cplus cminus copp ceqb p p'
+
+(** val padd0 :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
+ -> 'a1 pol **)
+
+let padd0 cO cplus ceqb p p' =
+ padd cO cplus ceqb p p'
+
+(** val xnormalise :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+ nFormula list **)
-let xnormalise t0 =
+let xnormalise cO cI cplus ctimes cminus copp ceqb t0 =
let { flhs = lhs; fop = o; frhs = rhs } = t0 in
+ let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in
+ let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in
(match o with
- | OpEq -> ((PEsub (lhs, rhs)) , Strict) :: (((PEsub (rhs, lhs)) ,
- Strict) :: [])
- | OpNEq -> ((PEsub (lhs, rhs)) , Equal) :: []
- | OpLe -> ((PEsub (lhs, rhs)) , Strict) :: []
- | OpGe -> ((PEsub (rhs, lhs)) , Strict) :: []
- | OpLt -> ((PEsub (lhs, rhs)) , NonStrict) :: []
- | OpGt -> ((PEsub (rhs, lhs)) , NonStrict) :: [])
+ | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) ::
+ (((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: [])
+ | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Equal) :: []
+ | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: []
+ | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: []
+ | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , NonStrict) ::
+ []
+ | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , NonStrict) ::
+ [])
-(** val cnf_normalise : 'a1 formula -> 'a1 nFormula cnf **)
+(** val cnf_normalise :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+ nFormula cnf **)
-let cnf_normalise t0 =
- map (fun x -> x :: []) (xnormalise t0)
+let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 =
+ map (fun x -> x :: []) (xnormalise cO cI cplus ctimes cminus copp ceqb t0)
-(** val xnegate : 'a1 formula -> 'a1 nFormula list **)
+(** val xnegate :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+ nFormula list **)
-let xnegate t0 =
+let xnegate cO cI cplus ctimes cminus copp ceqb t0 =
let { flhs = lhs; fop = o; frhs = rhs } = t0 in
+ let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in
+ let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in
(match o with
- | OpEq -> ((PEsub (lhs, rhs)) , Equal) :: []
- | OpNEq -> ((PEsub (lhs, rhs)) , Strict) :: (((PEsub (rhs, lhs)) ,
- Strict) :: [])
- | OpLe -> ((PEsub (rhs, lhs)) , NonStrict) :: []
- | OpGe -> ((PEsub (lhs, rhs)) , NonStrict) :: []
- | OpLt -> ((PEsub (rhs, lhs)) , Strict) :: []
- | OpGt -> ((PEsub (lhs, rhs)) , Strict) :: [])
-
-(** val cnf_negate : 'a1 formula -> 'a1 nFormula cnf **)
-
-let cnf_negate t0 =
- map (fun x -> x :: []) (xnegate t0)
-
-(** val simpl_expr :
- 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 pExprC **)
-
-let rec simpl_expr cI ceqb e = match e with
- | PEadd (x, y) -> PEadd ((simpl_expr cI ceqb x), (simpl_expr cI ceqb y))
- | PEmul (y, z0) ->
- let y' = simpl_expr cI ceqb y in
- (match y' with
- | PEc c ->
- if ceqb c cI
- then simpl_expr cI ceqb z0
- else PEmul (y', (simpl_expr cI ceqb z0))
- | _ -> PEmul (y', (simpl_expr cI ceqb z0)))
- | _ -> e
+ | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Equal) :: []
+ | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) ::
+ (((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: [])
+ | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , NonStrict) ::
+ []
+ | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , NonStrict) ::
+ []
+ | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: []
+ | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: [])
+
+(** val cnf_negate :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
+ -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1
+ nFormula cnf **)
+
+let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 =
+ map (fun x -> x :: []) (xnegate cO cI cplus ctimes cminus copp ceqb t0)
+
+(** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **)
+
+let rec xdenorm jmp = function
+ | Pc c -> PEc c
+ | Pinj (j, p2) -> xdenorm (pplus j jmp) p2
+ | PX (p2, j, q0) -> PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp),
+ (Npos j))))), (xdenorm (psucc jmp) q0))
+
+(** val denorm : 'a1 pol -> 'a1 pExpr **)
+
+let denorm p =
+ xdenorm XH p
(** val simpl_cone :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1
- coneMember -> 'a1 coneMember **)
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz ->
+ 'a1 psatz **)
let simpl_cone cO cI ctimes ceqb e = match e with
- | S_Square t0 ->
- let x = simpl_expr cI ceqb t0 in
- (match x with
- | PEc c -> if ceqb cO c then S_Z else S_Pos (ctimes c c)
- | _ -> S_Square x)
- | S_Mult (t1, t2) ->
+ | PsatzSquare t0 ->
+ (match t0 with
+ | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
+ | _ -> PsatzSquare t0)
+ | PsatzMulE (t1, t2) ->
(match t1 with
- | S_Mult (x, x0) ->
+ | PsatzMulE (x, x0) ->
(match x with
- | S_Pos p2 ->
+ | PsatzC p2 ->
(match t2 with
- | S_Pos c -> S_Mult ((S_Pos (ctimes c p2)), x0)
- | S_Z -> S_Z
+ | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x0)
+ | PsatzZ -> PsatzZ
| _ -> e)
| _ ->
(match x0 with
- | S_Pos p2 ->
+ | PsatzC p2 ->
(match t2 with
- | S_Pos c -> S_Mult ((S_Pos (ctimes c p2)), x)
- | S_Z -> S_Z
+ | PsatzC c -> PsatzMulE ((PsatzC
+ (ctimes c p2)), x)
+ | PsatzZ -> PsatzZ
| _ -> e)
| _ ->
(match t2 with
- | S_Pos c ->
- if ceqb cI c then t1 else S_Mult (t1, t2)
- | S_Z -> S_Z
+ | PsatzC c ->
+ if ceqb cI c
+ then t1
+ else PsatzMulE (t1, t2)
+ | PsatzZ -> PsatzZ
| _ -> e)))
- | S_Pos c ->
+ | PsatzC c ->
(match t2 with
- | S_Mult (x, x0) ->
+ | PsatzMulE (x, x0) ->
(match x with
- | S_Pos p2 -> S_Mult ((S_Pos (ctimes c p2)), x0)
+ | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x0)
| _ ->
(match x0 with
- | S_Pos p2 -> S_Mult ((S_Pos (ctimes c p2)), x)
+ | PsatzC p2 -> PsatzMulE ((PsatzC
+ (ctimes c p2)), x)
| _ ->
- if ceqb cI c then t2 else S_Mult (t1, t2)))
- | S_Add (y, z0) -> S_Add ((S_Mult ((S_Pos c), y)), (S_Mult
- ((S_Pos c), z0)))
- | S_Pos c0 -> S_Pos (ctimes c c0)
- | S_Z -> S_Z
- | _ -> if ceqb cI c then t2 else S_Mult (t1, t2))
- | S_Z -> S_Z
+ if ceqb cI c
+ then t2
+ else PsatzMulE (t1, t2)))
+ | PsatzAdd (y, z0) -> PsatzAdd ((PsatzMulE ((PsatzC c), y)),
+ (PsatzMulE ((PsatzC c), z0)))
+ | PsatzC c0 -> PsatzC (ctimes c c0)
+ | PsatzZ -> PsatzZ
+ | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))
+ | PsatzZ -> PsatzZ
| _ ->
(match t2 with
- | S_Pos c -> if ceqb cI c then t1 else S_Mult (t1, t2)
- | S_Z -> S_Z
+ | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2)
+ | PsatzZ -> PsatzZ
| _ -> e))
- | S_Add (t1, t2) ->
+ | PsatzAdd (t1, t2) ->
(match t1 with
- | S_Z -> t2
+ | PsatzZ -> t2
| _ -> (match t2 with
- | S_Z -> t1
- | _ -> S_Add (t1, t2)))
+ | PsatzZ -> t1
+ | _ -> PsatzAdd (t1, t2)))
| _ -> e
type q = { qnum : z; qden : positive }
@@ -1260,6 +1349,50 @@ let qopp x =
let qminus x y =
qplus x (qopp y)
+(** val pgcdn : nat -> positive -> positive -> positive **)
+
+let rec pgcdn n0 a b =
+ match n0 with
+ | O -> XH
+ | S n1 ->
+ (match a with
+ | XI a' ->
+ (match b with
+ | XI b' ->
+ (match pcompare a' b' Eq with
+ | Eq -> a
+ | Lt -> pgcdn n1 (pminus b' a') a
+ | Gt -> pgcdn n1 (pminus a' b') b)
+ | XO b0 -> pgcdn n1 a b0
+ | XH -> XH)
+ | XO a0 ->
+ (match b with
+ | XI p -> pgcdn n1 a0 b
+ | XO b0 -> XO (pgcdn n1 a0 b0)
+ | XH -> XH)
+ | XH -> XH)
+
+(** val pgcd : positive -> positive -> positive **)
+
+let pgcd a b =
+ pgcdn (plus (psize a) (psize b)) a b
+
+(** val zgcd : z -> z -> z **)
+
+let zgcd a b =
+ match a with
+ | Z0 -> zabs b
+ | Zpos a0 ->
+ (match b with
+ | Z0 -> zabs a
+ | Zpos b0 -> Zpos (pgcd a0 b0)
+ | Zneg b0 -> Zpos (pgcd a0 b0))
+ | Zneg a0 ->
+ (match b with
+ | Z0 -> zabs a
+ | Zpos b0 -> Zpos (pgcd a0 b0)
+ | Zneg b0 -> Zpos (pgcd a0 b0))
+
type 'a t =
| Empty
| Leaf of 'a
@@ -1277,28 +1410,42 @@ let rec find default vm p =
| XO p2 -> find default l p2
| XH -> e)
-type zWitness = z coneMember
+type zWitness = z psatz
-(** val zWeakChecker : z nFormula list -> z coneMember -> bool **)
+(** val zWeakChecker : z nFormula list -> z psatz -> bool **)
let zWeakChecker x x0 =
- check_normalised_formulas Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool
- zle_bool x x0
+ check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0
+
+(** val psub1 : z pol -> z pol -> z pol **)
+
+let psub1 p p' =
+ psub0 Z0 zplus zminus zopp zeq_bool p p'
+
+(** val padd1 : z pol -> z pol -> z pol **)
+
+let padd1 p p' =
+ padd0 Z0 zplus zeq_bool p p'
+
+(** val norm0 : z pExpr -> z pol **)
+
+let norm0 pe =
+ norm Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool pe
(** val xnormalise0 : z formula -> z nFormula list **)
let xnormalise0 t0 =
let { flhs = lhs; fop = o; frhs = rhs } = t0 in
+ let lhs0 = norm0 lhs in
+ let rhs0 = norm0 rhs in
(match o with
- | OpEq -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
- (((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) :: [])
- | OpNEq -> ((PEsub (lhs, rhs)) , Equal) :: []
- | OpLe -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
- []
- | OpGe -> ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
- []
- | OpLt -> ((PEsub (lhs, rhs)) , NonStrict) :: []
- | OpGt -> ((PEsub (rhs, lhs)) , NonStrict) :: [])
+ | OpEq -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) ::
+ (((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: [])
+ | OpNEq -> ((psub1 lhs0 rhs0) , Equal) :: []
+ | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: []
+ | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: []
+ | OpLt -> ((psub1 lhs0 rhs0) , NonStrict) :: []
+ | OpGt -> ((psub1 rhs0 lhs0) , NonStrict) :: [])
(** val normalise : z formula -> z nFormula cnf **)
@@ -1309,17 +1456,16 @@ let normalise t0 =
let xnegate0 t0 =
let { flhs = lhs; fop = o; frhs = rhs } = t0 in
+ let lhs0 = norm0 lhs in
+ let rhs0 = norm0 rhs in
(match o with
- | OpEq -> ((PEsub (lhs, rhs)) , Equal) :: []
- | OpNEq -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict)
- :: (((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
- [])
- | OpLe -> ((PEsub (rhs, lhs)) , NonStrict) :: []
- | OpGe -> ((PEsub (lhs, rhs)) , NonStrict) :: []
- | OpLt -> ((PEsub (rhs, (PEadd (lhs, (PEc (Zpos XH)))))) , NonStrict) ::
- []
- | OpGt -> ((PEsub (lhs, (PEadd (rhs, (PEc (Zpos XH)))))) , NonStrict) ::
- [])
+ | OpEq -> ((psub1 lhs0 rhs0) , Equal) :: []
+ | OpNEq -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) ::
+ (((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: [])
+ | OpLe -> ((psub1 rhs0 lhs0) , NonStrict) :: []
+ | OpGe -> ((psub1 lhs0 rhs0) , NonStrict) :: []
+ | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: []
+ | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: [])
(** val negate : z formula -> z nFormula cnf **)
@@ -1334,106 +1480,206 @@ let ceiling a b =
| Z0 -> q0
| _ -> zplus q0 (Zpos XH))
-type proofTerm =
- | RatProof of zWitness
- | CutProof of z pExprC * q * zWitness * proofTerm
- | EnumProof of q * z pExprC * q * zWitness * zWitness * proofTerm list
+type zArithProof =
+ | DoneProof
+ | RatProof of zWitness * zArithProof
+ | CutProof of zWitness * zArithProof
+ | EnumProof of zWitness * zWitness * zArithProof list
-(** val makeLb : z pExpr -> q -> z nFormula **)
+(** val isZ0 : z -> bool **)
-let makeLb v q0 =
- let { qnum = n0; qden = d } = q0 in
- (PEsub ((PEmul ((PEc (Zpos d)), v)), (PEc n0))) , NonStrict
+let isZ0 = function
+ | Z0 -> true
+ | _ -> false
-(** val qceiling : q -> z **)
+(** val zgcd_pol : z polC -> z * z **)
-let qceiling q0 =
- let { qnum = n0; qden = d } = q0 in ceiling n0 (Zpos d)
+let rec zgcd_pol = function
+ | Pc c -> Z0 , c
+ | Pinj (p2, p3) -> zgcd_pol p3
+ | PX (p2, p3, q0) ->
+ let g1 , c1 = zgcd_pol p2 in
+ let g2 , c2 = zgcd_pol q0 in
+ if isZ0 g1
+ then Z0 , c2
+ else if isZ0 (zgcd g1 c1)
+ then Z0 , c2
+ else if isZ0 g2 then Z0 , c2 else (zgcd (zgcd g1 c1) g2) , c2
-(** val makeLbCut : z pExprC -> q -> z nFormula **)
+(** val zdiv_pol : z polC -> z -> z polC **)
-let makeLbCut v q0 =
- (PEsub (v, (PEc (qceiling q0)))) , NonStrict
+let rec zdiv_pol p x =
+ match p with
+ | Pc c -> Pc (zdiv c x)
+ | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x))
+ | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x))
+
+(** val makeCuttingPlane : z polC -> z polC * z **)
+
+let makeCuttingPlane p =
+ let g , c = zgcd_pol p in
+ if zgt_bool g Z0
+ then (zdiv_pol (psubC zminus p c) g) , (zopp (ceiling (zopp c) g))
+ else p , Z0
-(** val neg_nformula : z nFormula -> z pExpr * op1 **)
+(** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **)
+
+let genCuttingPlane = function
+ | e , op ->
+ (match op with
+ | Equal ->
+ let g , c = zgcd_pol e in
+ if (&&) (zgt_bool g Z0)
+ ((&&) (zgt_bool c Z0) (negb (zeq_bool (zgcd g c) g)))
+ then None
+ else Some ((e , Z0) , op)
+ | NonEqual -> Some ((e , Z0) , op)
+ | Strict ->
+ let p , c = makeCuttingPlane (psubC zminus e (Zpos XH)) in
+ Some ((p , c) , NonStrict)
+ | NonStrict ->
+ let p , c = makeCuttingPlane e in Some ((p , c) , NonStrict))
-let neg_nformula = function
- | e , o -> (PEopp (PEadd (e, (PEc (Zpos XH))))) , o
+(** val nformula_of_cutting_plane :
+ ((z polC * z) * op1) -> z nFormula **)
-(** val cutChecker :
- z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option **)
+let nformula_of_cutting_plane = function
+ | e_z , o -> let e , z0 = e_z in (padd1 e (Pc z0)) , o
-let cutChecker l e lb pf =
- if zWeakChecker ((neg_nformula (makeLb e lb)) :: l) pf
- then Some (makeLbCut e lb)
- else None
+(** val is_pol_Z0 : z polC -> bool **)
-(** val zChecker : z nFormula list -> proofTerm -> bool **)
+let is_pol_Z0 = function
+ | Pc z0 -> (match z0 with
+ | Z0 -> true
+ | _ -> false)
+ | _ -> false
+
+(** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **)
+
+let eval_Psatz0 x x0 =
+ eval_Psatz Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0
+
+(** val check_inconsistent0 : z nFormula -> bool **)
+
+let check_inconsistent0 f =
+ check_inconsistent Z0 zeq_bool zle_bool f
+
+(** val zChecker : z nFormula list -> zArithProof -> bool **)
let rec zChecker l = function
- | RatProof pf0 -> zWeakChecker l pf0
- | CutProof (e, q0, pf0, rst) ->
- (match cutChecker l e q0 pf0 with
- | Some c -> zChecker (c :: l) rst
+ | DoneProof -> false
+ | RatProof (w, pf0) ->
+ (match eval_Psatz0 l w with
+ | Some f ->
+ if check_inconsistent0 f then true else zChecker (f :: l) pf0
+ | None -> false)
+ | CutProof (w, pf0) ->
+ (match eval_Psatz0 l w with
+ | Some f ->
+ (match genCuttingPlane f with
+ | Some cp ->
+ zChecker ((nformula_of_cutting_plane cp) :: l) pf0
+ | None -> true)
| None -> false)
- | EnumProof (lb, e, ub, pf1, pf2, rst) ->
- (match cutChecker l e lb pf1 with
- | Some n0 ->
- (match cutChecker l (PEopp e) (qopp ub) pf2 with
- | Some n1 ->
- let rec label pfs lb0 ub0 =
- match pfs with
- | [] -> if z_gt_dec lb0 ub0 then true else false
- | pf0 :: rsr ->
- (&&)
- (zChecker (((PEsub (e, (PEc lb0))) , Equal) ::
- l) pf0) (label rsr (zplus lb0 (Zpos XH)) ub0)
- in label rst (qceiling lb) (zopp (qceiling (qopp ub)))
+ | EnumProof (w1, w2, pf0) ->
+ (match eval_Psatz0 l w1 with
+ | Some f1 ->
+ (match eval_Psatz0 l w2 with
+ | Some f2 ->
+ (match genCuttingPlane f1 with
+ | Some p ->
+ let p2 , op3 = p in
+ let e1 , z1 = p2 in
+ (match genCuttingPlane f2 with
+ | Some p3 ->
+ let p4 , op4 = p3 in
+ let e2 , z2 = p4 in
+ (match op3 with
+ | NonStrict ->
+ (match op4 with
+ | NonStrict ->
+ if is_pol_Z0 (padd1 e1 e2)
+ then
+ let rec label pfs lb ub =
+
+ match pfs with
+ |
+ [] ->
+ if z_gt_dec lb ub
+ then true
+ else false
+ |
+ pf1 :: rsr ->
+ (&&)
+ (zChecker
+ (((psub1 e1 (Pc lb)) ,
+ Equal) :: l) pf1)
+ (label rsr
+ (zplus lb (Zpos XH)) ub)
+ in label pf0 (zopp z1) z2
+ else false
+ | _ -> false)
+ | _ -> false)
+ | None -> false)
+ | None -> false)
| None -> false)
| None -> false)
-(** val zTautoChecker : z formula bFormula -> proofTerm list -> bool **)
+(** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **)
let zTautoChecker f w =
tauto_checker normalise negate zChecker f w
-(** val map_cone : (nat -> nat) -> zWitness -> zWitness **)
-
-let rec map_cone f e = match e with
- | S_In n0 -> S_In (f n0)
- | S_Ideal (e0, cm) -> S_Ideal (e0, (map_cone f cm))
- | S_Monoid l -> S_Monoid (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
-
-(** val indexes : zWitness -> nat list **)
-
-let rec indexes = function
- | S_In n0 -> n0 :: []
- | S_Ideal (e0, cm) -> indexes cm
- | S_Monoid l -> l
- | S_Mult (cm1, cm2) -> app (indexes cm1) (indexes cm2)
- | S_Add (cm1, cm2) -> app (indexes cm1) (indexes cm2)
- | _ -> []
-
(** val n_of_Z : z -> n **)
let n_of_Z = function
| Zpos p -> Npos p
| _ -> N0
-type qWitness = q coneMember
+type qWitness = q psatz
-(** val qWeakChecker : q nFormula list -> q coneMember -> bool **)
+(** val qWeakChecker : q nFormula list -> q psatz -> bool **)
let qWeakChecker x x0 =
check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH);
- qden = XH } qplus qmult qminus qopp qeq_bool qle_bool x x0
+ qden = XH } qplus qmult qeq_bool qle_bool x x0
+
+(** val qnormalise : q formula -> q nFormula cnf **)
+
+let qnormalise t0 =
+ cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
+ qplus qmult qminus qopp qeq_bool t0
+
+(** val qnegate : q formula -> q nFormula cnf **)
+
+let qnegate t0 =
+ cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus
+ qmult qminus qopp qeq_bool t0
(** val qTautoChecker : q formula bFormula -> qWitness list -> bool **)
let qTautoChecker f w =
- tauto_checker (fun x -> cnf_normalise x) (fun x ->
- cnf_negate x) qWeakChecker f w
+ tauto_checker qnormalise qnegate qWeakChecker f w
+
+type rWitness = z psatz
+
+(** val rWeakChecker : z nFormula list -> z psatz -> bool **)
+
+let rWeakChecker x x0 =
+ check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0
+
+(** val rnormalise : z formula -> z nFormula cnf **)
+
+let rnormalise t0 =
+ cnf_normalise Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool t0
+
+(** val rnegate : z formula -> z nFormula cnf **)
+
+let rnegate t0 =
+ cnf_negate Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool t0
+
+(** val rTautoChecker : z formula bFormula -> rWitness list -> bool **)
+
+let rTautoChecker f w =
+ tauto_checker rnormalise rnegate rWeakChecker f w
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 948391466..34f61904a 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,5 +1,3 @@
-type __ = Obj.t
-
val negb : bool -> bool
type nat =
@@ -13,6 +11,8 @@ type comparison =
val compOpp : comparison -> comparison
+val plus : nat -> nat -> nat
+
val app : 'a1 list -> 'a1 list -> 'a1 list
val nth : nat -> 'a1 list -> 'a1 -> 'a1
@@ -55,6 +55,8 @@ val pmult : positive -> positive -> positive
val pcompare : positive -> positive -> comparison -> comparison
+val psize : positive -> nat
+
type n =
| N0
| Npos of positive
@@ -82,9 +84,7 @@ val zmult : z -> z -> z
val zcompare : z -> z -> comparison
-val dcompare_inf : comparison -> bool option
-
-val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
+val zabs : z -> z
val z_gt_dec : z -> z -> bool
@@ -102,6 +102,8 @@ val zdiv_eucl_POS : positive -> z -> z * z
val zdiv_eucl : z -> z -> z * z
+val zdiv : z -> z -> z
+
type 'c pol =
| Pc of 'c
| Pinj of positive * 'c pol
@@ -168,6 +170,10 @@ val pmul :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
+val psquare :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ bool) -> 'a1 pol -> 'a1 pol
+
type 'c pExpr =
| PEc of 'c
| PEX of positive
@@ -224,8 +230,6 @@ val tauto_checker :
('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
bFormula -> 'a3 list -> bool
-type 'c pExprC = 'c pExpr
-
type 'c polC = 'c pol
type op1 =
@@ -234,43 +238,42 @@ type op1 =
| Strict
| NonStrict
-type 'c nFormula = 'c pExprC * op1
-
-type monoidMember = nat list
+type 'c nFormula = 'c polC * op1
-type 'c coneMember =
- | S_In of nat
- | S_Ideal of 'c pExprC * 'c coneMember
- | S_Square of 'c pExprC
- | S_Monoid of monoidMember
- | S_Mult of 'c coneMember * 'c coneMember
- | S_Add of 'c coneMember * 'c coneMember
- | S_Pos of 'c
- | S_Z
+val opAdd : op1 -> op1 -> op1 option
-val nformula_times : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
+type 'c psatz =
+ | PsatzIn of nat
+ | PsatzSquare of 'c polC
+ | PsatzMulC of 'c polC * 'c psatz
+ | PsatzMulE of 'c psatz * 'c psatz
+ | PsatzAdd of 'c psatz * 'c psatz
+ | PsatzC of 'c
+ | PsatzZ
-val nformula_plus : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
+val pexpr_times_nformula :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
-val eval_monoid : 'a1 -> 'a1 nFormula list -> monoidMember -> 'a1 pExprC
+val nformula_times_nformula :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
-val eval_cone :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula
- list -> 'a1 coneMember -> 'a1 nFormula
+val nformula_plus_nformula :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1
+ nFormula -> 'a1 nFormula option
-val normalise_pexpr :
+val eval_Psatz :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
- 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 polC
+ bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
+ nFormula option
val check_inconsistent :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
- 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
- nFormula -> bool
+ 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
val check_normalised_formulas :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
- 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
- nFormula list -> 'a1 coneMember -> bool
+ bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
type op2 =
| OpEq
@@ -280,27 +283,53 @@ type op2 =
| OpLt
| OpGt
-type 'c formula = { flhs : 'c pExprC; fop : op2; frhs : 'c pExprC }
+type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr }
-val flhs : 'a1 formula -> 'a1 pExprC
+val flhs : 'a1 formula -> 'a1 pExpr
val fop : 'a1 formula -> op2
-val frhs : 'a1 formula -> 'a1 pExprC
+val frhs : 'a1 formula -> 'a1 pExpr
-val xnormalise : 'a1 formula -> 'a1 nFormula list
+val norm :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
-val cnf_normalise : 'a1 formula -> 'a1 nFormula cnf
+val psub0 :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
+ -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
-val xnegate : 'a1 formula -> 'a1 nFormula list
+val padd0 :
+ 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
+ 'a1 pol
-val cnf_negate : 'a1 formula -> 'a1 nFormula cnf
+val xnormalise :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
+ list
-val simpl_expr : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 pExprC
+val cnf_normalise :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
+ cnf
+
+val xnegate :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
+ list
+
+val cnf_negate :
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
+ 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
+ cnf
+
+val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
+
+val denorm : 'a1 pol -> 'a1 pExpr
val simpl_cone :
- 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 coneMember
- -> 'a1 coneMember
+ 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz ->
+ 'a1 psatz
type q = { qnum : z; qden : positive }
@@ -320,6 +349,12 @@ val qopp : q -> q
val qminus : q -> q -> q
+val pgcdn : nat -> positive -> positive -> positive
+
+val pgcd : positive -> positive -> positive
+
+val zgcd : z -> z -> z
+
type 'a t =
| Empty
| Leaf of 'a
@@ -327,9 +362,15 @@ type 'a t =
val find : 'a1 -> 'a1 t -> positive -> 'a1
-type zWitness = z coneMember
+type zWitness = z psatz
+
+val zWeakChecker : z nFormula list -> z psatz -> bool
+
+val psub1 : z pol -> z pol -> z pol
-val zWeakChecker : z nFormula list -> z coneMember -> bool
+val padd1 : z pol -> z pol -> z pol
+
+val norm0 : z pExpr -> z pol
val xnormalise0 : z formula -> z nFormula list
@@ -341,35 +382,53 @@ val negate : z formula -> z nFormula cnf
val ceiling : z -> z -> z
-type proofTerm =
- | RatProof of zWitness
- | CutProof of z pExprC * q * zWitness * proofTerm
- | EnumProof of q * z pExprC * q * zWitness * zWitness * proofTerm list
+type zArithProof =
+ | DoneProof
+ | RatProof of zWitness * zArithProof
+ | CutProof of zWitness * zArithProof
+ | EnumProof of zWitness * zWitness * zArithProof list
+
+val isZ0 : z -> bool
+
+val zgcd_pol : z polC -> z * z
-val makeLb : z pExpr -> q -> z nFormula
+val zdiv_pol : z polC -> z -> z polC
-val qceiling : q -> z
+val makeCuttingPlane : z polC -> z polC * z
-val makeLbCut : z pExprC -> q -> z nFormula
+val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
-val neg_nformula : z nFormula -> z pExpr * op1
+val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
-val cutChecker :
- z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option
+val is_pol_Z0 : z polC -> bool
-val zChecker : z nFormula list -> proofTerm -> bool
+val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
-val zTautoChecker : z formula bFormula -> proofTerm list -> bool
+val check_inconsistent0 : z nFormula -> bool
-val map_cone : (nat -> nat) -> zWitness -> zWitness
+val zChecker : z nFormula list -> zArithProof -> bool
-val indexes : zWitness -> nat list
+val zTautoChecker : z formula bFormula -> zArithProof list -> bool
val n_of_Z : z -> n
-type qWitness = q coneMember
+type qWitness = q psatz
+
+val qWeakChecker : q nFormula list -> q psatz -> bool
+
+val qnormalise : q formula -> q nFormula cnf
-val qWeakChecker : q nFormula list -> q coneMember -> bool
+val qnegate : q formula -> q nFormula cnf
val qTautoChecker : q formula bFormula -> qWitness list -> bool
+type rWitness = z psatz
+
+val rWeakChecker : z nFormula list -> z psatz -> bool
+
+val rnormalise : z formula -> z nFormula cnf
+
+val rnegate : z formula -> z nFormula cnf
+
+val rTautoChecker : z formula bFormula -> rWitness list -> bool
+
diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib
index 518654a45..2bd79ce04 100644
--- a/plugins/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mllib
@@ -2,6 +2,7 @@ Mutils
Micromega
Mfourier
Certificate
+Persistent_cache
Coq_micromega
G_micromega
Micromega_plugin_mod
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 23db2928a..72b2a70b6 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -51,6 +51,7 @@ let rec map3 f l1 l2 l3 =
| _ -> raise (Invalid_argument "map3")
+
let rec is_sublist l1 l2 =
match l1 ,l2 with
| [] ,_ -> true
@@ -326,3 +327,65 @@ struct
_hash_list l 0
end
+
+module type Tag =
+sig
+ type t
+
+ val from : int -> t
+ val next : t -> t
+ val pp : out_channel -> t -> unit
+ val compare : t -> t -> int
+end
+
+module Tag : Tag =
+struct
+ type t = int
+ let from i = i
+ let next i = i + 1
+ let pp o i = output_string o (string_of_int i)
+ let compare : int -> int -> int = Pervasives.compare
+end
+
+module TagSet = Set.Make(Tag)
+
+
+let command exe_path args vl =
+
+ (* creating pipes for stdin, stdout, stderr *)
+ let (stdin_read,stdin_write) = Unix.pipe ()
+ and (stdout_read,stdout_write) = Unix.pipe ()
+ and (stderr_read,stderr_write) = Unix.pipe () in
+
+ (* Creating channels from dile descr *)
+ let outch = Unix.out_channel_of_descr stdin_write in
+ let inch = Unix.in_channel_of_descr stdout_read in
+
+ (* Create the process *)
+ let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in
+
+ (* Write the data on the stdin of the future process *)
+ Marshal.to_channel outch vl [Marshal.No_sharing] ;
+ flush outch ;
+
+ (* Wait for its completion *)
+ let _pid,status = Unix.waitpid [] pid in
+
+ (* Recover the result *)
+ let res =
+ match status with
+ | Unix.WEXITED 0 -> Marshal.from_channel inch
+ | _ -> None in
+
+ (* Cleanup *)
+ close_out outch ; close_in inch ;
+ List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stderr_write; stdout_write];
+ res
+
+
+
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
new file mode 100644
index 000000000..272cc8931
--- /dev/null
+++ b/plugins/micromega/persistent_cache.ml
@@ -0,0 +1,175 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(* *)
+(* A persistent hashtable *)
+(* *)
+(* Frédéric Besson (Inria Rennes) 2009 *)
+(* *)
+(************************************************************************)
+
+
+module type PHashtable =
+ sig
+ type 'a t
+ type key
+
+ val create : int -> string -> 'a t
+ (** [create i f] creates an empty persistent table
+ with initial size i
+ associated with file [f] *)
+
+
+ val open_in : string -> 'a t
+ (** [open_in f] rebuilds a table from the records stored in file [f] *)
+
+ val find : 'a t -> key -> 'a
+ (** find has the specification of Hashtable.find *)
+
+ val add : 'a t -> key -> 'a -> unit
+ (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl].
+ (and writes the binding to the file associated with [tbl].)
+ If [key] is already bound, raises KeyAlreadyBound *)
+
+ val close : 'a t -> unit
+ (** [close tbl] is closing the table.
+ Once closed, a table cannot be used.
+ i.e, copy, find,add will raise UnboundTable *)
+
+ end
+
+open Hashtbl
+
+module PHashtable(Key:HashedType) : PHashtable with type key = Key.t =
+struct
+
+ type key = Key.t
+
+ module Table = Hashtbl.Make(Key)
+
+
+
+ exception InvalidTableFormat
+ exception UnboundTable
+
+
+ type mode = Closed | Open
+
+
+ type 'a t =
+ {
+ outch : out_channel ;
+ mutable status : mode ;
+ htbl : 'a Table.t
+ }
+
+
+let create i f =
+ {
+ outch = open_out_bin f ;
+ status = Open ;
+ htbl = Table.create i
+ }
+
+let finally f rst =
+ try
+ let res = f () in
+ rst () ; res
+ with x ->
+ (try rst ()
+ with _ -> raise x
+ ); raise x
+
+
+(** [from_file f] returns a hashtable by parsing records from file [f].
+ The structure of the file is
+ (KEY NL ELEM NL)*
+ where
+ NL is the character '\n'
+ KEY and ELEM are strings (without NL) parsed
+ by the functions Key.parse and Elem.parse
+
+ Raises Sys_error if the file cannot be open
+ Raises InvalidTableFormat if the file does not conform to the format,
+*)
+
+
+let read_key_elem inch =
+ try
+ Some (Marshal.from_channel inch)
+ with
+ | End_of_file -> None
+ | _ -> raise InvalidTableFormat
+
+let open_in f =
+ let flags = [Open_rdonly;Open_binary;Open_creat] in
+ let inch = open_in_gen flags 0o666 f in
+ let htbl = Table.create 10 in
+
+ let rec xload () =
+ match read_key_elem inch with
+ | None -> ()
+ | Some (key,elem) ->
+ Table.add htbl key elem ;
+ xload () in
+
+ try
+ finally (fun () -> xload () ) (fun () -> close_in inch) ;
+ {
+ outch = begin
+ let flags = [Open_append;Open_binary;Open_creat] in
+ open_out_gen flags 0o666 f
+ end ;
+ status = Open ;
+ htbl = htbl
+ }
+ with InvalidTableFormat ->
+ (* Try to keep as many entries as possible *)
+ begin
+ let flags = [Open_wronly; Open_trunc;Open_binary;Open_creat] in
+ let outch = open_out_gen flags 0o666 f in
+ Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
+ { outch = outch ;
+ status = Open ;
+ htbl = htbl
+ }
+ end
+
+
+let close t =
+ let {outch = outch ; status = status ; htbl = tbl} = t in
+ match t.status with
+ | Closed -> () (* don't do it twice *)
+ | Open ->
+ close_out outch ;
+ Table.clear tbl ;
+ t.status <- Closed
+
+let add t k e =
+ let {outch = outch ; status = status ; htbl = tbl} = t in
+ if status = Closed
+ then raise UnboundTable
+ else
+ begin
+ Table.add tbl k e ;
+ Marshal.to_channel outch (k,e) [Marshal.No_sharing]
+ end
+
+let find t k =
+ let {outch = outch ; status = status ; htbl = tbl} = t in
+ if status = Closed
+ then raise UnboundTable
+ else
+ let res = Table.find tbl k in
+ res
+
+end
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index e3d72ed9a..4085eb069 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -1125,6 +1125,7 @@ let file_of_string filename s =
let fd = Pervasives.open_out filename in
output_string fd s; close_out fd
+(*
let request_mark = "*** REQUEST ***"
let answer_mark = "*** ANSWER ***"
let end_mark = "*** END ***"
@@ -1171,16 +1172,16 @@ let flush_to_cache string_problem string_result =
close_out outch
with Sys_error _ ->
print_endline "Warning: Could not open or write to csdp cache"
-
+*)
exception CsdpInfeasible
let run_csdp dbg string_problem =
- try
+(* try
let res = look_in_cache string_problem in
if res = infeasible_mark then raise CsdpInfeasible;
if res = failure_mark then failwith "csdp error";
res
- with Not_found ->
+ with Not_found -> *)
let input_file = Filename.temp_file "sos" ".dat-s" in
let output_file = Filename.temp_file "sos" ".dat-s" in
let temp_path = Filename.dirname input_file in
@@ -1189,15 +1190,15 @@ let run_csdp dbg string_problem =
file_of_string params_file csdp_params;
let rv = Sys.command("cd "^temp_path^"; csdp "^input_file^" "^output_file^
(if dbg then "" else "> /dev/null")) in
- if rv = 1 or rv = 2 then
- (flush_to_cache string_problem infeasible_mark; raise CsdpInfeasible);
+ if rv = 1 or rv = 2 then
+ ((*flush_to_cache string_problem infeasible_mark;*) raise CsdpInfeasible);
if rv = 127 then
(print_string "csdp not found, exiting..."; exit 1);
if rv <> 0 & rv <> 3 (* reduced accuracy *) then
- (flush_to_cache string_problem failure_mark;
+ ((*flush_to_cache string_problem failure_mark;*)
failwith("csdp: error "^string_of_int rv));
let string_result = string_of_file output_file in
- flush_to_cache string_problem string_result;
+(* flush_to_cache string_problem string_result;*)
if not dbg then
(Sys.remove input_file; Sys.remove output_file; Sys.remove params_file);
string_result
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 13:27:47 +0000