Rplus.v: Definition of R+

Require Export Uprop.
Open Local Scope U_scope.
Require Export Omega.
Require Export Arith.

Extra axiom on U : test of order

Variable isle : U -> U -> bool.
Hypothesis isle_true_eq : forall x y, x <= y <-> isle x y = true.

Lemma isle_true : forall x y, x <= y -> isle x y = true.

Lemma isle_false_iff : forall x y, ~ (x <= y) <-> isle x y = false.

Lemma isle_false_nle : forall x y, ~ (x <= y) -> isle x y = false.

Lemma isle_false : forall x y, y < x -> isle x y = false.

Hint Resolve isle_true_eq isle_false_iff.

Hint Immediate isle_true isle_false isle_false_nle.

Lemma isle_rec : forall (x y:U) (P : bool -> Type),
(x <= y -> P true)
-> (y < x -> P false)
-> P (isle x y).

Lemma isle_lt_dec : forall x y : U, {x <= y} + {y < x}.

Lemma isle_dec : forall x y : U, {x <= y} + { ~ x <= y}.

Lemma iseq_dec : forall x y : U, {x == y} + { ~ x == y}.

Hint Resolve isle_dec iseq_dec.

Add Morphism isle with signature Oeq ==> Oeq ==> eq as isle_eq_compat.
Save.

Definition is0 (x:U) := isle x 0.

Definition is1 (x:U) := isle 1 x.

Definition of Rp with integer part and fractional part in U

Record Rp := mkRp { int:nat; frac:U }.

Delimit Scope Rp_scope with Rp.
Open Local Scope Rp_scope.

Lemma int_simpl : forall n x, int (mkRp n x) = n.

Lemma frac_simpl : forall n x, frac (mkRp n x) = x.

Lemma mkRp_eta : forall r, r = mkRp (int r) (frac r).
Hint Resolve mkRp_eta.

Avoid two representations of same value (n,1)==(S n,0)

Lemma orc_lt_eq1 : forall x, orc (x < 1) (x == 1) .

Lemma or_lt_eq1 : forall x, (x < 1) \/ (x == 1) .

Definition if1 {A} (x:U) (o1 o2:A) : A := if isle_dec U1 x then o1 else o2.

Lemma if1_eq1 : forall {A} (x:U) (o1 o2:A), 1 <= x -> if1 x o1 o2 = o1.

Lemma if1_lt1 : forall {A} (x:U) (o1 o2:A), x < 1 -> if1 x o1 o2 = o2.

Hint Resolve @if1_eq1 @if1_lt1.

Lemma if1_elim : forall {A} (x:U) (o1 o2:A) (P:A -> Type),
(x == 1 -> P o1) -> (x < 1 -> P o2) -> P (if1 x o1 o2).

Add Parametric Morphism {A} {o:ord A} : (if1 (A:=A)) with signature
Oeq ==> Oeq ==> Oeq ==> Oeq as if1_eq_compat_ord.
Save.

Add Parametric Morphism {A} : (if1 (A:=A)) with signature
Oeq ==> eq ==> eq ==> eq as if1_eq_compat.
Save.

Hint Immediate if1_eq_compat if1_eq_compat_ord.

Definition floor (r : Rp) : nat := if1 (frac r) (S (int r)) (int r).

Definition decimal (r : Rp) : U := if1 (frac r) 0%U (frac r).

Lemma floor_int : forall x, frac x < 1%U -> floor x = int x.
Hint Resolve floor_int.

Lemma floor_int_equiv : forall x, frac x < 1%U <-> floor x = int x.

Lemma floor_mkRp_int n x : (x < 1)%U -> floor (mkRp n x) = n.
Hint Resolve floor_mkRp_int.

Lemma decimal_frac : forall x, frac x < 1%U -> decimal x = frac x.
Hint Resolve decimal_frac.

Lemma decimal_frac_equiv : forall x, frac x < 1%U <-> decimal x = frac x.

Lemma decimal_mkRp_frac : forall n x, (x < 1)%U -> decimal (mkRp n x) = x.
Hint Resolve decimal_mkRp_frac.

Lemma floor_S_int : forall x, 1%U <= frac x -> floor x = S (int x).
Hint Resolve floor_S_int.

Lemma floor_S_int_equiv : forall x, frac x == 1%U <-> floor x = S (int x).

Lemma floor_mkRp_S_int n x : (x == 1)%U -> floor (mkRp n x) = S n.
Hint Resolve floor_mkRp_S_int.

Lemma decimal_0 : forall x, 1%U <= frac x -> decimal x = 0.
Hint Resolve decimal_0.

Lemma decimal_0_equiv : forall x, (frac x == 0 \/ frac x == 1%U) <-> decimal x == 0.

Lemma decimal_mkRp_0 : forall n x, (x == 1)%U -> decimal (mkRp n x) = 0.
Hint Resolve decimal_mkRp_0.

Lemma decimal_lt1 : forall x, decimal x < 1%U.
Hint Resolve decimal_lt1.

Lemma int_floor_le : forall x, int x <= floor x.
Hint Resolve int_floor_le.

Lemma decimal_frac_le : forall x, decimal x <= frac x.
Hint Resolve decimal_frac_le.

Morphism with Leibniz equality on the argument

Add Morphism frac with signature eq ==> Oeq as frac_eq_compat.
Save.

Add Morphism int with signature eq ==> eq as int_eq_compat.
Save.

From N and U to Rp

Definition N2Rp n := mkRp n 0.
Definition U2Rp x := mkRp 0 x.

Coercion U2Rp : U >-> Rp.
Coercion N2Rp : nat >-> Rp.

Notation R0 := (N2Rp 0).
Notation R1 := (N2Rp 1).

Lemma floorN2Rp : forall n:nat, floor n = n.

Lemma decimalN2Rp_eq : forall n:nat, decimal n = 0.

Hint Resolve decimalN2Rp_eq floorN2Rp.

Lemma decimalN2Rp : forall n:nat, decimal n == 0.
Hint Resolve decimalN2Rp.

Lemma floorU2Rp : forall x:U, x < 1 -> floor x = O.

Lemma decimalU2Rp_eq : forall x:U, x < 1 -> decimal x = x.

Hint Resolve floorU2Rp decimalU2Rp_eq.

Lemma decimalU2Rp : forall x:U, x < 1 -> decimal x == x.
Hint Resolve decimalU2Rp.

Lemma floorU1_eq : forall x, x==1 -> floor x = 1%nat.
Hint Resolve floorU1_eq.

Lemma decimalU1_eq : forall x, x==1 -> decimal x = 0%U.
Hint Resolve decimalU1_eq.

Lemma floorU1 : floor U1 = 1%nat.

Lemma decimalU1 : decimal U1 = 0%U.
Hint Resolve floorU1 decimalU1.

Order structure on Rp

Definition Rpeq r1 r2 := floor r1 = floor r2 /\ decimal r1 == decimal r2.

Definition Rple r1 r2
:= (floor r1 < floor r2)%nat \/ (floor r1 = floor r2 /\ decimal r1 <= decimal r2).

Instance Rpord : ord Rp := {Oeq := Rpeq; Ole := Rple}.
Defined.

Lemma Rpeq_simpl
: forall x y : Rp, (x == y) = (floor x = floor y /\ decimal x == decimal y).

Lemma Rpeq_intro
: forall x y : Rp, floor x = floor y -> decimal x == decimal y -> x == y.

Lemma Rple_simpl : forall x y : Rp,
(x <= y) = ((floor x < floor y)%nat \/ (floor x = floor y /\ decimal x <= decimal y)).

Lemma Rple_intro_lt : forall x y : Rp,
(floor x < floor y)%nat -> x <= y.

Lemma Rple_intro_eq : forall x y : Rp,
floor x = floor y -> decimal x <= decimal y -> x <= y.

Hint Resolve Rpeq_intro Rple_intro_lt Rple_intro_eq.

Lemma Rple_intro_le_floor : forall x y : Rp,
(floor x <= floor y)%nat -> decimal x <= decimal y -> x <= y.
Hint Immediate Rple_intro_le_floor.

Lemma Rplt_intro_lt_floor : forall x y : Rp,
(floor x < floor y)%nat -> x < y.
Hint Resolve Rplt_intro_lt_floor.

Lemma Rplt_intro_lt_decimal : forall x y : Rp,
(floor x = floor y)%nat -> decimal x < decimal y -> x < y.
Hint Resolve Rplt_intro_lt_decimal.

Add Morphism mkRp with signature eq ==> Oeq ==> Oeq
as mkRp_eq_compat.
Save.

Add Morphism mkRp with signature le ==> Ole ==> Ole
as mkRp_le_compat.
Save.

Hint Resolve mkRp_eq_compat mkRp_le_compat.

Lemma Rpeq_norm : forall n x, (x==1)%U -> mkRp n x == (S n).
Hint Resolve Rpeq_norm.

Lemma Rpeq_norm1 : forall n,mkRp n 1 == (S n).
Hint Resolve Rpeq_norm1.

Add Morphism floor with signature Oeq ==> eq as floor_eq_compat.
Save.

Add Morphism floor with signature Ole ==> le as floor_le_compat.
Save.

Hint Resolve floor_eq_compat floor_le_compat.

