Commit fa40ac39 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Adapt to new definition of IZR.

parent b28d90f7
...@@ -387,132 +387,20 @@ Qed. ...@@ -387,132 +387,20 @@ Qed.
End Rmissing. End Rmissing.
Section Z2R. Notation Z2R := IZR.
Notation Z2R_opp := opp_IZR.
(** Z2R function (Z -> R) *) Notation Z2R_plus := plus_IZR.
Fixpoint P2R (p : positive) := Notation Z2R_minus := minus_IZR.
match p with Notation Z2R_mult := mult_IZR.
| xH => 1%R Notation le_Z2R := le_IZR.
| xO xH => 2%R Notation Z2R_le := IZR_le.
| xO t => (2 * P2R t)%R Notation lt_Z2R := lt_IZR.
| xI xH => 3%R Notation Z2R_lt := IZR_lt.
| xI t => (1 + 2 * P2R t)%R Notation eq_Z2R := eq_IZR.
end. Notation Z2R_neq := IZR_neq.
Notation Z2R_abs := abs_IZR.
Definition Z2R n :=
match n with
| Zpos p => P2R p
| Zneg p => Ropp (P2R p)
| Z0 => R0
end.
Theorem P2R_INR :
forall n, P2R n = INR (nat_of_P n).
Proof.
induction n ; simpl ; try (
rewrite IHn ;
rewrite <- (mult_INR 2) ;
rewrite <- (nat_of_P_mult_morphism 2) ;
change (2 * n)%positive with (xO n)).
(* xI *)
rewrite (Rplus_comm 1).
change (nat_of_P (xO n)) with (Pmult_nat n 2).
case n ; intros ; simpl ; try apply refl_equal.
case (Pmult_nat p 4) ; intros ; try apply refl_equal.
rewrite Rplus_0_l.
apply refl_equal.
apply Rplus_comm.
(* xO *)
case n ; intros ; apply refl_equal.
(* xH *)
apply refl_equal.
Qed.
Theorem Z2R_IZR :
forall n, Z2R n = IZR n.
Proof.
intro.
case n ; intros ; simpl.
apply refl_equal.
apply P2R_INR.
apply Ropp_eq_compat.
apply P2R_INR.
Qed.
Theorem Z2R_opp :
forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply Ropp_Ropp_IZR.
Qed.
Theorem Z2R_plus :
forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply plus_IZR.
Qed.
Theorem minus_IZR :
forall n m : Z,
IZR (n - m) = (IZR n - IZR m)%R.
Proof.
intros.
unfold Zminus.
rewrite plus_IZR.
rewrite Ropp_Ropp_IZR.
apply refl_equal.
Qed.
Theorem Z2R_minus :
forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply minus_IZR.
Qed.
Theorem Z2R_mult :
forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply mult_IZR.
Qed.
Theorem le_Z2R :
forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply le_IZR.
Qed.
Theorem Z2R_le :
forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_le.
Qed.
Theorem lt_Z2R :
forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply lt_IZR.
Qed.
Theorem Z2R_lt : Section Z2R.
forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_lt.
Qed.
Theorem Z2R_le_lt : Theorem Z2R_le_lt :
forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R. forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R.
...@@ -532,14 +420,6 @@ now apply le_Z2R. ...@@ -532,14 +420,6 @@ now apply le_Z2R.
now apply lt_Z2R. now apply lt_Z2R.
Qed. Qed.
Theorem eq_Z2R :
forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z.
Proof.
intros m n H.
apply eq_IZR.
now rewrite <- 2!Z2R_IZR.
Qed.
Theorem neq_Z2R : Theorem neq_Z2R :
forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z. forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z.
Proof. Proof.
...@@ -548,22 +428,6 @@ apply H. ...@@ -548,22 +428,6 @@ apply H.
now apply f_equal. now apply f_equal.
Qed. Qed.
Theorem Z2R_neq :
forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_neq.
Qed.
Theorem Z2R_abs :
forall z, Z2R (Zabs z) = Rabs (Z2R z).
Proof.
intros.
repeat rewrite Z2R_IZR.
now rewrite Rabs_Zabs.
Qed.
End Z2R. End Z2R.
(** Decidable comparison on reals *) (** Decidable comparison on reals *)
...@@ -1000,7 +864,6 @@ intros x. ...@@ -1000,7 +864,6 @@ intros x.
unfold Zfloor. unfold Zfloor.
rewrite Z2R_minus. rewrite Z2R_minus.
simpl. simpl.
rewrite Z2R_IZR.
apply Rplus_le_reg_r with (1 - x)%R. apply Rplus_le_reg_r with (1 - x)%R.
ring_simplify. ring_simplify.
exact (proj2 (archimed x)). exact (proj2 (archimed x)).
...@@ -1016,7 +879,6 @@ rewrite Z2R_minus. ...@@ -1016,7 +879,6 @@ rewrite Z2R_minus.
unfold Rminus. unfold Rminus.
rewrite Rplus_assoc. rewrite Rplus_assoc.
rewrite Rplus_opp_l, Rplus_0_r. rewrite Rplus_opp_l, Rplus_0_r.
rewrite Z2R_IZR.
exact (proj1 (archimed x)). exact (proj1 (archimed x)).
Qed. Qed.
...@@ -1643,7 +1505,7 @@ intros e. ...@@ -1643,7 +1505,7 @@ intros e.
unfold bpow. unfold bpow.
rewrite Zpower_pos_nat. rewrite Zpower_pos_nat.
unfold Z2R at 2. unfold Z2R at 2.
rewrite P2R_INR. rewrite <- INR_IPR.
induction (nat_of_P e). induction (nat_of_P e).
rewrite Rmult_0_l. rewrite Rmult_0_l.
now rewrite exp_0. now rewrite exp_0.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment