diff options
author | 2011-05-25 08:44:59 +0000 | |
---|---|---|
committer | 2011-05-25 08:44:59 +0000 | |
commit | 7f19da0503ce5895f3ad4080f4fb96dc2287aa26 (patch) | |
tree | 81c70926bb8833c2ec04dceff7a6ecd17c0638b3 /plugins | |
parent | 77f1db2c35d3d337f4a47dc98d02f3c4749d9ade (diff) |
Q2R -> IQR
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14155 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/micromega/RMicromega.v | 113 | ||||
-rw-r--r-- | plugins/micromega/VarMap.v | 211 | ||||
-rw-r--r-- | plugins/micromega/certificate.ml | 2 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 4 | ||||
-rw-r--r-- | plugins/micromega/polynomial.ml | 6 |
5 files changed, 66 insertions, 270 deletions
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index eb4847486..2be99da1e 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -19,6 +19,7 @@ Require Import Raxioms RIneq Rpow_def DiscrR. Require Import QArith. Require Import Qfield. + Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -63,7 +64,7 @@ Proof. apply (Rmult_lt_compat_r) ; auto. Qed. -Definition Q2R := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R. +Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R. Lemma Rinv_elim : forall x y z, @@ -123,9 +124,9 @@ Qed. Lemma Qeq_true : forall x y, Qeq_bool x y = true -> - Q2R x = Q2R y. + IQR x = IQR y. Proof. - unfold Q2R. + unfold IQR. simpl. intros. apply Qeq_bool_eq in H. @@ -143,12 +144,12 @@ Proof. split ; apply Rlt_neq ; auto. Qed. -Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y. +Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y. Proof. intros. apply Qeq_bool_neq in H. intro. apply H. clear H. - unfold Qeq,Q2R in *. + unfold Qeq,IQR in *. simpl in *. revert H0. repeat Rinv_elim. @@ -166,12 +167,12 @@ Qed. -Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y. +Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y. Proof. intros. apply Qle_bool_imp_le in H. unfold Qle in H. - unfold Q2R. + unfold IQR. simpl in *. apply IZR_le in H. repeat rewrite mult_IZR in H. @@ -191,20 +192,20 @@ Qed. -Lemma Q2R_0 : Q2R 0 = 0. +Lemma IQR_0 : IQR 0 = 0. Proof. compute. apply Rinv_1. Qed. -Lemma Q2R_1 : Q2R 1 = 1. +Lemma IQR_1 : IQR 1 = 1. Proof. compute. apply Rinv_1. Qed. -Lemma Q2R_plus : forall x y, Q2R (x + y) = Q2R x + Q2R y. +Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y. Proof. intros. - unfold Q2R. + unfold IQR. simpl in *. rewrite plus_IZR in *. rewrite mult_IZR in *. @@ -218,28 +219,28 @@ Proof. split ; apply Rlt_neq ; auto. Qed. -Lemma Q2R_opp : forall x, Q2R (- x) = - Q2R x. +Lemma IQR_opp : forall x, IQR (- x) = - IQR x. Proof. intros. - unfold Q2R. + unfold IQR. simpl. rewrite opp_IZR. ring. Qed. -Lemma Q2R_minus : forall x y, Q2R (x - y) = Q2R x - Q2R y. +Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y. Proof. intros. unfold Qminus. - rewrite Q2R_plus. - rewrite Q2R_opp. + rewrite IQR_plus. + rewrite IQR_opp. ring. Qed. -Lemma Q2R_mult : forall x y, Q2R (x * y) = Q2R x * Q2R y. +Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y. Proof. - unfold Q2R ; intros. + unfold IQR ; intros. simpl. repeat rewrite mult_IZR. simpl. @@ -249,10 +250,10 @@ Proof. intros. field ; split ; apply Rlt_neq ; auto. Qed. -Lemma Q2R_inv_lt : forall x, (0 < x)%Q -> - Q2R (/ x) = / Q2R x. +Lemma IQR_inv_lt : forall x, (0 < x)%Q -> + IQR (/ x) = / IQR x. Proof. - unfold Q2R ; simpl. + unfold IQR ; simpl. intros. unfold Qlt in H. revert H. @@ -301,10 +302,10 @@ Proof. apply Ropp_eq_0_compat ; auto. Qed. -Lemma Q2R_x_0 : forall x, Q2R x = 0 -> x == 0%Q. +Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q. Proof. destruct x ; simpl. - unfold Q2R. + unfold IQR. simpl. INR_nat_of_P. intros. @@ -320,20 +321,20 @@ Proof. Qed. -Lemma Q2R_inv_gt : forall x, (0 > x)%Q -> - Q2R (/ x) = / Q2R x. +Lemma IQR_inv_gt : forall x, (0 > x)%Q -> + IQR (/ x) = / IQR x. Proof. intros. rewrite <- (Qopp_involutive_strong x). rewrite <- Qinv_opp. - rewrite Q2R_opp. - rewrite Q2R_inv_lt. - repeat rewrite Q2R_opp. + rewrite IQR_opp. + rewrite IQR_inv_lt. + repeat rewrite IQR_opp. rewrite Ropp_inv_permute. auto. intro. apply Ropp_0 in H0. - apply Q2R_x_0 in H0. + apply IQR_x_0 in H0. rewrite H0 in H. compute in H. discriminate. unfold Qlt in *. @@ -341,8 +342,8 @@ Proof. auto with zarith. Qed. -Lemma Q2R_inv : forall x, ~ x == 0 -> - Q2R (/ x) = / Q2R x. +Lemma IQR_inv : forall x, ~ x == 0 -> + IQR (/ x) = / IQR x. Proof. intros. assert ( 0 > x \/ 0 < x)%Q. @@ -352,12 +353,12 @@ Proof. right. reflexivity. left ; reflexivity. destruct H0. - apply Q2R_inv_gt ; auto. - apply Q2R_inv_lt ; auto. + apply IQR_inv_gt ; auto. + apply IQR_inv_lt ; auto. Qed. -Lemma Q2R_inv_ext : forall x, - Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x). +Lemma IQR_inv_ext : forall x, + IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x). Proof. intros. case_eq (Qeq_bool x 0). @@ -371,7 +372,7 @@ Proof. reflexivity. rewrite <- H. ring. intros. - apply Q2R_inv. + apply IQR_inv. intro. rewrite <- Qeq_bool_iff in H0. congruence. @@ -385,16 +386,16 @@ Lemma QSORaddon : R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *) Qeq_bool Qle_bool - Q2R nat to_nat pow. + IQR nat to_nat pow. Proof. constructor. constructor ; intros ; try reflexivity. - apply Q2R_0. - apply Q2R_1. - apply Q2R_plus. - apply Q2R_minus. - apply Q2R_mult. - apply Q2R_opp. + apply IQR_0. + apply IQR_1. + apply IQR_plus. + apply IQR_minus. + apply IQR_mult. + apply IQR_opp. apply Qeq_true ; auto. apply R_power_theory. apply Qeq_false. @@ -435,7 +436,7 @@ Fixpoint R_of_Rcst (r : Rcst) : R := | C0 => R0 | C1 => R1 | CZ z => IZR z - | CQ q => Q2R q + | CQ q => IQR q | CPlus r1 r2 => (R_of_Rcst r1) + (R_of_Rcst r2) | CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2) | CMult r1 r2 => (R_of_Rcst r1) * (R_of_Rcst r2) @@ -446,20 +447,20 @@ Fixpoint R_of_Rcst (r : Rcst) : R := | COpp r => - (R_of_Rcst r) end. -Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c. +Lemma Q_of_RcstR : forall c, IQR (Q_of_Rcst c) = R_of_Rcst c. Proof. induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2). - apply Q2R_0. - apply Q2R_1. + apply IQR_0. + apply IQR_1. reflexivity. - unfold Q2R. simpl. rewrite Rinv_1. reflexivity. - apply Q2R_plus. - apply Q2R_minus. - apply Q2R_mult. + unfold IQR. simpl. rewrite Rinv_1. reflexivity. + apply IQR_plus. + apply IQR_minus. + apply IQR_mult. rewrite <- IHc. - apply Q2R_inv_ext. + apply IQR_inv_ext. rewrite <- IHc. - apply Q2R_opp. + apply IQR_opp. Qed. Require Import EnvRing. @@ -492,7 +493,7 @@ Definition Reval_formula' := eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt nat_of_N pow R_of_Rcst. Definition QReval_formula := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R nat_of_N pow . + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR nat_of_N pow . Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. @@ -507,12 +508,12 @@ Proof. Qed. Definition Qeval_nformula := - eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R. + eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt IQR. Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d). Proof. - exact (fun env d =>eval_nformula_dec Rsor Q2R env d). + exact (fun env d =>eval_nformula_dec Rsor IQR env d). Qed. Definition RWitness := Psatz Q. diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 6c248e839..f41252b78 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -45,217 +45,6 @@ Section MakeVarMap. end end. - (* FK: scheduled for deletion *) - (* an off_map (a map with offset) offers the same functionalites as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *) - (* - Definition off_map := (option positive *t )%type. - - - - Definition jump (j:positive) (l:off_map ) := - let (o,m) := l in - match o with - | None => (Some j,m) - | Some j0 => (Some (j+j0)%positive,m) - end. - - Definition nth (n:positive) (l: off_map ) := - let (o,m) := l in - let idx := match o with - | None => n - | Some i => i + n - end%positive in - find idx m. - - - Definition hd (l:off_map) := nth xH l. - - - Definition tail (l:off_map ) := jump xH l. - - - Lemma psucc : forall p, (match p with - | xI y' => xO (Psucc y') - | xO y' => xI y' - | 1%positive => 2%positive - end) = (p+1)%positive. - Proof. - destruct p. - auto with zarith. - rewrite xI_succ_xO. - auto with zarith. - reflexivity. - Qed. - - Lemma jump_Pplus : forall i j l, - (jump (i + j) l) = (jump i (jump j l)). - Proof. - unfold jump. - destruct l. - destruct o. - rewrite Pplus_assoc. - reflexivity. - reflexivity. - Qed. - - Lemma jump_simpl : forall p l, - jump p l = - match p with - | xH => tail l - | xO p => jump p (jump p l) - | xI p => jump p (jump p (tail l)) - end. - Proof. - destruct p ; unfold tail ; intros ; repeat rewrite <- jump_Pplus. - (* xI p = p + p + 1 *) - rewrite xI_succ_xO. - rewrite Pplus_diag. - rewrite <- Pplus_one_succ_r. - reflexivity. - (* xO p = p + p *) - rewrite Pplus_diag. - reflexivity. - reflexivity. - Qed. - - Ltac jump_s := - repeat - match goal with - | |- context [jump xH ?e] => rewrite (jump_simpl xH) - | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p)) - | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p)) - end. - - Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). - Proof. - unfold tail. - intros. - repeat rewrite <- jump_Pplus. - rewrite Pplus_comm. - reflexivity. - Qed. - - Lemma jump_Psucc : forall j l, - (jump (Psucc j) l) = (jump 1 (jump j l)). - Proof. - intros. - rewrite <- jump_Pplus. - rewrite Pplus_one_succ_r. - rewrite Pplus_comm. - reflexivity. - Qed. - - Lemma jump_Pdouble_minus_one : forall i l, - (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). - Proof. - unfold tail. - intros. - repeat rewrite <- jump_Pplus. - rewrite <- Pplus_one_succ_r. - rewrite Psucc_o_double_minus_one_eq_xO. - rewrite Pplus_diag. - reflexivity. - Qed. - - Lemma jump_x0_tail : forall p l, jump (xO p) (tail l) = jump (xI p) l. - Proof. - intros. - jump_s. - repeat rewrite <- jump_Pplus. - reflexivity. - Qed. - - - Lemma nth_spec : forall p l, - nth p l = - match p with - | xH => hd l - | xO p => nth p (jump p l) - | xI p => nth p (jump p (tail l)) - end. - Proof. - unfold nth. - destruct l. - destruct o. - simpl. - rewrite psucc. - destruct p. - replace (p0 + xI p)%positive with ((p + (p0 + 1) + p))%positive. - reflexivity. - rewrite xI_succ_xO. - rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag. - rewrite Pplus_comm. - symmetry. - rewrite (Pplus_comm p0). - rewrite <- Pplus_assoc. - rewrite (Pplus_comm 1)%positive. - rewrite <- Pplus_assoc. - reflexivity. - (**) - replace ((p0 + xO p))%positive with (p + p0 + p)%positive. - reflexivity. - rewrite <- Pplus_diag. - rewrite <- Pplus_assoc. - rewrite Pplus_comm. - rewrite Pplus_assoc. - reflexivity. - reflexivity. - simpl. - destruct p. - rewrite xI_succ_xO. - rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag. - symmetry. - rewrite Pplus_comm. - rewrite Pplus_assoc. - reflexivity. - rewrite Pplus_diag. - reflexivity. - reflexivity. - Qed. - - - Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l). - Proof. - destruct l. - unfold tail. - unfold hd. - unfold jump. - unfold nth. - destruct o. - symmetry. - rewrite Pplus_comm. - rewrite <- Pplus_assoc. - rewrite (Pplus_comm p0). - reflexivity. - rewrite Pplus_comm. - reflexivity. - Qed. - - Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). - Proof. - destruct l. - unfold tail. - unfold nth, jump. - destruct o. - rewrite ((Pplus_comm p)). - rewrite <- (Pplus_assoc p0). - rewrite Pplus_diag. - rewrite <- Psucc_o_double_minus_one_eq_xO. - rewrite Pplus_one_succ_r. - rewrite (Pplus_comm (Pdouble_minus_one p)). - rewrite Pplus_assoc. - rewrite (Pplus_comm p0). - reflexivity. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO. - rewrite Pplus_diag. - reflexivity. - Qed. - -*) End MakeVarMap. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 5efe9f426..540d1b9c1 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1182,6 +1182,7 @@ let reduce_var_change psys = let lia sys = + LinPoly.MonT.clear (); let sys = List.map (develop_constraint z_spec) sys in let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in let sys = mapi (fun c i -> (c,Hyp i)) sys in @@ -1189,6 +1190,7 @@ let reduce_var_change psys = let nlia sys = + LinPoly.MonT.clear (); let sys = List.map (develop_constraint z_spec) sys in let sys = mapi (fun c i -> (c,Hyp i)) sys in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 42d451a2d..50b01d751 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -407,7 +407,7 @@ struct let coq_Rdiv = lazy (r_constant "Rdiv") let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") - let coq_Q2R = lazy (constant "Q2R") + let coq_IQR = lazy (constant "IQR") let coq_IZR = lazy (constant "IZR") let coq_PEX = lazy (constant "PEX" ) @@ -997,7 +997,7 @@ struct ParseError -> match op with | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0)) - | op when op = Lazy.force coq_Q2R -> Mc.CQ (parse_q args.(0)) + | op when op = Lazy.force coq_IQR -> Mc.CQ (parse_q args.(0)) (* | op when op = Lazy.force coq_IZR -> Mc.CZ (parse_z args.(0))*) | _ -> raise ParseError end diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index d203f0e87..14d312a5c 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -590,9 +590,13 @@ struct (** A hash table might be preferable but requires a hash function. *) let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) let (monomial_of_index : Monomial.t IntMap.t ref) = ref (IntMap.empty) + let fresh = ref 0 + let clear () = + index_of_monomial := MonoMap.empty; + monomial_of_index := IntMap.empty ; + fresh := 0 - let fresh = ref 0 let register m = try |