Add Morphism decimal with signature Oeq ==> Oeq as decimal_eq_compat.
Save.

Lemma floor_decimal_mkRp_elim : forall n d (R : Rp -> Prop),
(forall x, x == mkRp n d -> R x -> R (mkRp n d)) ->
(d < 1 -> R (mkRp n d)) -> (d == 1 -> R (S n)) -> R (mkRp n d).

Lemma floor_decimal_U2Rp_elim : forall (x:U) (R : nat -> U -> Prop),
(x < 1 -> R 0%nat x) -> (x == 1 -> R 1%nat 0) -> R (floor x) (decimal x).

Lemma decimal_eq_R0 : forall x, x == R0 -> decimal x == 0.

Lemma floor_eq_R0 : forall x, x == R0 -> floor x = O.

Hint Immediate floor_eq_R0 decimal_eq_R0.

Lemma floorR0 : floor R0 = O.

Lemma decimalR0 : decimal R0 == 0.
Hint Resolve floorR0 decimalR0.

Lemma floor_decimal : forall x, x == mkRp (floor x) (decimal x).
Hint Resolve floor_decimal.

Add Morphism U2Rp with signature Oeq ==> Oeq
as U2Rp_eq_compat.
Save.

Add Morphism U2Rp with signature Ole ==> Ole
as U2Rp_le_compat.
Save.

Hint Resolve U2Rp_eq_compat U2Rp_le_compat.

Lemma eq_U2Rp_intro : forall (r:Rp) (x:U),
floor r = O -> decimal r == x -> r == U2Rp x.
Hint Resolve eq_U2Rp_intro.

Lemma U2Rp_eq_intro : forall (r:Rp) (x:U),
floor r = O -> decimal r == x -> U2Rp x == r.
Hint Resolve U2Rp_eq_intro.

Lemma U2Rp_le_simpl : forall x y : U, U2Rp x <= U2Rp y -> x <= y.

Lemma U2Rp_eq_simpl : forall x y : U, U2Rp x == U2Rp y -> x == y.

Hint Immediate U2Rp_le_simpl U2Rp_eq_simpl.

Add Morphism U2Rp with signature Olt ==> Olt
as U2Rp_lt_compat.
Save.
Hint Resolve U2Rp_lt_compat.

Lemma U2Rp_lt_simpl : forall x y : U, U2Rp x < U2Rp y -> x < y.
Hint Immediate U2Rp_lt_simpl.

Lemma U2Rp_eq_rewrite : forall x y : U, (x == y) <-> U2Rp x == U2Rp y.

Lemma U2Rp_le_rewrite : forall x y : U, (x <= y) <-> U2Rp x <= U2Rp y.

Lemma U2Rp_lt_rewrite : forall x y : U, (x < y) <-> U2Rp x < U2Rp y.

Add Morphism N2Rp with signature le ==> Ole
as N2Rp_le_compat.
Save.
Hint Resolve N2Rp_le_compat.

Add Morphism N2Rp with signature eq ==> Oeq
as N2Rp_eq_compat.
Save.
Hint Resolve N2Rp_eq_compat.

Lemma N2Rp_eq_simpl : forall a b, N2Rp a == N2Rp b -> a = b.
Hint Immediate N2Rp_eq_simpl.

Lemma N2Rp_eq_rewrite : forall a b, a = b <-> N2Rp a == N2Rp b.

Lemma decimal_0_eq_floor : forall x:Rp, decimal x == 0 -> x == floor x.
Hint Resolve decimal_0_eq_floor.

Lemma floor_decimal_R0 : forall x:Rp, floor x = O -> decimal x == 0%U -> x == R0.
Hint Resolve floor_decimal_R0.

Add Morphism N2Rp with signature lt ==> Olt
as N2Rp_lt_compat.
Save.
Hint Resolve N2Rp_lt_compat.

Lemma N2Rp_le_simpl : forall (x y : nat), N2Rp x <= N2Rp y -> (x<=y)%nat.
Hint Immediate N2Rp_le_simpl.

Lemma N2Rp_le_rewrite : forall (x y : nat), (x<=y)%nat <-> N2Rp x <= N2Rp y.

Lemma N2Rp_lt_simpl : forall (x y : nat), N2Rp x < N2Rp y -> (x<y)%nat.
Hint Immediate N2Rp_lt_simpl.

Lemma N2Rp_lt_rewrite : forall (x y : nat), (x<y)%nat <-> N2Rp x < N2Rp y.

Lemma Rple_eq_floor_le_decimal
: forall r1 r2, r1 <= r2 -> (floor r1 = floor r2) -> decimal r1 <= decimal r2.

Hint Immediate Rple_eq_floor_le_decimal.

Lemma Rple_N2Rp_mkRp : forall n m x, (n<=m)%nat -> N2Rp n <= mkRp m x.
Hint Resolve Rple_N2Rp_mkRp.

Lemma U2Rp1_R1 : U2Rp 1 == R1.
Hint Resolve U2Rp1_R1.

Lemma U2Rp_le_R1 : forall x:U, U2Rp x <= R1.
Hint Resolve U2Rp_le_R1.

Basic relations are classical

Lemma le_class : forall x y:nat, class (x <= y)%nat.

Lemma eq_nat_class : forall x y:nat, class (x = y).

Hint Resolve le_class eq_nat_class.

Lemma Rple_class : forall x y: Rp, class (x <= y).
Hint Resolve Rple_class.

Lemma Rple_total : forall x y : Rp, orc (x <= y) (y <= x).
Hint Resolve Rple_total.

Lemma Rpeq_class : forall x y:Rp, class (x == y).
Hint Resolve Rpeq_class.

Lemma Rple_zero : forall (x:Rp), R0 <= x.
Hint Resolve Rple_zero.

Lemma Rple_dec : forall x y: Rp, {x <= y} + { ~ x <= y}.

Lemma Rpeq_dec : forall x y: Rp, {x == y} + { ~ x == y}.

Lemma Rple_lt_eq_dec : forall x y: Rp, x <= y -> {x < y} + {x == y}.

Lemma Rple_lt_dec : forall x y: Rp, {x <= y} + {y < x}.

Hint Resolve Rple_dec Rpeq_dec Rple_lt_eq_dec Rple_lt_dec.

Lemma Rp_lt_eq_lt_dec : forall x y:Rp, {x < y} + {x==y} + {y < x}.
Hint Resolve Rp_lt_eq_lt_dec.

Lemma Rplt_neq_zero: forall x : Rp, ~ R0 == x -> R0 < x.

Lemma notRple_lt: forall x y : Rp, ~ y <= x -> x < y.
Hint Immediate notRple_lt.

Lemma notRplt_le: forall x y : Rp, ~ x < y -> y <= x.
Hint Immediate notRplt_le.

Lemma floor_le : forall x, N2Rp (floor x) <= x.
Hint Resolve floor_le.

Lemma floor_gt_S : forall x, x < S (floor x).
Hint Resolve floor_gt_S.

Lemma Rplt_nat_floor : forall (x : Rp) (n:nat), x < n -> (floor x < n)%nat.
Hint Resolve Rplt_nat_floor.

Lemma Rplt1_floor : forall x:Rp, x < R1 -> floor x = O.
Hint Resolve Rplt1_floor.

Lemma Rplt1_decimal : forall x:Rp, x < R1 -> x == decimal x.
Hint Resolve Rplt1_decimal.

Lemma Rplt_nat_floor_le : forall (x : Rp) (n:nat), N2Rp n <= x -> (n <= floor x)%nat.
Hint Resolve Rplt_nat_floor_le.

Lemma Rplt_nat_floor_lt : forall (x : Rp) (n:nat), N2Rp (S n) < x -> (n < floor x)%nat.
Hint Resolve Rplt_nat_floor_lt.

Definition and basic properties

Definition Rpplus r1 r2 :=
if isle ([1-](decimal r2)) (decimal r1) then mkRp (S (floor r1 + floor r2)) (decimal r1 & decimal r2)
else mkRp (floor r1 + floor r2)%nat (decimal r1 + decimal r2).

Infix "+" := Rpplus : Rp_scope.

Lemma Rpplus_simpl : forall r1 r2 : Rp,
r1 + r2 = if isle ([1-](decimal r2)) (decimal r1) then mkRp (S (floor r1 + floor r2)) (decimal r1 & decimal r2)
else mkRp (floor r1 + floor r2)%nat (decimal r1 + decimal r2).

Lemma Rpplus_rec : forall (r1 r2:Rp) (P : Rp -> Type),
(decimal r1 < [1-]decimal r2 -> P (mkRp (floor r1 + floor r2) (decimal r1 + decimal r2)))
-> ([1-]decimal r2 <= decimal r1 -> P (mkRp (S (floor r1 + floor r2)) (decimal r1 & decimal r2)))
-> P (r1 + r2).

Lemma Rpplus_simpl_ok : forall (r1 r2:Rp),
decimal r1 < [1-]decimal r2 -> r1 + r2 = mkRp (floor r1 + floor r2) (decimal r1 + decimal r2).

Lemma Rpplus_simpl_over : forall (r1 r2:Rp),
[1-]decimal r2 <= decimal r1 -> r1 + r2 = mkRp (1 + (floor r1 + floor r2)) (decimal r1 & decimal r2).

