Library ALEA.Rplus
Add Rec LoadPath "." as ALEA.
Require Export Uprop.
Open Local Scope U_scope.
Require Export Omega.
Require Export Arith.
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.
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.
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.
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.
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 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.
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.
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.
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.
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).
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.
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.
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.
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).
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.
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.
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
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.
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.
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 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.
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).
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)).
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).
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.
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.
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.
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.
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.
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.
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.