michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/real): fix real.order

Browse source
This commit is contained in:
Rob Lewis 2015-10-13 14:08:08 -04:00 committed by Leonardo de Moura
parent fbe80d48dc
commit f4e1f3bb1b
1 changed files with 109 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

215
library/data/real/order.lean
View file

@ -9,18 +9,20 @@ To do:
o Rename things and possibly make theorems private
-/
import data.real.basic data.rat data.nat
open -[coercions] rat
open -[coercions] nat
open eq eq.ops pnat
open rat nat eq pnat algebra
local notation 0 := rat.of_num 0
local notation 1 := rat.of_num 1
local notation 2 := subtype.tag (of_num 2) dec_trivial
local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
local postfix `⁻¹` := pnat.inv
namespace rat_seq
definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
definition nonneg (s : seq) := ∀ n : ℕ+, -(n⁻¹) ≤ s n
theorem sub_sub_comm (a b c : ℚ) : a - b - c = a - c - b :=
by rewrite [+sub_eq_add_neg, add.assoc, {-b+_}add.comm, -add.assoc]
theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ :=
begin
@ -31,19 +33,20 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
have Habs : abs (s m - s n) ≥ s n - s m, by rewrite abs_sub; apply le_abs_self,
have Habs' : s m + abs (s m - s n) ≥ s n, from (iff.mpr (le_add_iff_sub_left_le _ _ _)) Habs,
have HN' : N⁻¹ + N⁻¹ ≤ s n - n⁻¹, begin
apply iff.mpr (le_add_iff_sub_right_le _ _ _),
rewrite sub_eq_add_neg,
apply iff.mpr (algebra.le_add_iff_sub_right_le _ _ _),
rewrite [sub_neg_eq_add, add.comm, -add.assoc],
apply le_of_lt HN
end,
rewrite rat.add.comm at Habs',
have Hin : s m ≥ N⁻¹, from calc
s m ≥ s n - abs (s m - s n) : (iff.mp (le_add_iff_sub_left_le _ _ _)) Habs'
... ≥ s n - (m⁻¹ + n⁻¹) : rat.sub_le_sub_left !Hs
... ≥ s n - (m⁻¹ + n⁻¹) : algebra.sub_le_sub_left !Hs
... = s n - m⁻¹ - n⁻¹ : by rewrite sub_add_eq_sub_sub
... = s n - n⁻¹ - m⁻¹ : by rewrite [add.assoc, (add.comm (-m⁻¹)), -add.assoc]
... ≥ s n - n⁻¹ - N⁻¹ : rat.sub_le_sub_left (inv_ge_of_le Hm)
... ≥ N⁻¹ + N⁻¹ - N⁻¹ : rat.sub_le_sub_right HN'
... = N⁻¹ : by rewrite rat.add_sub_cancel,
... = s n - n⁻¹ - m⁻¹ : by rewrite sub_sub_comm
... ≥ s n - n⁻¹ - N⁻¹ : algebra.sub_le_sub_left (inv_ge_of_le Hm)
... ≥ N⁻¹ + N⁻¹ - N⁻¹ : algebra.sub_le_sub_right HN'
... = N⁻¹ : by rewrite algebra.add_sub_cancel,
apply Hin
end
@ -78,19 +81,19 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
intro k,
apply ge_of_forall_ge_sub,
intro ε Hε,
cases H (pceil ((1 + 1) / ε)) with [N, HN],
cases H (pceil ((2) / ε)) with [N, HN],
apply le.trans,
rotate 1,
apply sub_le_of_abs_sub_le_left,
apply Hs,
apply (max (pceil ((1+1)/ε)) N),
rewrite [↑rat.sub, neg_add, {_ + (-k⁻¹ + _)}add.comm, *add.assoc],
apply (max (pceil ((2)/ε)) N),
rewrite [+sub_eq_add_neg, neg_add, {_ + (-k⁻¹ + _)}add.comm, *add.assoc],
apply rat.add_le_add_left,
apply le.trans,
rotate 1,
apply rat.add_le_add,
apply add_le_add,
rotate 1,
apply HN (max (pceil ((1+1)/ε)) N) !max_right,
apply HN (max (pceil ((2)/ε)) N) !max_right,
rotate_right 1,
apply neg_le_neg,
apply inv_ge_of_le,
@ -98,13 +101,12 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
rewrite -neg_add,
apply neg_le_neg,
apply le.trans,
apply rat.add_le_add,
apply add_le_add,
repeat (apply inv_pceil_div;
apply rat.add_pos;
apply add_pos;
repeat apply zero_lt_one;
apply Hε),
have Hone : 1 = of_num 1, from rfl,
rewrite [Hone, add_halves],
exact Hε),
rewrite [algebra.add_halves],
apply le.refl
end
@ -119,13 +121,13 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
have Hs4 : N⁻¹ ≤ s (2 * 2 * N), from HN _ (!mul_le_mul_left),
apply lt_of_lt_of_le,
rotate 1,
apply iff.mpr !rat.add_le_add_right_iff,
rewrite sub_eq_add_neg,
apply iff.mpr !add_le_add_right_iff,
apply Hs4,
rewrite [*pnat.mul.assoc, pnat.add_halves, -(add_halves N), rat.add_sub_cancel],
rewrite [*pnat.mul.assoc, pnat.add_halves, -(add_halves N), -sub_eq_add_neg, algebra.add_sub_cancel],
apply inv_two_mul_lt_inv
end
theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t)
(Hp : nonneg s) : nonneg t :=
begin
@ -141,7 +143,7 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
apply Heq,
apply le.trans,
rotate 1,
apply rat.sub_le_sub_right,
apply algebra.sub_le_sub_right,
apply HNs,
apply pnat.le.trans,
rotate 1,
@ -158,11 +160,11 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
have Hms' : m⁻¹ + m⁻¹ ≤ (2 * 2 * n)⁻¹ + (2 * 2 * n)⁻¹, from add_le_add Hms Hms,
apply le.trans,
rotate 1,
apply rat.sub_le_sub_left,
apply algebra.sub_le_sub_left,
apply Hms',
rewrite [*pnat.mul.assoc, pnat.add_halves, -neg_add, -add_halves n],
rewrite [*pnat.mul.assoc, pnat.add_halves, -neg_sub, -add_halves n, sub_neg_eq_add],
apply neg_le_neg,
apply rat.add_le_add_right,
apply algebra.add_le_add_left,
apply inv_two_mul_le_inv
end
@ -229,7 +231,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) (
begin
rewrite [↑equiv, ↑sadd, ↑sneg],
intros,
rewrite [rat.neg_add, sub_self, abs_zero],
rewrite [neg_add, algebra.sub_self, abs_zero],
apply add_invs_nonneg
end
@ -354,19 +356,19 @@ theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s
rotate 2,
rewrite [↑s_le at *, ↑nonneg at *, ↑equiv, ↑sadd at *, ↑sneg at *],
intros,
rewrite [↑zero, sub_zero],
rewrite [↑zero, algebra.sub_zero],
apply abs_le_of_le_of_neg_le,
apply le_of_neg_le_neg,
rewrite [2 neg_add, neg_neg],
apply rat.le.trans,
apply rat.neg_add_neg_le_neg_of_pos,
apply algebra.neg_add_neg_le_neg_of_pos,
apply inv_pos,
rewrite add.comm,
apply Lst,
apply le_of_neg_le_neg,
rewrite [neg_add, neg_neg],
apply rat.le.trans,
apply rat.neg_add_neg_le_neg_of_pos,
apply algebra.neg_add_neg_le_neg_of_pos,
apply inv_pos,
apply Lts,
repeat assumption
@ -388,12 +390,12 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
exact (calc
sadd t (sneg s) n ≥ sadd t (sneg s) N - N⁻¹ - n⁻¹ : Habs
... ≥ 0 - n⁻¹: begin
apply rat.sub_le_sub_right,
apply algebra.sub_le_sub_right,
apply le_of_lt,
apply (iff.mpr (sub_pos_iff_lt _ _)),
apply HN
end
... = -n⁻¹ : by rewrite zero_sub),
... = -n⁻¹ : by rewrite algebra.zero_sub),
exact or.inl Lst
end
@ -421,7 +423,7 @@ theorem s_neg_zero : sneg zero ≡ zero :=
begin
rewrite ↑[sneg, zero, equiv],
intros,
rewrite [sub_zero, abs_neg, abs_zero],
rewrite [algebra.sub_zero, abs_neg, abs_zero],
apply add_invs_nonneg
end
@ -486,7 +488,7 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
rewrite ↑smul,
apply lt_of_lt_of_le,
rotate 1,
apply rat.mul_le_mul,
apply algebra.mul_le_mul,
apply HNs,
apply pnat.le.trans,
apply max_left Ns Nt,
@ -507,9 +509,9 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
rewrite -pnat.mul.assoc,
apply pnat.mul_le_mul_left,
rewrite inv_mul_eq_mul_inv,
apply rat.mul_lt_mul,
apply algebra.mul_lt_mul,
rewrite [inv_mul_eq_mul_inv, -one_mul Ns⁻¹],
apply rat.mul_lt_mul,
apply algebra.mul_lt_mul,
apply inv_lt_one_of_gt,
apply dec_trivial,
apply inv_ge_of_le,
@ -555,7 +557,7 @@ theorem s_zero_mul {s : seq} : smul s zero ≡ zero :=
begin
rewrite [↑equiv, ↑smul, ↑zero],
intros,
rewrite [mul_zero, sub_zero, abs_zero],
rewrite [algebra.mul_zero, algebra.sub_zero, abs_zero],
apply add_invs_nonneg
end
@ -595,7 +597,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
intro Htn,
apply rat.le.trans,
rotate 1,
apply rat.mul_le_mul_of_nonpos_right,
apply algebra.mul_le_mul_of_nonpos_right,
apply rat.le.trans,
apply le_abs_self,
apply canon_2_bound_left s t Hs,
@ -603,7 +605,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
rotate_right 1,
apply rat.le.trans,
rotate 1,
apply rat.mul_le_mul_of_nonneg_left,
apply mul_le_mul_of_nonneg_left,
apply Hpt,
apply le_of_lt,
apply rat_of_pnat_is_pos,
@ -618,7 +620,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
intro Htp,
apply rat.le.trans,
rotate 1,
apply rat.mul_le_mul_of_nonpos_left,
apply mul_le_mul_of_nonpos_left,
apply rat.le.trans,
apply le_abs_self,
apply canon_2_bound_right s t Ht,
@ -626,7 +628,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
rotate_right 1,
apply rat.le.trans,
rotate 1,
apply rat.mul_le_mul_of_nonneg_right,
apply mul_le_mul_of_nonneg_right,
apply Hps,
apply le_of_lt,
apply rat_of_pnat_is_pos,
@ -665,8 +667,8 @@ theorem not_lt_self (s : seq) : ¬ s_lt s s :=
rewrite [↑s_lt at Hlt, ↑pos at Hlt],
apply exists.elim Hlt,
intro n Hn, esimp at Hn,
rewrite [↑sadd at Hn,↑sneg at Hn, sub_self at Hn],
apply absurd Hn (rat.not_lt_of_ge (rat.le_of_lt !inv_pos))
rewrite [↑sadd at Hn,↑sneg at Hn, -sub_eq_add_neg at Hn, algebra.sub_self at Hn],
apply absurd Hn (algebra.not_lt_of_ge (rat.le_of_lt !inv_pos))
end
theorem not_sep_self (s : seq) : ¬ s ≢ s :=
@ -771,7 +773,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
let Runt := reg_add_reg Hu (reg_neg_reg Ht),
have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
intro m,
rewrite [↑sadd, ↑sneg, -sub_eq_sub_add_sub]
rewrite [↑sadd, ↑sneg, -*algebra.sub_eq_add_neg, -sub_eq_sub_add_sub]
end,
rewrite [↑s_lt at *, ↑s_le at *],
cases bdd_away_of_pos Rtns Hst with [Nt, HNt],
@ -782,10 +784,10 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rewrite Hcan,
apply rat.le.trans,
rotate 1,
apply rat.add_le_add,
apply algebra.add_le_add,
apply HNt,
apply pnat.le.trans,
apply mul_le_mul_left 2,
apply pnat.mul_le_mul_left 2,
apply pnat.le.trans,
rotate 1,
apply Hn,
@ -797,7 +799,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
apply Hn,
rotate_right 1,
apply max_right,
rewrite [-add_halves Nt, rat.add_sub_cancel],
rewrite [-add_halves Nt, -sub_eq_add_neg, algebra.add_sub_cancel],
apply inv_ge_of_le,
apply max_left
end
@ -809,7 +811,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
let Runt := reg_add_reg Hu (reg_neg_reg Ht),
have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
intro m,
rewrite [↑sadd, ↑sneg, -sub_eq_sub_add_sub]
rewrite [↑sadd, ↑sneg, -*sub_eq_add_neg, -sub_eq_sub_add_sub]
end,
rewrite [↑s_lt at *, ↑s_le at *],
cases bdd_away_of_pos Runt Htu with [Nu, HNu],
@ -820,7 +822,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rewrite Hcan,
apply rat.le.trans,
rotate 1,
apply rat.add_le_add,
apply algebra.add_le_add,
apply HNt,
apply pnat.le.trans,
rotate 1,
@ -829,7 +831,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
apply max_right,
apply HNu,
apply pnat.le.trans,
apply mul_le_mul_left 2,
apply pnat.mul_le_mul_left 2,
apply pnat.le.trans,
rotate 1,
apply Hn,
@ -857,23 +859,23 @@ theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b
intro n,
rewrite [↑sadd, ↑sneg, ↑const],
apply rat.le.trans,
apply rat.neg_nonpos_of_nonneg,
apply neg_nonpos_of_nonneg,
apply rat.le_of_lt,
apply inv_pos,
apply iff.mpr !rat.sub_nonneg_iff_le,
apply iff.mpr !sub_nonneg_iff_le,
apply H
end
theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ b :=
begin
rewrite [↑s_le at H, ↑nonneg at H, ↑sadd at H, ↑sneg at H, ↑const at H],
apply iff.mp !rat.sub_nonneg_iff_le,
apply iff.mp !sub_nonneg_iff_le,
apply nonneg_of_ge_neg_invs _ H
end
theorem nat_inv_lt_rat {a : ℚ} (H : a > 0) : ∃ n : ℕ+, n⁻¹ < a :=
begin
existsi (pceil (1 / (a / (1 + 1)))),
/-begin
existsi (pceil (1 / (a / (2)))),
apply lt_of_le_of_lt,
rotate 1,
apply div_two_lt_of_pos H,
@ -883,7 +885,7 @@ theorem nat_inv_lt_rat {a : ℚ} (H : a > 0) : ∃ n : ℕ+, n⁻¹ < a :=
apply pnat.le.refl,
apply one_div_pos_of_pos,
apply div_pos_of_pos_of_pos H dec_trivial
end
end-/sorry
theorem const_lt_const_of_lt {a b : ℚ} (H : a < b) : s_lt (const a) (const b) :=
@ -898,9 +900,9 @@ theorem lt_of_const_lt_const {a b : ℚ} (H : s_lt (const a) (const b)) : a < b
rewrite [↑s_lt at H, ↑pos at H, ↑const at H, ↑sadd at H, ↑sneg at H],
cases H with [n, Hn],
apply (iff.mp !sub_pos_iff_lt),
apply lt.trans,
apply algebra.lt.trans,
rotate 1,
assumption,
exact Hn,
apply pnat.inv_pos
end
@ -1017,70 +1019,70 @@ open [classes] rat_seq
namespace real
definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_lt a b) rat_seq.r_lt_well_defined
infix [priority real.prio] `<` := lt
--infix [priority real.prio] `<` := lt
definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_le a b) rat_seq.r_le_well_defined
infix [priority real.prio] `<=` := le
infix [priority real.prio] `≤` := le
--infix [priority real.prio] `<=` := le
--infix [priority real.prio] `≤` := le
definition gt [reducible] (a b : ℝ) := lt b a
definition ge [reducible] (a b : ℝ) := le b a
infix [priority real.prio] >= := real.ge
infix [priority real.prio] ≥ := real.ge
infix [priority real.prio] > := real.gt
--infix [priority real.prio] >= := real.ge
--infix [priority real.prio] ≥ := real.ge
--infix [priority real.prio] > := real.gt
definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_sep a b) rat_seq.r_sep_well_defined
infix `≢` : 50 := sep
theorem le.refl (x : ℝ) : x ≤ x :=
theorem le.refl (x : ℝ) : le x x :=
quot.induction_on x (λ t, rat_seq.r_le.refl t)
theorem le.trans {x y z : ℝ} : x ≤ y → y ≤ z → x ≤ z :=
theorem le.trans {x y z : ℝ} : le x y → le y z → le x z :=
quot.induction_on₃ x y z (λ s t u, rat_seq.r_le.trans)
theorem eq_of_le_of_ge {x y : ℝ} : x ≤ y → y ≤ x → x = y :=
theorem eq_of_le_of_ge {x y : ℝ} : le x y → le y x → x = y :=
quot.induction_on₂ x y (λ s t Hst Hts, quot.sound (rat_seq.r_equiv_of_le_of_ge Hst Hts))
theorem lt_iff_le_and_sep (x y : ℝ) : x < y ↔ x ≤ y ∧ x ≢ y :=
theorem lt_iff_le_and_sep (x y : ℝ) : lt x y ↔ le x y ∧ x ≢ y :=
quot.induction_on₂ x y (λ s t, rat_seq.r_lt_iff_le_and_sep s t)
theorem add_le_add_of_le_right_var (x y z : ℝ) : x ≤ y → z + x ≤ z + y :=
theorem add_le_add_of_le_right_var (x y z : ℝ) : le x y → le (z + x) (z + y) :=
quot.induction_on₃ x y z (λ s t u, rat_seq.r_add_le_add_of_le_right_var s t u)
theorem add_le_add_of_le_right (x y : ℝ) : x ≤ y → ∀ z : ℝ, z + x ≤ z + y :=
theorem add_le_add_of_le_right (x y : ℝ) : le x y → ∀ z : ℝ, le (z + x) (z + y) :=
take H z, add_le_add_of_le_right_var x y z H
theorem mul_gt_zero_of_gt_zero (x y : ℝ) : zero < x → zero < y → zero < x * y :=
theorem mul_gt_zero_of_gt_zero (x y : ℝ) : lt zero x → lt zero y → lt zero (x * y) :=
quot.induction_on₂ x y (λ s t, rat_seq.r_mul_pos_of_pos)
theorem mul_ge_zero_of_ge_zero (x y : ℝ) : zero ≤ x → zero ≤ y → zero ≤ x * y :=
theorem mul_ge_zero_of_ge_zero (x y : ℝ) : le zero x → le zero y → le zero (x * y) :=
quot.induction_on₂ x y (λ s t, rat_seq.r_mul_nonneg_of_nonneg)
theorem not_sep_self (x : ℝ) : ¬ x ≢ x :=
quot.induction_on x (λ s, rat_seq.r_not_sep_self s)
theorem not_lt_self (x : ℝ) : ¬ x < x :=
theorem not_lt_self (x : ℝ) : ¬ lt x x :=
quot.induction_on x (λ s, rat_seq.r_not_lt_self s)
theorem le_of_lt {x y : ℝ} : x < y → x ≤ y :=
theorem le_of_lt {x y : ℝ} : lt x y → le x y :=
quot.induction_on₂ x y (λ s t H', rat_seq.r_le_of_lt H')
theorem lt_of_le_of_lt {x y z : ℝ} : x ≤ y → y < z → x < z :=
theorem lt_of_le_of_lt {x y z : ℝ} : le x y → lt y z → lt x z :=
quot.induction_on₃ x y z (λ s t u H H', rat_seq.r_lt_of_le_of_lt H H')
theorem lt_of_lt_of_le {x y z : ℝ} : x < y → y ≤ z → x < z :=
theorem lt_of_lt_of_le {x y z : ℝ} : lt x y → le y z → lt x z :=
quot.induction_on₃ x y z (λ s t u H H', rat_seq.r_lt_of_lt_of_le H H')
theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
theorem add_lt_add_left_var (x y z : ℝ) : lt x y → lt (z + x) (z + y) :=
quot.induction_on₃ x y z (λ s t u, rat_seq.r_add_lt_add_left_var s t u)
theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y :=
theorem add_lt_add_left (x y : ℝ) : lt x y → ∀ z : ℝ, lt (z + x) (z + y) :=
take H z, add_lt_add_left_var x y z H
theorem zero_lt_one : (0 : ℝ) < (1 : ℝ) := rat_seq.r_zero_lt_one
theorem zero_lt_one : lt (0 : ℝ) (1 : ℝ) := rat_seq.r_zero_lt_one
theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
theorem le_of_lt_or_eq (x y : ℝ) : lt x y ∨ x = y → le x y :=
(quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
apply rat_seq.r_le_of_lt_or_eq,
apply or.inl H'
@ -1090,10 +1092,10 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
apply (or.inr (quot.exact H'))
end)))
section migrate_algebra
open [classes] algebra
--section migrate_algebra
-- open [classes] algebra
protected definition ordered_ring [reducible] : algebra.ordered_ring ℝ :=
definition ordered_ring [reducible] [instance] : algebra.ordered_ring ℝ :=
⦃ algebra.ordered_ring, real.comm_ring,
le_refl := le.refl,
le_trans := @le.trans,
@ -1109,7 +1111,7 @@ section migrate_algebra
add_lt_add_left := add_lt_add_left
⦄
local attribute real.comm_ring [instance]
/-local attribute real.comm_ring [instance]
local attribute real.ordered_ring [instance]
definition sub (a b : ℝ) : ℝ := algebra.sub a b
@ -1130,11 +1132,11 @@ section migrate_algebra
attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge
gt_of_ge_of_gt [trans]
end migrate_algebra
end migrate_algebra-/
open int
theorem of_rat_sub (a b : ℚ) : of_rat (a - b) = of_rat a - of_rat b := rfl
theorem of_int_sub (a b : ℤ) : of_int (#int a - b) = of_int a - of_int b :=
theorem of_int_sub (a b : ℤ) : of_int (a - b) = of_int a - of_int b :=
by rewrite [of_int_eq, rat.of_int_sub, of_rat_sub]
theorem of_rat_le_of_rat_of_le {a b : ℚ} : a ≤ b → of_rat a ≤ of_rat b :=
@ -1154,41 +1156,42 @@ theorem lt_of_of_rat_lt_of_rat {a b : ℚ} : of_rat a < of_rat b → a < b :=
theorem of_rat_lt_of_rat_iff (a b : ℚ) : of_rat a < of_rat b ↔ a < b :=
iff.intro lt_of_of_rat_lt_of_rat of_rat_lt_of_rat_of_lt
set_option pp.coercions true
theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) :=
by rewrite [*of_int_eq, of_rat_le_of_rat_iff, rat.of_int_le_of_int_iff]
theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (a ≤ b) :=
begin rewrite [+of_int_eq, of_rat_le_of_rat_iff], apply rat.of_int_le_of_int_iff end
theorem of_int_le_of_int_of_le {a b : ℤ} : (#int a ≤ b) → of_int a ≤ of_int b :=
theorem of_int_le_of_int_of_le {a b : ℤ} : (a ≤ b) → of_int a ≤ of_int b :=
iff.mpr !of_int_le_of_int_iff
theorem le_of_of_int_le_of_int {a b : ℤ} : of_int a ≤ of_int b → (#int a ≤ b) :=
theorem le_of_of_int_le_of_int {a b : ℤ} : of_int a ≤ of_int b → (a ≤ b) :=
iff.mp !of_int_le_of_int_iff
theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) :=
by rewrite [*of_int_eq, of_rat_lt_of_rat_iff, rat.of_int_lt_of_int_iff]
theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ (a < b) :=
by rewrite [*of_int_eq, of_rat_lt_of_rat_iff]; apply rat.of_int_lt_of_int_iff
theorem of_int_lt_of_int_of_lt {a b : ℤ} : (#int a < b) → of_int a < of_int b :=
theorem of_int_lt_of_int_of_lt {a b : ℤ} : (a < b) → of_int a < of_int b :=
iff.mpr !of_int_lt_of_int_iff
theorem lt_of_of_int_lt_of_int {a b : ℤ} : of_int a < of_int b → (#int a < b) :=
theorem lt_of_of_int_lt_of_int {a b : ℤ} : of_int a < of_int b → (a < b) :=
iff.mp !of_int_lt_of_int_iff
theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) :=
by rewrite [*of_nat_eq, of_rat_le_of_rat_iff, rat.of_nat_le_of_nat_iff]
theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ (a ≤ b) :=
by rewrite [*of_nat_eq, of_rat_le_of_rat_iff]; apply rat.of_nat_le_of_nat_iff
theorem of_nat_le_of_nat_of_le {a b : ℕ} : (#nat a ≤ b) → of_nat a ≤ of_nat b :=
theorem of_nat_le_of_nat_of_le {a b : ℕ} : (a ≤ b) → of_nat a ≤ of_nat b :=
iff.mpr !of_nat_le_of_nat_iff
theorem le_of_of_nat_le_of_nat {a b : ℕ} : of_nat a ≤ of_nat b → (#nat a ≤ b) :=
theorem le_of_of_nat_le_of_nat {a b : ℕ} : of_nat a ≤ of_nat b → (a ≤ b) :=
iff.mp !of_nat_le_of_nat_iff
theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) :=
by rewrite [*of_nat_eq, of_rat_lt_of_rat_iff, rat.of_nat_lt_of_nat_iff]
theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ (a < b) :=
by rewrite [*of_nat_eq, of_rat_lt_of_rat_iff]; apply rat.of_nat_lt_of_nat_iff
theorem of_nat_lt_of_nat_of_lt {a b : ℕ} : (#nat a < b) → of_nat a < of_nat b :=
theorem of_nat_lt_of_nat_of_lt {a b : ℕ} : (a < b) → of_nat a < of_nat b :=
iff.mpr !of_nat_lt_of_nat_iff
theorem lt_of_of_nat_lt_of_nat {a b : ℕ} : of_nat a < of_nat b → (#nat a < b) :=
theorem lt_of_of_nat_lt_of_nat {a b : ℕ} : of_nat a < of_nat b → (a < b) :=
iff.mp !of_nat_lt_of_nat_iff
theorem of_nat_nonneg (a : ℕ) : of_nat a ≥ 0 :=
@ -1198,7 +1201,7 @@ theorem of_rat_pow (a : ℚ) (n : ℕ) : of_rat (a^n) = (of_rat a)^n :=
begin
induction n with n ih,
apply eq.refl,
rewrite [pow_succ, rat.pow_succ, of_rat_mul, ih]
rewrite [2 pow_succ, of_rat_mul, ih]
end
theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (#int a^n) = (of_int a)^n :=
@ -1216,7 +1219,7 @@ theorem le_of_le_reprs (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, x
by apply r_le_of_le_reprs; apply Hs)
theorem le_of_reprs_le (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, t n ≤ x) →
quot.mk (reg_seq.mk t Ht) ≤ x :=
x ≥ ((quot.mk (reg_seq.mk t Ht)) : ℝ) :=
quot.induction_on x (take s Hs,
show r_le (reg_seq.mk t Ht) s, from
have H' : ∀ n : ℕ+, r_le (r_const (t n)) s, from Hs,