Lemma Rpplus_simpl_ok2 : forall (r1 r2:Rp),
decimal r1 <= [1-]decimal r2 -> r1 + r2 == mkRp (floor r1 + floor r2) (decimal r1 + decimal r2).

Lemma floor_Rpplus_simpl_ok : forall (r1 r2:Rp),
decimal r1 < [1-]decimal r2 -> floor (r1 + r2) = (floor r1 + floor r2)%nat.

Lemma floor_Rpplus_simpl_over : forall (r1 r2:Rp),
[1-]decimal r2 <= decimal r1 -> floor (r1 + r2) = (1 + (floor r1 + floor r2))%nat.

Lemma decimal_Rpplus_simpl_ok : forall (r1 r2:Rp),
decimal r1 < [1-]decimal r2 -> decimal (r1 + r2) == (decimal r1 + decimal r2)%U.

Lemma decimal_Rpplus_simpl_over : forall (r1 r2:Rp),
[1-]decimal r2 <= decimal r1 -> decimal (r1 + r2) = (decimal r1 & decimal r2)%U.

Lemma Rpdiff_0_1 : ~ (R0 == R1).
Hint Resolve Rpdiff_0_1.

Lemma Rpplus_sym : forall r1 r2 : Rp, r1 + r2 == r2 + r1.
Hint Resolve Rpplus_sym.

Lemma Rpplus_zero_left : forall r : Rp, R0 + r == r.
Hint Resolve Rpplus_zero_left.

Lemma Rpplus_zero_right : forall r : Rp, r + R0 == r.
Hint Resolve Rpplus_zero_right.

Lemma Rpplus_assoc : forall r1 r2 r3 : Rp, r1 + (r2 + r3) == (r1 + r2) + r3.
Hint Resolve Rpplus_assoc.

Link with operations on nat and U

Lemma N2Rp_plus : forall n m : nat, N2Rp n + N2Rp m == N2Rp (n+m)%nat.

Lemma N2Rp_S_plus_1 : forall n, N2Rp (S n) == R1 + n.
Hint Resolve N2Rp_plus N2Rp_S_plus_1.

Lemma N2Rp_plus_left : forall (n:nat) (r:Rp),
N2Rp n + r == mkRp (n + floor r)%nat (decimal r).

Lemma U2Rp_plus_0_1 : forall x y:U, x == 0 -> y == 1 -> U2Rp x + U2Rp y == U2Rp 1.
Hint Immediate U2Rp_plus_0_1.

Lemma decimal_le : forall x:U, decimal x <= x.
Hint Resolve decimal_le.

Lemma Uinv_decimal : forall x y : U, x <= [1-]y -> decimal x <= [1-]decimal y.
Hint Resolve Uinv_decimal.

Lemma U2Rp_plus_le : forall x y : U, x <= [1-]y ->
U2Rp x + U2Rp y == U2Rp (x+y).
Hint Resolve U2Rp_plus_le.

Lemma U2Rp_plus_ge : forall x y : U, [1-]y <= x ->
U2Rp x + U2Rp y == mkRp 1%nat (x&y).

Lemma Rpplus_floor_decimal : forall r:Rp, r == N2Rp (floor r) + U2Rp (decimal r).

Lemma Rpplus_NU2Rp : forall n x, N2Rp n + U2Rp x == mkRp n x.
Hint Resolve N2Rp_plus N2Rp_plus_left U2Rp_plus_ge Rpplus_floor_decimal
Rpplus_NU2Rp.

Lemma U2Rp_ge_R1 : forall x y:U, [1-]x <= y -> R1 <= U2Rp x + U2Rp y.
Hint Resolve U2Rp_ge_R1.

Lemma Rple1_U2Rp : forall x:Rp, x <= R1 -> {y : U | x == U2Rp y}.

Lemma U2Rp_plus : forall x y, U2Rp (x+y) <= x+y.

Lemma Rple_floor : forall x : Rp, N2Rp (floor x) <= x.
Hint Resolve Rple_floor.

Lemma Rple_S_N2Rp : forall (r:Rp) (n:nat), r <= n -> r <= S n.
Hint Immediate Rple_S_N2Rp.

Lemma Rplt_S_N2Rp: forall (r:Rp) (n:nat), r <= n -> r < S n.
Hint Immediate Rplt_S_N2Rp.

Monotonicity ans stability

Instance Rpplus_mon_right : forall r, monotonic (Rpplus r).
Save.
Hint Resolve Rpplus_mon_right.

Instance Rpplus_monotonic2 : monotonic2 Rpplus.
Save.
Hint Resolve Rpplus_monotonic2.

Add Morphism Rpplus with signature Oeq ==> Oeq ==> Oeq
as Rpplus_eq_compat.
Save.

Add Morphism Rpplus with signature Ole ==> Ole ==> Ole
as Rpplus_le_compat.
Save.
Hint Immediate Rpplus_eq_compat Rpplus_le_compat.

Lemma Rpplus_le_compat_left
: forall x y z : Rp, x <= y -> x + z <= y + z.

Lemma Rpplus_le_compat_right
: forall x y z : Rp, y <= z -> x + y <= x + z.
Hint Resolve Rpplus_le_compat_left Rpplus_le_compat_right.

Lemma Rpplus_eq_compat_left
: forall x y z : Rp, x == y -> x + z == y + z.

Lemma Rpplus_eq_compat_right
: forall x y z : Rp, y == z -> x + y == x + z.
Hint Resolve Rpplus_eq_compat_left Rpplus_eq_compat_right.

Instance Rpplus_mon2 : monotonic2 Rpplus.
Save.

Definition RpPlus : Rp -m> Rp -m> Rp := mon2 Rpplus.

Lemma Rple_plus_right : forall r1 r2, r1 <= r1 + r2.
Hint Resolve Rple_plus_right.

Lemma Rple_plus_left : forall r1 r2, r2 <= r1 + r2.
Hint Resolve Rple_plus_left.

Lemma Rpplus_perm3: forall x y z : Rp, x + (y + z) == z + (x + y).

Lemma Rpplus_perm2: forall x y z : Rp, x + (y + z) == y + (x + z).
Hint Resolve Rpplus_perm2 Rpplus_perm3.

Substraction Rpminus

Definition and basic properties

Definition Rpminus r1 r2 :=
match nat_compare (floor r1) (floor r2) with
Lt => R0
| Eq => mkRp 0 (decimal r1 - decimal r2)
| Gt => if isle (decimal r2) (decimal r1)
then mkRp (floor r1 - floor r2) (decimal r1 - decimal r2)
else mkRp (pred (floor r1 - floor r2)) (decimal r1 + [1-]decimal r2)
end.

Infix "-" := Rpminus : Rp_scope.

Lemma Rpminus_rec : forall (r1 r2:Rp) (P : Rp -> Type),
( (floor r1 < floor r2)%nat -> P R0 )
-> ( floor r1 = floor r2 -> P (mkRp 0 (decimal r1 - decimal r2)))
-> ( (floor r2 < floor r1)%nat -> decimal r2 <= decimal r1
-> P (mkRp (floor r1 - floor r2) (decimal r1 - decimal r2)))
-> ( (floor r2 < floor r1)%nat -> decimal r1 < decimal r2
-> P (mkRp (pred (floor r1 - floor r2)) (decimal r1 + [1-]decimal r2)))
-> P (r1 - r2).

Useful lemma
Lemma decimal_minus_lt1 : forall (x:Rp) (y:U), ((decimal x) - y < 1)%U.
Hint Resolve decimal_minus_lt1.

Lemma Rpminus_simpl_lt : forall (r1 r2:Rp),
(floor r1 < floor r2)%nat -> r1 - r2 = R0.

Lemma Rpminus_simpl_eq : forall (r1 r2:Rp),
floor r1 = floor r2 -> r1 - r2 = U2Rp (decimal r1 - decimal r2).

Lemma Rpminus_simpl_gt : forall (r1 r2:Rp),
decimal r2 <= decimal r1 -> (floor r2 < floor r1)%nat ->
r1 - r2 = mkRp (floor r1 - floor r2) (decimal r1 - decimal r2).

Lemma Rpminus_simpl_gt2 : forall (r1 r2:Rp),
decimal r2 <= decimal r1 -> (floor r2 <= floor r1)%nat ->
r1 - r2 = mkRp (floor r1 - floor r2) (decimal r1 - decimal r2).

Lemma Rpminus_simpl_gtc : forall (r1 r2:Rp),
decimal r1 < decimal r2 -> (floor r2 < floor r1)%nat ->
r1 - r2 = mkRp (pred (floor r1 - floor r2)) (decimal r1 + [1-]decimal r2).

Lemma Rpminus_simpl_gtc2 : forall (r1 r2:Rp),
decimal r1 <= decimal r2 -> (floor r2 < floor r1)%nat ->
r1 - r2 == mkRp (pred (floor r1 - floor r2)) (decimal r1 + [1-]decimal r2).

Hint Resolve Rpminus_simpl_lt Rpminus_simpl_eq Rpminus_simpl_gt Rpminus_simpl_gt2 Rpminus_simpl_gtc Rpminus_simpl_gtc2.

Algebraic properties of Rpminus

Lemma Rpminus_le_zero: forall r1 r2 : Rp, r1 <= r2 -> (r1 - r2) == R0.

