From f4e1f3bb1bc9df3be720b8daaa5fbd9955df711b Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 13 Oct 2015 14:08:08 -0400 Subject: [PATCH] feat(library/data/real): fix real.order --- library/data/real/order.lean | 215 ++++++++++++++++++----------------- 1 file changed, 109 insertions(+), 106 deletions(-) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 857008868..d4031934f 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -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,