diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/RMicromega.v | 6 | ||||
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 12 | ||||
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 7 |
3 files changed, 16 insertions, 9 deletions
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 2b6ef8c5d..3f29a4fcf 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -67,7 +67,7 @@ Lemma RZSORaddon : SORaddon R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) Zeq_bool Zle_bool - IZR Nnat.nat_of_N pow. + IZR nat_of_N pow. Proof. constructor. constructor ; intros ; try reflexivity. @@ -94,7 +94,7 @@ Definition INZ (n:N) : R := | Npos p => IZR (Zpos p) end. -Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow. +Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR nat_of_N pow. Definition Reval_op2 (o:Op2) : R -> R -> Prop := @@ -112,7 +112,7 @@ Definition Reval_formula (e: PolEnv R) (ff : Formula Z) := let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs). Definition Reval_formula' := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR nat_of_N pow. Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index aa32b386c..e8e02f2ca 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -142,12 +142,12 @@ Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := Definition PhiR : list R -> PolZ -> R := (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)). -Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n). +Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (N_of_nat n). Definition PEevalR : list R -> PEZ -> R := PEeval 0 ring_plus ring_mult ring_sub ring_opp (gen_phiZ 0 1 ring_plus ring_mult ring_opp) - Nnat.nat_of_N pow. + nat_of_N pow. Lemma P0Z_correct : forall l, PhiR l P0Z = 0. Proof. trivial. Qed. @@ -177,8 +177,8 @@ Proof. Qed. Lemma R_power_theory - : power_theory 1 ring_mult ring_eq Nnat.nat_of_N pow. -apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. + : power_theory 1 ring_mult ring_eq nat_of_N pow. +apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. Lemma norm_correct : forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). @@ -288,7 +288,7 @@ Fixpoint interpret3 t fv {struct t}: R := | (PEopp t1) => let v1 := interpret3 t1 fv in (ring_opp v1) | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2) + let v1 := interpret3 t1 fv in pow v1 (nat_of_N t2) | (PEc t1) => (IZR1 t1) | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 end. @@ -484,7 +484,7 @@ Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := tacsimpl; repeat (split;[assumption|idtac]); exact I | simpl in Hg2; tacsimpl; - apply Rdomain_pow with (interpret3 _ Rd c fv) (Nnat.nat_of_N r); auto with domain; + apply Rdomain_pow with (interpret3 _ Rd c fv) (nat_of_N r); auto with domain; tacsimpl; apply domain_axiom_one_zero || (simpl) || idtac "could not prove discrimination result" ] diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index ff433bbd8..5b6f4670f 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -298,3 +298,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x). + +Theorem intro_Z : + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros n; exists (Z_of_nat n); split; trivial. + rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat. +Qed. |