Lemma Rpminus_zero_right: forall x : Rp, x - R0 == x.
Hint Resolve Rpminus_zero_right Rpminus_le_zero.

Monotonicity

Lemma Rpminus_le_compat_left: forall x y z : Rp, x <= y -> (x - z) <= (y - z).
Hint Resolve Rpminus_le_compat_left.

Lemma Rpminus_eq_compat_left:
forall x y z : Rp, x == y -> (x - z) == (y - z).

Lemma Rpminus_le_compat_right: forall x y z : Rp, y <= z -> (x - z) <= (x - y).
Hint Resolve Rpminus_le_compat_right.

Lemma Rpminus_eq_compat_right:
forall x y z : Rp, y == z -> (x - y) == (x - z).

Hint Resolve Rpminus_eq_compat_left Rpminus_eq_compat_right.

Lemma Rpminus_eq_compat:
forall x y z t : Rp, x == y -> z == t -> (x - z) == (y - t).

Lemma Rpminus_le_compat:
forall x y z t : Rp, x <= y -> t <= z -> (x - z) <= (y - t).

Hint Immediate Rpminus_eq_compat Rpminus_le_compat.

Add Morphism Rpminus with signature Oeq ==> Oeq ==> Oeq
as Rpminus_eq_morphism.
Save.

Add Morphism Rpminus with signature Ole ==> Ole --> Ole
as Rpminus_le_morphism.
Save.

Instance Rpminus_mon2 : monotonic2 (o2:=Iord Rp) Rpminus.
Save.
Hint Resolve Rpminus_mon2.

Definition RpMinus : Rp -m> Rp --m> Rp := mon2 (o2:=Iord Rp) Rpminus.

Lemma U2Rp_minus : forall x y:U, U2Rp x - U2Rp y == U2Rp (x - y).

Lemma N2Rp_minus : forall x y:nat, N2Rp x - N2Rp y == N2Rp (x - y).

More algebraic properties

Lemma Rpminus_zero_left: forall r : Rp, (R0 - r) == R0.
Hint Resolve Rpminus_zero_left.

Lemma Rpminus_eq: forall r : Rp, (r - r) == R0.
Hint Resolve Rpminus_eq.

Lemma Rpplus_minus_simpl_right : forall r1 r2 : Rp, (r1 + r2 - r2) == r1.
Hint Resolve Rpplus_minus_simpl_right.

Lemma Rpplus_minus_simpl_left : forall r1 r2 : Rp, (r1 + r2 - r1) == r2.
Hint Resolve Rpplus_minus_simpl_left.

Lemma Rpminus_plus_simpl : forall r1 r2 : Rp, r2 <= r1 -> (r1 - r2 + r2) == r1.
Hint Resolve Rpminus_plus_simpl.

Lemma Rpminus_plus_simpl_le : forall r1 r2 : Rp, r1 <= r1 - r2 + r2.
Hint Resolve Rpminus_plus_simpl_le.

Lemma Rpplus_le_simpl_right:
forall x y z : Rp, (x + z) <= (y + z) -> x <= y.

Lemma Rpplus_le_simpl_left:
forall x y z : Rp, (x + y) <= (x + z) -> y <= z.

Lemma Rpplus_eq_simpl_right:
forall x y z : Rp, (x + z) == (y + z) -> x == y.

Lemma Rpplus_eq_simpl_left:
forall x y z : Rp, (x + y) == (x + z) -> y == z.

Lemma Rpplus_eq_perm_left: forall x y z : Rp, x == y + z -> x - y == z.
Hint Immediate Rpplus_eq_perm_left.

Lemma Rpplus_eq_perm_right: forall x y z : Rp, x + z == y -> x == y - z.
Hint Immediate Rpplus_eq_perm_right.

Lemma Rpplus_le_perm_left: forall x y z : Rp, x <= y + z -> x - y <= z.
Hint Immediate Rpplus_le_perm_left.

Lemma Rpplus_le_perm_right: forall x y z : Rp, x + z <= y -> x <= y - z.
Hint Immediate Rpplus_le_perm_right.

Lemma Rpminus_plus_perm_right:
forall x y z : Rp, y <= x -> y <= z -> x - y + z == x + (z - y).
Hint Resolve Rpminus_plus_perm_right.

Lemma Rpminus_plus_perm : forall x y z : Rp, y <= x -> x - y + z == (x + z) - y.
Hint Resolve Rpminus_plus_perm.

Lemma Rpminus_assoc_right : forall x y z, y <= x -> z <= y -> x - (y - z) == x - y + z.
Hint Resolve Rpminus_assoc_right.

Lemma Rpplus_minus_assoc : forall x y z, z <= y -> x + y - z == x + (y - z).
Hint Resolve Rpplus_minus_assoc.

Lemma Rpminus_zero_le: forall r1 r2 : Rp, (r1 - r2) == R0 -> r1 <= r2.
Hint Immediate Rpminus_zero_le.

Lemma U2Rp_Uesp : forall x y, [1-]x <= y -> U2Rp (x & y) == U2Rp x + U2Rp y - R1.
Hint Resolve U2Rp_Uesp.

Lemma Rpminus_le_perm_right:
forall x y z : Rp, z <= y -> x <= y - z -> x + z <= y.
Hint Resolve Rpminus_le_perm_right.

Lemma Rpminus_le_perm_left:
forall x y z : Rp, x - y <= z -> x <= z + y.
Hint Resolve Rpminus_le_perm_left.

Lemma Rpminus_eq_perm_right:
forall x y z : Rp, z <= y -> x == y - z -> x + z == y.
Hint Resolve Rpminus_eq_perm_right.

Lemma Rpminus_eq_perm_left:
forall x y z : Rp, y <= x -> x - y == z -> x == z + y.
Hint Resolve Rpminus_eq_perm_left.

Lemma Rpplus_lt_compat_left : forall x y z : Rp, x < y -> x + z < y + z.

Lemma Rpplus_lt_compat_right : forall x y z : Rp, y < z -> x + y < x + z.

Lemma U2Rp_Uinv : forall x, U2Rp ([1-]x) == R1 - U2Rp x.
Hint Resolve U2Rp_Uinv.

Lemma Rpplus_Uinv_le : forall x y : U, x + y <= R1 -> x <= [1-]y.
Hint Immediate Rpplus_Uinv_le.

Lemma Rpminus_lt_compat_right:
forall x y z : Rp, z <= x -> y < z -> x - z < x - y.
Hint Resolve Rpminus_lt_compat_right.

Lemma Rpminus_lt_compat_left: forall x y z : Rp, z <= x -> x < y -> x - z < y - z.
Hint Resolve Rpminus_lt_compat_left.

Lemma Rpminus_lt_0 : forall x y : Rp, x < y -> R0 < y - x.
Hint Immediate Rpminus_lt_0.

Lemma Rpminus_Sn_R1 : forall (n:nat), N2Rp (S n) - R1 == n.
Hint Resolve Rpminus_Sn_R1.

Lemma Rpminus_Sn_1 : forall (n:nat), N2Rp (S n) - 1%U == n.
Hint Resolve Rpminus_Sn_1.

Lemma Rpminus_assoc_left : forall x y z : Rp, x - y - z == x - (y + z).
Hint Resolve Rpminus_assoc_left.

Lemma Rpminus_perm : forall x y z : Rp, x - y - z == x - z - y.
Hint Resolve Rpminus_perm.

Multiplications Rpmult

Multiplication by an integer NRpmult

Fixpoint NRpmult p r {struct p} : Rp :=
match p with O => R0
| S n => r + (NRpmult n r)
end.

Infix "*/" := NRpmult (at level 60) : Rp_scope.

Lemma NRpmult_0 : forall r : Rp, 0 */ r = R0.

Lemma NRpmult_S : forall (n:nat) (r : Rp), (S n) */ r = r + (n */ r).
Hint Resolve NRpmult_0 NRpmult_S.

Lemma NRpmult_zero : forall n : nat, n */ R0 == R0.

Lemma NRpmult_1: forall x : Rp, (1 */ x) == x.
Hint Resolve NRpmult_1.

Lemma plus_NRpmult_distr:
forall (n m : nat) (r : Rp), (n + m */ r) == ((n */ r) + (m */ r)).

Lemma NRpmult_plus_distr:
forall (n : nat) (r1 r2 : Rp), (n */ r1 + r2) == ((n */ r1) + (n */ r2)).

Hint Resolve plus_NRpmult_distr NRpmult_plus_distr.

Lemma NRpmult_le_compat_right :
forall (n : nat) (r1 r2 : Rp), r1 <= r2 -> (n */ r1) <= (n */ r2).
Hint Resolve NRpmult_le_compat_right.

Lemma NRpmult_le_compat_left:
forall (n m : nat) (r : Rp), (n <= m)%nat -> (n */ r) <= (m */ r).
Hint Resolve NRpmult_le_compat_left.

Add Morphism NRpmult with signature le ==> Ole ==> Ole
as NRpmult_le_compat.
Save.
Hint Immediate NRpmult_le_compat.

Add Morphism NRpmult with signature eq ==> Oeq ==> Oeq
as NRpmult_eq_compat.
Save.
Hint Immediate NRpmult_eq_compat.

Lemma NRpmult_mult_assoc: forall (n m : nat) (r:Rp), n * m */ r == n */ (m */ r).
Hint Resolve NRpmult_mult_assoc.

Lemma NRpmult_N2Rp : forall n m, n */ N2Rp m == N2Rp (n*m).
Hint Resolve NRpmult_N2Rp.

Lemma NRpmult_floor_decimal : forall n (r:Rp), n */ r == N2Rp (n * floor r) + (n */ U2Rp (decimal r)).
Hint Resolve NRpmult_floor_decimal.

Lemma NRpmult_minus_distr : forall n r1 r2, n */ (r1 - r2) == (n */ r1) - (n */ r2).
Hint Resolve NRpmult_minus_distr.

Lemma NRpmult_R1 : forall n, n */ R1 == N2Rp n.
Hint Resolve NRpmult_R1.

Multiplication between positive reals

Definition Rpmult (r1 r2 : Rp) : Rp :=
(floor r1 */ r2) + (floor r2 */ U2Rp (decimal r1)) + U2Rp (decimal r1 * decimal r2)%U.

Infix "*" := Rpmult : Rp_scope.

Lemma Rpmult_zero_left: forall r : Rp, R0 * r == R0.
Hint Resolve Rpmult_zero_left.

Lemma Rpmult_sym : forall r1 r2 : Rp, r1 * r2 == r2 * r1.
Hint Resolve Rpmult_sym.

Lemma Rpmult_zero_right: forall r : Rp, r * R0 == R0.
Hint Resolve Rpmult_zero_right.

Lemma NRpmult_mult : forall n r, N2Rp n * r == n */ r.
Hint Resolve NRpmult_mult.

Lemma Rpmult_one_left: forall x : Rp, (R1 * x) == x.
Hint Resolve Rpmult_one_left.

Lemma NRp_Nmult_eq : forall n (x:U), (n */ x < 1)%U -> (n */ x)%Rp == (n */ x)%U.
Hint Resolve NRp_Nmult_eq.

Lemma NRp_Nmult_eq_le1
: forall n (x:U), (n */ x <= R1)%Rp -> (n */ x)%Rp == (n */ x)%U.

Lemma U2Rp_Nmult_NRpmult : forall n x, U2Rp (n */ x) <= n */ x.

Lemma U2Rp_Nmult_le : forall n x, U2Rp (n */ x) <= n * x.
Hint Resolve U2Rp_Nmult_NRpmult U2Rp_Nmult_le.

Lemma N2Rp_mult : forall x y, N2Rp (x * y) == N2Rp x * N2Rp y.
Hint Resolve N2Rp_mult.

Lemma U2Rp_mult : forall x y, U2Rp (x * y) == U2Rp x * U2Rp y.
Hint Resolve U2Rp_mult.

Lemma U2Rp_esp_mult
: forall x y z, [1-]x <= y -> U2Rp ((x & y) * z) == U2Rp (x * z) + U2Rp (y * z) - U2Rp z.
Hint Resolve U2Rp_esp_mult.

Instance Rpmult_mon_right : forall x, monotonic (Rpmult x).
Save.
Hint Resolve Rpmult_mon_right.

Instance Rpmult_monotonic2 : monotonic2 Rpmult.
Save.
Hint Resolve Rpmult_monotonic2.

Instance Rpmult_stable2 : stable2 Rpmult.
Save.
Hint Resolve Rpmult_stable2.

Add Morphism Rpmult with signature Ole ==> Ole ==> Ole
as Rpmult_le_compat.
Save.
Hint Immediate Rpmult_le_compat.

Add Morphism Rpmult with signature Oeq ==> Oeq ==> Oeq
as Rpmult_eq_compat.
Save.
Hint Immediate Rpmult_eq_compat.

Lemma Rpmult_le_compat_left : forall x y z : Rp, x <= y -> x * z <= y * z.

Lemma Rpmult_le_compat_right : forall x y z : Rp, y <= z -> x * y <= x * z.

Lemma Rpmult_eq_compat_left : forall x y z : Rp, x == y -> x * z == y * z.

Lemma Rpmult_eq_compat_right : forall x y z : Rp, y == z -> x * y == x * z.
Hint Resolve Rpmult_le_compat_left Rpmult_le_compat_right Rpmult_eq_compat_left Rpmult_eq_compat_right.

Instance Rpmult_mon2 : monotonic2 Rpmult.
Save.

Definition RpMult : Rp -m> Rp -m> Rp := mon2 Rpmult.

Lemma Rpdistr_plus_right
: forall r1 r2 r3 : Rp, (r1 + r2) * r3 == r1 * r3 + r2 * r3.

Lemma Rpdistr_plus_left : forall r1 r2 r3 : Rp, r1 * (r2 + r3) == r1 * r2 + r1 * r3.

Hint Resolve Rpdistr_plus_right Rpdistr_plus_left.

Lemma Rpmult_NRpmult_perm : forall n x y, x * (n */ y) == n */ (x * y).
Hint Resolve Rpmult_NRpmult_perm.

Lemma Rpmult_decomp : forall r1 r2 : Rp,
r1 * r2 == (N2Rp (floor r1 * floor r2))
+ (floor r1 */ U2Rp (decimal r2)) + (floor r2 */ U2Rp (decimal r1))
+ U2Rp (decimal r1 * decimal r2).

Lemma Rpmult2_decomp : forall r1 r2 r3: Rp,
r1 * (r2 * r3) == (N2Rp (floor r1 * floor r2 * floor r3))
+ ((floor r1 * floor r2) */ U2Rp (decimal r3))
+ ((floor r1 * floor r3) */ U2Rp (decimal r2))
+ ((floor r2 * floor r3) */ U2Rp (decimal r1))
+ (floor r1 */ U2Rp (decimal r2 * decimal r3))
+ (floor r2 */ U2Rp (decimal r1 * decimal r3))
+ (floor r3 */ U2Rp (decimal r1 * decimal r2))
+ U2Rp (decimal r1 * decimal r2 * decimal r3).

Lemma Rpmult_assoc : forall r1 r2 r3 : Rp, r1 * (r2 * r3) == r1 * r2 * r3.
Hint Resolve Rpmult_assoc.

Lemma Rpmult_one_right: forall x : Rp, (x * R1) == x.
Hint Resolve Rpmult_one_right.

Lemma Rpmult_not0_left : forall x y : Rp, ~ R0 == x * y -> ~ R0 == x.
Hint Resolve Rpmult_not0_left.

Lemma Rpmult_not0_right : forall x y : Rp, ~ R0 == x * y -> ~ R0 == y.
Hint Resolve Rpmult_not0_right.

Lemma U2Rp_0_simpl : forall x : U, R0 == U2Rp x -> 0 == x.
Hint Immediate U2Rp_0_simpl.

Lemma U2Rp_not_0 : forall x : U, ~ R0 == x -> ~ 0 == x.
Hint Resolve U2Rp_not_0.

Lemma U2Rp_not_0_equiv : forall x : U, ~ R0 == x <-> ~ 0 == x.

Lemma U2Rp_lt_0 : forall x:U, R0 < x -> 0 < x.
Hint Resolve U2Rp_lt_0.

Lemma U2Rp_0_lt : forall x:U, 0 < x -> R0 < x.
Hint Resolve U2Rp_0_lt.

Lemma Rpplus_lt_simpl_left: forall x y z : Rp, x + z < y + z -> x < y.

Lemma Rpplus_lt_simpl_right: forall x y z : Rp, x + y < x + z -> y < z.

Lemma plus_lt_1_decimal : forall x y:Rp, x + y < R1 -> decimal x < [1-] decimal y.
Hint Immediate plus_lt_1_decimal.

Lemma plus_lt_1_decimal_plus : forall x y, x + y < R1 -> decimal (x+y) == (decimal x + decimal y)%U.
Hint Immediate plus_lt_1_decimal_plus.

Lemma Rpplus_0_simpl_left : forall x y : Rp, R0 == x + y -> R0 == x.

Lemma Rpplus_0_simpl_right : forall x y : Rp, R0 == x + y -> R0 == y.

Lemma Rpplus_0_simpl : forall x y : Rp, R0 == x + y -> R0 == x /\ R0 == y.

Lemma NRpmult_0_simpl : forall (n:nat) (x : Rp), R0 == n */ x -> n = O \/ R0 == x.

Lemma Rpmult_0_simpl : forall x y : Rp, R0 == x * y -> R0 == x \/ R0 == y.

Lemma Rpmult_not_0 : forall x y : Rp, ~ R0 == x -> ~ R0 == y -> ~ R0 == x * y.
Hint Resolve Rpmult_not_0.

Lemma Rpdistr_minus_right : forall r1 r2 r3 : Rp, (r1 - r2) * r3 == r1 * r3 - r2 * r3.
Hint Resolve Rpdistr_minus_right.

Lemma Rpdistr_minus_left : forall r1 r2 r3 : Rp, r1 * (r2 - r3) == r1 * r2 - r1 * r3.
Hint Resolve Rpdistr_minus_left.

Lemma U2Rp_mult_le_left : forall (x:U) (y:Rp), x * y <= y.
Hint Resolve U2Rp_mult_le_left.

Lemma U2Rp_mult_le_right : forall (x:Rp) (y:U), x * y <= x.
Hint Resolve U2Rp_mult_le_right.

Division Rpdiv

Inverse U1div of elements of U

A stronger formulation of the Archimedian property to be able to compute n

Hypothesis archimedian2: forall x : U, ~ 0 == x -> exists n : nat, [1/]1+n <= x.

Require Export Markov.

Definition 1/x for x in U

Section U1div_def.
Variable x : U.
Hypothesis x_not0 : ~ 0 == x.

Definition P (n:nat) := ([1-](n */ x) < x)%U.

Lemma Pdec : dec P.

Definition DP : Dec := mk_Dec Pdec.

Lemma Pacc : exists n : nat, P n.

Let n := minimize DP Pacc.

Lemma Olt_Uinv_Nmult_nx_x : [1-](n */ x) < x.
Hint Resolve Olt_Uinv_Nmult_nx_x.

Lemma Nmult_nx_1 : (n */ x) <= R1.
Hint Resolve Nmult_nx_1.

Definition U1div0 : Rp := mkRp n (([1-] (n */ x))/x).

Lemma Olt_frac_U1div0_1 : (([1-] (n */ x))/x) < 1.
Hint Resolve Olt_frac_U1div0_1.

Lemma floor_U1div0 : floor U1div0 = n.

Lemma decimal_U1div0 : decimal U1div0 = ([1-] (n */ x)) /x.

Lemma U1div0_left : U2Rp x * U1div0 == R1.

Lemma U1div0_right : U1div0 * U2Rp x == R1.

End U1div_def.
Hint Resolve U1div0_right U1div0_left.

Definition U1div (x:U) := match iseq_dec 0 x with
left _ => R0 | right H => U1div0 x H end.

Lemma U1div_left : forall x, ~ 0 == x -> U2Rp x * U1div x == R1.
Hint Resolve U1div_left.

Lemma U1div_right : forall x, ~ 0 == x -> U1div x * U2Rp x == R1.
Hint Resolve U1div_right.

Lemma U1div_zero : forall x, 0 == x -> U1div x == R0.
Hint Resolve U1div_zero.

Lemma Unth_mult_le1 : forall x:Rp, U2Rp ([1/]1+(floor x)) * x <= R1.
Hint Resolve Unth_mult_le1.

Non-zero elements

Class notz (x:Rp) := notz_def : ~ R0 == x.

Lemma notz_le_compat : forall x y, notz x -> x <= y -> notz y.

Add Morphism notz with signature Ole ++> Basics.impl as notz_le_compat_morph.
Save.

Lemma notz_eq_compat : forall x y, notz x -> x == y -> notz y.

Add Morphism notz with signature Oeq ==> Basics.impl as notz_eq_compat_morph.
Save.

Instance notz_mult : forall x y, notz x -> notz y -> notz (x * y).
Save.
Hint Resolve notz_mult.

Instance notz_plus_left : forall x y, notz x -> notz (x + y).
Save.
Hint Immediate notz_plus_left.

Instance notz_plus_right : forall x y, notz y -> notz (x + y).
Save.
Hint Immediate notz_plus_right.

Lemma notz_mult_inv_left : forall x y, notz (x * y) -> notz x.

Lemma notz_mult_inv_right : forall x y, notz (x * y) -> notz y.

Instance notz_1 : notz R1.
Save.
Hint Resolve notz_1.

Inverse of elements in Rp Rp1div

Section Rp1div_def.
Variable x : Rp.

Let a := U2Rp ([1/]1+(floor x)) * x.

Lemma a_le_1 : a <= R1.

Lemma a_not_0 : notz x -> notz a.

Lemma a_is_0 : R0 == x -> R0 == a.

Lemma U2Rp_eq_not_0 : notz x -> forall y, a == U2Rp y -> ~ 0 == y.

Lemma U2Rp_eq_is_0 : R0 == x -> forall y, a == U2Rp y -> 0 == y.

Definition Rp1div : Rp :=
let (y,H) := Rple1_U2Rp a a_le_1 in U2Rp ([1/]1+(floor x)) * U1div y.

Lemma Rp1div_left : notz x -> x * Rp1div == R1.
Hint Resolve Rp1div_left.

Lemma Rp1div_right : notz x -> Rp1div * x == R1.
Hint Resolve Rp1div_right.

Lemma Rp1div_zero : R0 == x -> Rp1div == R0.

End Rp1div_def.

Notation "[1/] x" := (Rp1div x) (at level 35, right associativity) : Rp_scope.
Hint Resolve Rp1div_left Rp1div_right Rp1div_zero.

Lemma Rp1div_0 : [1/]R0 == R0.
Hint Resolve Rp1div_0.

Instance notz_1div : forall x {nx:notz x}, notz ([1/]x).
Save.
Hint Resolve notz_1div.

Lemma notz_dec : forall x, {notz x} + {R0 == x}.

Lemma Rpmult_le_simpl_left : forall (x y z : Rp) {nx : notz x},
x * y <= x * z -> y <= z.
Hint Resolve Rpmult_le_simpl_left.

Lemma Rpmult_le_simpl_right : forall (x y z : Rp) {nz : notz z},
x * z <= y * z -> x <= y.
Hint Resolve Rpmult_le_simpl_right.

Lemma Rpmult_eq_simpl_left : forall (x y z : Rp) {nx : notz x},
x * y == x * z -> y == z.
Hint Resolve Rpmult_eq_simpl_left.

Lemma Rpmult_eq_simpl_right : forall (x y z : Rp) {nz : notz z},
x * z == y * z -> x == y.
Hint Resolve Rpmult_eq_simpl_right.

Lemma Rpmult_le_perm_right :
forall (x y z : Rp) {nz: notz z}, x * z <= y -> x <= y * [1/]z.
Hint Resolve Rpmult_le_perm_right.

Lemma Rpmult_eq_perm_right :
forall (x y z : Rp) {nz: notz z}, x * z == y -> x == y * [1/]z.
Hint Resolve Rpmult_eq_perm_right.

Lemma Rpmult_le_perm_left :
forall (x y z : Rp), x <= y * z -> x * [1/]y <= z.
Hint Resolve Rpmult_le_perm_left.

Lemma Rpmult_eq_perm_left :
forall (x y z : Rp) {ny: notz y}, x == y * z -> x * [1/]y == z.
Hint Resolve Rpmult_eq_perm_left.

Lemma Rpmult_lt_zero: forall x y : Rp, R0 < x -> R0 < y -> R0 < x * y.
Hint Resolve Rpmult_lt_zero.

Lemma Rp1div_le_perm_left :
forall (x y z : Rp) {ny:notz y}, x * [1/]y <= z -> x <= z * y.
Hint Resolve Rp1div_le_perm_left.

Lemma Rp1div_eq_perm_left :
forall (x y z : Rp) {ny:notz y}, x * [1/]y == z -> x == z * y.
Hint Resolve Rp1div_eq_perm_left.

Lemma Rp1div_le_perm_right :
forall (x y z : Rp) {nz:notz z}, x <= y * [1/]z -> x * z <= y.
Hint Resolve Rp1div_le_perm_right.

Lemma Rp1div_eq_perm_right :
forall (x y z : Rp) {nz:notz z}, x == y * [1/]z -> x * z == y.
Hint Resolve Rp1div_eq_perm_right.

Lemma Rp1div_le_compat : forall (x y : Rp) {nx:notz x}, x <= y -> ([1/]y) <= ([1/]x).
Hint Resolve Rp1div_le_compat.

Add Morphism Rp1div with signature Oeq ==> Oeq
as Rp1div_eq_compat.
Save.
Hint Resolve Rp1div_eq_compat.

Lemma is_Rp1div : forall x y, x * y == R1 -> x == [1/]y.

Lemma Rp1div_1 : [1/]R1 == R1.
Hint Resolve Rp1div_1.

Lemma Rp1div_Rp1div : forall r, [1/][1/]r == r.

Lemma Rp1div_le_simpl : forall x y : Rp, notz y -> [1/]y <= [1/]x -> x <= y.
Hint Immediate Rp1div_le_simpl.

Lemma Rp1div_eq_simpl : forall x y : Rp, [1/]y == [1/]x -> x == y.
Hint Immediate Rp1div_eq_simpl.

Lemma Rp1div_lt_compat : forall x y : Rp, notz x -> x < y -> [1/]y < [1/]x.
Hint Resolve Rp1div_lt_compat.

Lemma Rpmult_Rp1div : forall r1 r2, [1/](r1*r2) == ([1/]r1)*([1/]r2).

Definition of general division

Definition Rpdiv r1 r2 := r1 * [1/] r2.
Notation "x / y" := (Rpdiv x y) : Rp_scope.

Add Morphism Rpdiv with signature Oeq ==> Oeq ==> Oeq
as Rpdiv_eq_compat.
Save.

Lemma Rpdiv_le_compat : forall x y x' y',
notz y' -> x <= y -> y' <= x' -> x/x' <= y/y'.

Lemma Rpdiv_Rp1div : forall r1 r2, [1/](r1/r2) == r2/r1.
Hint Resolve Rpdiv_Rp1div.

Exponential function

Fixpoint Rpexp x (n:nat) {struct n} : Rp :=
match n with O => R1 | S p => x * Rpexp x p end.

Infix "^" := Rpexp : Rp_scope.

Lemma Rpexp_simpl : forall x n, x ^ n = match n with O => R1 | S p => x * (x ^ p) end.

Lemma U2Rp_exp: forall (x:U) n, U2Rp (x ^ n) == (U2Rp x) ^ n.

Lemma Rpexp_le1_mon : forall x n, x <= R1 -> x ^ (S n) <= x ^ n.
Hint Resolve Rpexp_le1_mon.

Lemma Rpexp_le1 : forall x n, x <= R1 -> x ^ n <= R1.
Hint Resolve Rpexp_le1.

Lemma Rpexp_le_compat : forall x y n, x <= y -> x ^ n <= y ^ n.
Hint Resolve Rpexp_le_compat.

Lemma Rpexp_ge1_mon : forall x n, R1 <= x -> x ^ n <= x ^ (S n).
Hint Resolve Rpexp_ge1_mon.

Add Morphism Rpexp with signature Oeq ==> eq ==> Oeq as Rpexp_eq_compat.
Save.

Hint Immediate Rpexp_eq_compat.

Instance Rpexp_mon : forall x, x <= R1 -> monotonic (o2:=Iord Rp) (Rpexp x).
Save.

Lemma Rpexp_0 : forall x, x ^ O == R1.

Lemma Rpexp_1 : forall x, x ^ (S O) == x.
Hint Resolve Rpexp_0 Rpexp_1.

Lemma Rpexp_zero : forall n, (0 < n)%nat -> R0 ^ n == R0.

Lemma Rpexp_one : forall n, R1 ^ n == R1.

Lemma Rpexp_Rp1div_right
: forall r n, notz r -> ([1/]r) ^ n * r ^ n == R1.
Hint Resolve Rpexp_Rp1div_right.

Lemma Rpexp_Rp1div_left
: forall r n, notz r -> r ^ n * ([1/]r) ^ n == R1.
Hint Resolve Rpexp_Rp1div_left.

Lemma Rpexp_Rp1div : forall r n, ([1/]r)^n == [1/](r^n).
Hint Resolve Rpexp_Rp1div.

Lemma Rpexp_Rpmult : forall r m n, r ^ m * r ^ n == r ^ (m+n).

Compatibility of lubs and operations

Lemma islub_Rpplus : forall (f g:nat -> Rp) {mf:monotonic f} {mg:monotonic g} lf lg,
islub f lf -> islub g lg -> islub (fun n => f n + g n) (lf + lg).

Lemma islub_Rpminus : forall (f g:nat -> Rp) {mf:monotonic f} {mg:monotonic (o2:=Iord Rp) g} lf lg,
islub f lf -> isglb g lg -> islub (fun n => f n - g n) (lf - lg).

Lemma islub_cte : forall c : Rp, islub (fun n:nat => c) c.

Lemma islub_fcte : forall f (c:Rp), (forall n:nat, f n == c) -> islub f c.

Lemma islub_zero : forall (f:nat -> Rp), islub f R0 -> forall n, f n == R0.

Lemma islub_Rpplus_cte_left (f :nat -> Rp) lf c :
islub f lf -> islub (fun n => c + f n) (c + lf).
Hint Resolve islub_Rpplus_cte_left.

Lemma islub_Rpplus_cte_right (f :nat -> Rp) lf c :
islub f lf -> islub (fun n => f n + c) (lf + c).
Hint Resolve islub_Rpplus_cte_right.

Lemma islub_Rpmult : forall (f g:nat -> Rp) {mf: monotonic f} {mg:monotonic g} lf lg,
islub f lf -> islub g lg -> islub (fun n => f n * g n) (lf * lg).

Lemma islub_lub_U : forall (f:nat -m> U), islub (fun n => U2Rp (f n)) (U2Rp (lub f)).

Lemma isglb_glb_U : forall (f:nat -m-> U), isglb (fun n => U2Rp (f n)) (U2Rp (glb f)).

Sum of first n values of a function

Instance Rpcompplus_mon (a:nat -> Rp) : monotonic (compn Rpplus R0 a).
Save.

Definition Rpsigma (a: nat -> Rp) : nat -m> Rp := mon (compn Rpplus R0 a).

Lemma Rpsigma_0: forall f : nat -> Rp, Rpsigma f O == R0.
Hint Resolve Rpsigma_0.

Lemma Rpsigma_S:
forall (f : nat -> Rp) (n : nat), Rpsigma f (S n) = f n + Rpsigma f n.
Hint Resolve Rpsigma_S.

Lemma Rpsigma_1 : forall f : nat -> Rp, Rpsigma f 1%nat == f O.
Hint Resolve Rpsigma_1.

Lemma Rpsigma_incr:
forall (f : nat -> Rp) (n m : nat), n <= m -> (Rpsigma f) n <= (Rpsigma f) m.
Hint Resolve Rpsigma_incr.

Lemma Rpsigma_le_compat:
forall (f g : nat -> Rp) (n : nat),
(forall k : nat, (k < n)%nat -> f k <= g k) -> Rpsigma f n <= Rpsigma g n.
Hint Resolve Rpsigma_le_compat.

Lemma Rpsigma_eq_compat:
forall (f g : nat -> Rp) (n : nat),
(forall k : nat, (k < n)%nat -> f k == g k) -> Rpsigma f n == Rpsigma g n.
Hint Resolve Rpsigma_eq_compat.

Lemma Rpsigma_eq_compat_index:
forall (f g : nat -> Rp) (n m: nat), n=m ->
(forall k : nat, (k < n)%nat -> f k == g k) -> (Rpsigma f) n == (Rpsigma g) m.

Lemma Rpsigma_S_lift:
forall (f : nat -> Rp) (n : nat),
Rpsigma f (S n) == f O + Rpsigma (fun k : nat => f (S k)) n.

Lemma Rpsigma_plus_lift:
forall (f : nat -> Rp) (n m : nat),
(Rpsigma f) (n + m)%nat ==
Rpsigma f n + Rpsigma (fun k : nat => f (n + k)%nat) m.

Lemma Rpsigma_zero : forall f n,
(forall k, (k<n)%nat -> f k == R0) -> Rpsigma f n == R0.
Hint Resolve Rpsigma_zero.

Lemma Rpsigma_le : forall f n k, (k<n)%nat -> f k <= Rpsigma f n.
Hint Resolve Rpsigma_le.

Lemma Rpsigma_not_zero : forall f n k, (k<n)%nat -> R0 < f k -> R0 < Rpsigma f n.

Lemma Rpsigma_zero_elim : forall f n,
Rpsigma f n == R0 -> forall k, (k<n)%nat -> f k == R0.

Lemma Rpsigma_minus_decr : forall f n, (forall k, f (S k) <= f k) ->
Rpsigma (fun k => f k - f (S k)) n == f O - f n.

Lemma Rpsigma_minus_incr : forall f n, (forall k, f k <= f (S k)) ->
Rpsigma (fun k => f (S k) - f k) n == f n - f O.

Instance Rpsigma_mon: monotonic Rpsigma.
Save.

Lemma Rpsigma_plus:
forall (f g : nat -> Rp) (n : nat),
Rpsigma (fun k : nat => f k + g k) n == Rpsigma f n + Rpsigma g n.

Lemma Rpsigma_mult:
forall (f : nat -> Rp) (n : nat) (c : Rp),
Rpsigma (fun k : nat => c * f k) n == c * Rpsigma f n.

Lemma Rpsigma_U2Rp : forall (f : nat -> U) n, retract f n
-> Rpsigma f n == sigma f n.
Hint Resolve Rpsigma_U2Rp.

Lemma Rpsigma_U2Rp_bound : forall (f : nat -> U) n, Rpsigma f n <= n.
Hint Resolve Rpsigma_U2Rp_bound.

Lemma islub_Rpsigma : forall (F : nat -> nat -> Rp) {M:monotonic F} (n:nat) (f:nat -> Rp),
(forall k, islub (fun p => F p k) (f k)) -> islub (fun p => Rpsigma (F p) n) (Rpsigma f n).

Lemma islub_U2Rp : forall (f:nat -> U) (x:U), islub f x -> islub (fun n => U2Rp (f n)) (U2Rp x).

Geometrical sum : sigma_0^n x^i

Section GeometricalSum.
Variable x : Rp.
Hypothesis xone : x < R1.

Definition sumg (n:nat) : Rp := Rpsigma (Rpexp x) n.

Lemma sumg_0 : sumg 0 = R0.

Lemma sumg_S : forall n, sumg (S n) = (x ^ n) + sumg n.

Instance invx_not0 : notz (R1 - x).
Save.
Hint Resolve invx_not0.

Lemma sumg_eq : forall n, sumg n == [1/](R1 - x) * (R1 - x ^ n).

Lemma glb_exp_0 : isglb (fun n => x ^ n) R0.

Instance mon_Rpexp_lt : monotonic (o2:=Iord Rp) (Rpexp x).
Save.

Definition RpExp : nat -m-> Rp := mon (o2:=Iord Rp) (Rpexp x).

Lemma sumg_lim : islub sumg ([1/](R1 - x)).

End GeometricalSum.

Miscelaneous lemmas

Lemma U2Rp_half : forall x y:U,
U2Rp ([1/2] * x + [1/2]*y) == ([1/2] * U2Rp x) + [1/2] * U2Rp y.

Lemma Rphalf_plus: ([1/2] + [1/2])%Rp == R1.
Hint Resolve Rphalf_plus.

Lemma Rphalf_refl: forall t : Rp, ([1/2] * t + [1/2] * t)%Rp == t.
Hint Resolve Rphalf_refl.

Lemma Rple_lt_eps
: forall x y:Rp, (forall eps:Rp, R0 < eps -> x <= y + eps) -> x <= y.

Min Max

Definition Rpmin r1 r2 :=
match lt_eq_lt_dec (floor r1) (floor r2) with
inleft (left _) => r1
| inleft (right _) => mkRp (floor r1) (min (decimal r1) (decimal r2))
| inright _ => r2
end.

Lemma min_decimal_lt1 : forall x y, min (decimal x) (decimal y) < 1.
Hint Resolve min_decimal_lt1.

Lemma Rpmin_le_right: forall x y : Rp, Rpmin x y <= x.

Lemma Rpmin_le_left: forall x y : Rp, Rpmin x y <= y.
Hint Resolve Rpmin_le_right Rpmin_le_left.

Lemma Rpmin_le: forall x y z : Rp, z <= x -> z <= y -> z <= Rpmin x y.
Hint Immediate Rpmin_le.

Lemma Rpmin_le_sym : forall x y, Rpmin x y <= Rpmin y x.
Hint Resolve Rpmin_le_sym.

Lemma Rpmin_sym : forall x y, Rpmin x y == Rpmin y x.
Hint Resolve Rpmin_sym.

Lemma Rpmin_le_compat_left : forall x y z, x <= y -> Rpmin x z <= Rpmin y z.
Hint Resolve Rpmin_le_compat_left.

Lemma Rpmin_le_compat_right : forall x y z, y <= z -> Rpmin x y <= Rpmin x z.
Hint Resolve Rpmin_le_compat_right.

Add Morphism Rpmin with signature Ole ==> Ole ==> Ole as Rpmin_le_compat.
Save.
Hint Immediate Rpmin_le_compat.

Add Morphism Rpmin with signature Oeq ==> Oeq ==> Oeq as Rpmin_eq_compat.
Save.
Hint Immediate Rpmin_eq_compat.

Lemma Rpmin_idem: forall x : Rp, Rpmin x x == x.
Hint Resolve Rpmin_idem.

Lemma Rpmin_eq_right : forall x y : Rp, x <= y -> Rpmin x y == x.

Lemma Rpmin_eq_left : forall x y : Rp, y <= x -> Rpmin x y == y.

Hint Resolve Rpmin_eq_right Rpmin_eq_left.

A simplification tactic

Ltac my_rewrite t := setoid_rewrite t || rewrite t.

Ltac Rpsimpl := match goal with
|- context [(Rpplus R0 ?x)] => my_rewrite (Rpplus_zero_left x)
| |- context [(Rpplus ?x R0)] => my_rewrite (Rpplus_zero_right x)
| |- context [(U2Rp U1)] => my_rewrite U2Rp1_R1
| |- context [(U2Rp ?x)] => Usimpl
| |- context [(Rpmult R0 ?x)] => my_rewrite (Rpmult_zero_left x)
| |- context [(Rpmult ?x R0)] => my_rewrite (Rpmult_zero_right x)
| |- context [(Rpmult R1 ?x)] => my_rewrite (Rpmult_one_left x)
| |- context [(Rpmult ?x R1)] => my_rewrite (Rpmult_one_right x)
| |- context [(Rpminus 0 ?x)] => my_rewrite (Rpminus_zero_left x)
| |- context [(Rpminus ?x 0)] => my_rewrite (Rpminus_zero_right x)
| |- context [(Rpmult ?x (Rp1div ?x))] => my_rewrite (Rp1div_right x)
| |- context [(Rpmult (Rp1div ?x) ?x)] => my_rewrite (Rp1div_left x)

| |- context [?x^O] => my_rewrite (Rpexp_0 x)
| |- context [?x^(S O)] => my_rewrite (Rpexp_1 x)
| |- context [0^(?n)] => my_rewrite Rpexp_zero; [idtac|omega]
| |- context [R1^(?n)] => my_rewrite Rpexp_one
| |- context [(NRpmult 0 ?x)] => my_rewrite NRpmult_0
| |- context [(NRpmult 1 ?x)] => my_rewrite NRpmult_1
| |- context [(NRpmult ?n 0)] => my_rewrite NRpmult_zero
| |- context [(Rpsigma ?f O)] => my_rewrite Rpsigma_0
| |- context [(Rpsigma ?f (S O))] => my_rewrite Rpsigma_1
| |- (Ole (Rpplus ?x ?y) (Rpplus ?x ?z)) => apply Rpplus_le_compat_right
| |- (Ole (Rpplus ?x ?z) (Rpplus ?y ?z)) => apply Rpplus_le_compat_left
| |- (Ole (Rpplus ?x ?z) (Rpplus ?z ?y)) => my_rewrite (Rpplus_sym z y);
apply Rpplus_le_compat_left
| |- (Ole (Rpplus ?x ?y) (Rpplus ?z ?x)) => my_rewrite (Rpplus_sym x y);
apply Rpplus_le_compat_left
| |- (Ole (Rpminus ?x ?y) (Rpminus ?x ?z)) => apply Rpminus_le_compat_right
| |- (Ole (Rpminus ?x ?z) (Rpminus ?y ?z)) => apply Rpminus_le_compat_left
| |- ((Rpplus ?x ?y) == (Rpplus ?x ?z)) => apply Rpplus_eq_compat_right
| |- ((Rpplus ?x ?z) == (Rpplus ?y ?z)) => apply Rpplus_eq_compat_left
| |- ((Rpplus ?x ?z) == (Rpplus ?z ?y)) => my_rewrite (Rpplus_sym z y);
apply Rpplus_eq_compat_left
| |- ((Rpplus ?x ?y) == (Rpplus ?z ?x)) => my_rewrite (Rpplus_sym x y);
apply Rpplus_eq_compat_left
| |- ((Rpminus ?x ?y) == (Rpminus ?x ?z)) => apply Rpminus_eq_compat_right
| |- ((Rpminus ?x ?z) == (Rpminus ?y ?z)) => apply Rpminus_eq_compat_left
| |- (Ole (Rpmult ?x ?y) (Rpmult ?x ?z)) => apply Rpmult_le_compat_right
| |- (Ole (Rpmult ?x ?z) (Rpmult ?y ?z)) => apply Rpmult_le_compat_left
| |- (Ole (Rpmult ?x ?z) (Rpmult ?z ?y)) => my_rewrite (Rpmult_sym z y);
apply Rpmult_le_compat_left
| |- (Ole (Rpmult ?x ?y) (Rpmult ?z ?x)) => my_rewrite (Rpmult_sym x y);
apply Rpmult_le_compat_left
| |- ((Rpmult ?x ?y) == (Rpmult ?x ?z)) => apply Rpmult_eq_compat_right
| |- ((Rpmult ?x ?z) == (Rpmult ?y ?z)) => apply Rpmult_eq_compat_left
| |- ((Rpmult ?x ?z) == (Rpmult ?z ?y)) => my_rewrite (Rpmult_sym z y);
apply Rpmult_eq_compat_left
| |- ((Rpmult ?x ?y) == (Rpmult ?z ?x)) => my_rewrite (Rpmult_sym x y);
apply Rpmult_eq_compat_left
end.

More lemmas on notz

Instance notz_S : forall k, notz (N2Rp (S k)).
Hint Resolve notz_S.

Instance notz_Rpexp : forall r n, notz r -> notz (r^n).
Hint Resolve notz_Rpexp.

Instance notz_square : forall r, notz r -> notz (r^2).
Hint Resolve notz_square.

Lemma notz_Unth : forall n, notz ([1/]1+n)%U.
Hint Resolve notz_Unth.

Lemma notz_lt_0 : forall x, R0 < x -> notz x.
Hint Resolve notz_lt_0.

Lemma notz_lt : forall x y, x < y -> notz y.

Lemma notz_lt_minus : forall x y, x < y -> notz (y-x).
Hint Resolve notz_lt_minus.

Lemma notz_N2Rp_lt_0 : forall n:nat, (0 < n)%nat -> notz n.
Hint Resolve notz_N2Rp_lt_0.

Lemma notz_Rpdiv : forall x y, notz x -> notz y -> notz (x / y).
Hint Resolve notz_Rpdiv.

Compatibility of operations on U and R+

Lemma U2Rp_Nmult_eq : forall (n:nat) (u:U), n * u <= R1 ->
U2Rp (n */ u) == N2Rp n * U2Rp u.
Hint Resolve U2Rp_Nmult_eq.

Lemma Nmult_def_Rp : forall n x, Nmult_def n x -> n * x <= R1.

Lemma U2Rp_Nmult_Nmult_def : forall n x, Nmult_def n x ->
U2Rp (Nmult n x) == n * x.

Lemma U2Rp_Unth : forall n, U2Rp (Unth n) == Rp1div (N2Rp (S n)).

Lemma Rpexp_Rpmult_distr :
forall r1 r2 k, (r1 * r2) ^ k == r1^k * r2^k.
Hint Resolve Rpexp_Rpmult_distr.