From 53236718a8dc6ceaefafdfcae7499d0abf8d6121 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 17 Jun 2016 12:03:31 +0200 Subject: [PATCH] refactor(library/data/pnat): make pnat a decidable_linear_order --- library/data/pnat.lean | 75 ++++++++++++++++----------------- library/data/real/basic.lean | 35 ++++++--------- library/data/real/complete.lean | 44 +++++++++---------- library/data/real/division.lean | 44 +++++++++---------- library/data/real/order.lean | 56 ++++++++++++------------ 5 files changed, 121 insertions(+), 133 deletions(-) diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 4a328329d..dcb6a7067 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -11,9 +11,11 @@ are those needed for that construction. import data.rat.order data.nat open nat rat subtype eq.ops +definition pnat := { n : ℕ | n > 0 } + namespace pnat -definition pnat := { n : ℕ | n > 0 } +protected definition prio := num.pred nat.prio notation `ℕ+` := pnat @@ -35,19 +37,19 @@ protected definition le (p q : ℕ+) := p~ ≤ q~ protected definition lt (p q : ℕ+) := p~ < q~ -definition pnat_has_add [instance] : has_add pnat := +definition pnat_has_add [instance] [priority pnat.prio] : has_add pnat := has_add.mk pnat.add -definition pnat_has_mul [instance] : has_mul pnat := +definition pnat_has_mul [instance] [priority pnat.prio] : has_mul pnat := has_mul.mk pnat.mul -definition pnat_has_le [instance] : has_le pnat := +definition pnat_has_le [instance] [priority pnat.prio] : has_le pnat := has_le.mk pnat.le -definition pnat_has_lt [instance] : has_lt pnat := +definition pnat_has_lt [instance] [priority pnat.prio] : has_lt pnat := has_lt.mk pnat.lt -definition pnat_has_one [instance] : has_one pnat := +definition pnat_has_one [instance] [priority pnat.prio] : has_one pnat := has_one.mk (pos (1:nat) dec_trivial) protected lemma mul_def (p q : ℕ+) : p * q = tag (p~ * q~) (mul_pos (pnat_pos p) (pnat_pos q)) := @@ -62,44 +64,44 @@ rfl protected theorem pnat.eq {p q : ℕ+} : p~ = q~ → p = q := subtype.eq -definition pnat_le_decidable [instance] (p q : ℕ+) : decidable (p ≤ q) := -begin rewrite pnat.le_def, exact nat.decidable_le p~ q~ end +protected definition decidable_lt : decidable_rel pnat.lt := +λa b, nat.decidable_lt a~ b~ -definition pnat_lt_decidable [instance] {p q : ℕ+} : decidable (p < q) := -begin rewrite pnat.lt_def, exact nat.decidable_lt p~ q~ end +protected theorem le_refl (a : ℕ+) : a ≤ a := +begin rewrite pnat.le_def end protected theorem le_trans {p q r : ℕ+} : p ≤ q → q ≤ r → p ≤ r := begin rewrite *pnat.le_def, apply nat.le_trans end -definition max (p q : ℕ+) : ℕ+ := -tag (max p~ q~) (lt_of_lt_of_le (!pnat_pos) (!le_max_right)) +protected theorem le_antisymm {n m : ℕ+} : n ≤ m → m ≤ n → n = m := +begin rewrite +pnat.le_def, intros, apply (pnat.eq (nat.le_antisymm a a_1)) end -protected theorem max_right (a b : ℕ+) : max a b ≥ b := -begin change b ≤ max a b, rewrite pnat.le_def, apply le_max_right end +protected theorem le_iff_lt_or_eq (m n : ℕ+) : m ≤ n ↔ m < n ∨ m = n := +begin + rewrite [pnat.lt_def, pnat.le_def], apply iff.intro, + { intro, apply or.elim (nat.lt_or_eq_of_le a), + intro, apply or.intro_left, assumption, + intro, apply or.intro_right, apply pnat.eq, assumption }, + { intro, apply or.elim a, apply nat.le_of_lt, intro, rewrite a_1 } +end -protected theorem max_left (a b : ℕ+) : max a b ≥ a := -begin change a ≤ max a b, rewrite pnat.le_def, apply le_max_left end +protected theorem le_total (m n : ℕ+) : m ≤ n ∨ n ≤ m := +begin rewrite pnat.le_def, apply nat.le_total end -protected theorem max_eq_right {a b : ℕ+} (H : a < b) : max a b = b := -begin rewrite pnat.lt_def at H, exact pnat.eq (max_eq_right_of_lt H) end +protected theorem lt_irrefl (a : ℕ+) : ¬ a < a := +begin rewrite pnat.lt_def, apply nat.lt_irrefl end -protected theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a := -begin rewrite pnat.lt_def at H, exact pnat.eq (max_eq_left (le_of_not_gt H)) end - -protected theorem le_of_lt {a b : ℕ+} : a < b → a ≤ b := -begin rewrite [pnat.lt_def, pnat.le_def], apply nat.le_of_lt end - -protected theorem not_lt_of_ge {a b : ℕ+} : a ≤ b → ¬ (b < a) := -begin rewrite [pnat.lt_def, pnat.le_def], apply not_lt_of_ge end - -protected theorem le_of_not_gt {a b : ℕ+} : ¬ a < b → b ≤ a := -begin rewrite [pnat.lt_def, pnat.le_def], apply le_of_not_gt end - -protected theorem eq_of_le_of_ge {a b : ℕ+} : a ≤ b → b ≤ a → a = b := -begin rewrite [+pnat.le_def], intros H1 H2, exact pnat.eq (eq_of_le_of_ge H1 H2) end - -protected theorem le_refl (a : ℕ+) : a ≤ a := -begin rewrite pnat.le_def end +protected definition decidable_linear_order [trans_instance] : decidable_linear_order pnat := +⦃ decidable_linear_order, + le := pnat.le, + le_refl := by apply pnat.le_refl, + le_trans := by apply @pnat.le_trans, + le_antisymm := by apply @pnat.le_antisymm, + lt := pnat.lt, + lt_irrefl := by apply pnat.lt_irrefl, + le_iff_lt_or_eq := by apply pnat.le_iff_lt_or_eq, + decidable_lt := pnat.decidable_lt, + le_total := by apply pnat.le_total ⦄ notation 2 := (tag 2 dec_trivial : ℕ+) notation 3 := (tag 3 dec_trivial : ℕ+) @@ -273,9 +275,6 @@ end protected theorem mul_le_mul_right (p q : ℕ+) : p ≤ p * q := by rewrite pnat.mul_comm; apply pnat.mul_le_mul_left -theorem pnat.lt_of_not_le {p q : ℕ+} : ¬ p ≤ q → q < p := -begin rewrite [pnat.le_def, pnat.lt_def], apply lt_of_not_ge end - protected theorem inv_cancel_left (p : ℕ+) : rat_of_pnat p * p⁻¹ = (1 : ℚ) := mul_one_div_cancel (ne.symm (ne_of_lt !rat_of_pnat_is_pos)) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 13f3bdf55..c2789a1d5 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -199,7 +199,7 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) apply rat.le_trans, apply rat.add_le_add_left, apply add_le_add, - apply HNj (max j Nj) (pnat.max_right j Nj), + apply HNj (max j Nj) (le_max_right j Nj), apply Ht, have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹), from λm, calc @@ -211,8 +211,8 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) rewrite hsimp, have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin apply add_le_add, - apply inv_ge_of_le (pnat.max_left j Nj), - apply inv_ge_of_le (pnat.max_left j Nj), + apply inv_ge_of_le (le_max_left j Nj), + apply inv_ge_of_le (le_max_left j Nj), end, apply (calc n⁻¹ + n⁻¹ + j⁻¹ + ((max j Nj)⁻¹ + (max j Nj)⁻¹) ≤ n⁻¹ + n⁻¹ + j⁻¹ + (j⁻¹ + j⁻¹) : @@ -303,30 +303,19 @@ theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : definition K₂ (s t : seq) := max (K s) (K t) private theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s := - if H : K s < K t then - (have H1 : K₂ s t = K t, from pnat.max_eq_right H, - have H2 : K₂ t s = K t, from pnat.max_eq_left (pnat.not_lt_of_ge (pnat.le_of_lt H)), - by rewrite [H1, -H2]) - else - (have H1 : K₂ s t = K s, from pnat.max_eq_left H, - if J : K t < K s then - (have H2 : K₂ t s = K s, from pnat.max_eq_right J, by rewrite [H1, -H2]) - else - (have Heq : K t = K s, from - pnat.eq_of_le_of_ge (pnat.le_of_not_gt H) (pnat.le_of_not_gt J), - by rewrite [↑K₂, Heq])) +!max.comm theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K₂ s t) := calc abs (s n) ≤ rat_of_pnat (K s) : canon_bound Hs n - ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!pnat.max_left) + ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!le_max_left) theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) : abs (t n) ≤ rat_of_pnat (K₂ s t) := calc abs (t n) ≤ rat_of_pnat (K t) : canon_bound Ht n - ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!pnat.max_right) + ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!le_max_right) definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n)) @@ -710,12 +699,12 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular apply abs_add_le_abs_add_abs, apply add_le_add, apply HN1, - apply pnat.le_trans, - apply pnat.max_left N1 N2, + apply le.trans, + apply le_max_left N1 N2, apply Hn, apply HN2, - apply pnat.le_trans, - apply pnat.max_right N1 N2, + apply le.trans, + apply le_max_right N1 N2, apply Hn end @@ -738,7 +727,7 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz : have HN' : ∀ (n : ℕ+), N ≤ n → abs (t n) ≤ ε / Kq s, from λ n, (eq.subst (sub_zero (t n)) (HN n)), apply HN', - apply pnat.le_trans Hn, + apply le.trans Hn, apply pnat.mul_le_mul_left, apply abs_nonneg, apply le_of_lt (Kq_bound_pos Hs), @@ -915,7 +904,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one := ... = abs 1 : abs_of_pos zero_lt_one ... ≤ 2⁻¹ : H, let H'' := ge_of_inv_le H', - apply absurd (one_lt_two) (pnat.not_lt_of_ge H'') + apply absurd (one_lt_two) (not_lt_of_ge H'') end --------------------------------------------- diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index a7b92cee4..0beece400 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -56,7 +56,7 @@ theorem rat_approx_seq {s : seq} (H : regular s) : rewrite -sub_eq_add_neg, apply sub_le_sub_left, apply HN, - apply pnat.le_trans, + apply le.trans, apply Hp, rewrite -*pnat.mul_assoc, apply pnat.mul_le_mul_left, @@ -289,11 +289,11 @@ theorem cauchy_with_rate_of_converges_to_with_rate {X : r_seq} {a : ℝ} {N : krewrite pnat.add_halves, end -private definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k)) +private definition Nb (M : ℕ+ → ℕ+) := λ k, max (3 * k) (M (2 * k)) -private theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !pnat.max_right +private theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !le_max_right -private theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !pnat.max_left +private theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !le_max_left section lim_seq parameter {X : r_seq} @@ -318,7 +318,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) : rotate 1, apply Nb_spec_right, rotate 1, - apply pnat.le_trans, + apply le.trans, apply Hmn, apply Nb_spec_right, krewrite [-+of_rat_add], @@ -341,7 +341,7 @@ theorem lim_seq_reg : rat_seq.regular lim_seq := apply abs_add_three, cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2], apply lim_seq_reg_helper Hor1, - let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2), + let Hor2' := le_of_lt (lt_of_not_ge Hor2), krewrite [abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub, rat.add_comm, add_comm_three], apply lim_seq_reg_helper Hor2' @@ -383,17 +383,17 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li apply le.trans, apply add_le_add_three, apply Hc, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, apply Nb_spec_right, have HMk : M (2 * k) ≤ Nb M n, begin - apply pnat.le_trans, + apply le.trans, apply Nb_spec_right, - apply pnat.le_trans, + apply le.trans, apply Hn, - apply pnat.le_trans, + apply le.trans, apply pnat.mul_le_mul_left 3, apply Nb_spec_left end, @@ -409,13 +409,13 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li apply rat.le_refl, apply inv_ge_of_le, apply pnat_mul_le_mul_left', - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, apply Nb_spec_left, apply inv_ge_of_le, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, @@ -442,7 +442,7 @@ theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_int z := apply rat_seq.s_le_of_le_pointwise (rat_seq.reg_seq.is_reg s), apply rat_seq.const_reg, intro n, - apply rat.le_trans, + apply le.trans, apply Hb, apply ubound_ge end, @@ -814,7 +814,7 @@ private theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i rewrite (if_pos Havg), apply Ha, rewrite [if_neg Havg, ↑avg_seq, ↑avg], - apply rat.le_trans, + apply le.trans, apply Ha, rewrite -(add_halves (under_seq (i + a))) at {1}, apply add_le_add_right, @@ -839,7 +839,7 @@ private theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq rewrite [add_succ, over_succ], cases em (ub (avg_seq (i + a))) with [Havg, Havg], rewrite [if_pos Havg, ↑avg_seq, ↑avg], - apply rat.le_trans, + apply le.trans, rotate 1, apply Ha, rotate 1, @@ -869,15 +869,15 @@ private theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n) abs (s m - s n) ≤ m⁻¹ + n⁻¹ := begin cases H m n Hm with [T1under, T1over], - cases H m m (!pnat.le_refl) with [T2under, T2over], - apply rat.le_trans, + cases H m m (!le.refl) with [T2under, T2over], + apply le.trans, apply dist_bdd_within_interval, apply under_seq'_lt_over_seq'_single, rotate 1, repeat assumption, - apply rat.le_trans, + apply le.trans, apply width', - apply rat.le_trans, + apply le.trans, apply rat_power_two_inv_ge, apply le_add_of_nonneg_right, apply rat.le_of_lt (!pnat.inv_pos) @@ -890,7 +890,7 @@ private theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_s intros, cases em (m ≤ n) with [Hm, Hn], apply regular_lemma_helper Hm H, - note T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H, + note T := regular_lemma_helper (le_of_lt (lt_of_not_ge Hn)) H, rewrite [abs_sub at T, {n⁻¹ + _}add.comm at T], exact T end @@ -954,11 +954,11 @@ private theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y := private theorem under_over_equiv : p_under_seq ≡ p_over_seq := begin intros, - apply rat.le_trans, + apply le.trans, have H : p_under_seq n < p_over_seq n, from !under_seq_lt_over_seq, rewrite [abs_of_neg (iff.mpr !sub_neg_iff_lt H), neg_sub], apply width', - apply rat.le_trans, + apply le.trans, apply rat_power_two_inv_ge, apply le_add_of_nonneg_left, apply rat.le_of_lt !pnat.inv_pos diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 5d1acfb7c..cceeadbd6 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -122,7 +122,7 @@ private theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) begin apply eq.trans, apply dif_pos Hsep, - apply dif_neg (pnat.not_lt_of_ge Hn) + apply dif_neg (not_lt_of_ge Hn) end private theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+} @@ -144,7 +144,7 @@ private theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) end) else (begin - rewrite [(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hn)), abs_one_div], + rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hn)), abs_one_div], apply div_le_pnat, apply ps_spec, rewrite pnat.mul_assoc, @@ -194,7 +194,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ rewrite [sub_self, abs_zero], apply add_invs_nonneg, rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt), - (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt))], + (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt))], rewrite [(!div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul], apply le.trans, apply mul_le_mul, @@ -203,7 +203,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ apply mul_le_mul, rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt), apply le_ps Hs Hsep, - rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)), + rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)), apply le_ps Hs Hsep, apply abs_nonneg, apply le_of_lt !rat_of_pnat_is_pos, @@ -212,18 +212,18 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ rewrite [right_distrib, *pnat_cancel', add.comm], apply add_le_add_right, apply inv_ge_of_le, - apply pnat.le_of_lt, + apply le_of_lt, apply Hmlt, cases em (n < ps Hs Hsep) with [Hnlt, Hnlt], rewrite [(s_inv_of_sep_lt_p Hs Hsep Hnlt), - (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))], + (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))], rewrite [(!div_sub_div Hspm Hsp), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul], apply le.trans, apply mul_le_mul, apply Hs, rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hsp), abs_mul], apply mul_le_mul, - rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)), + rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)), apply le_ps Hs Hsep, rewrite -(s_inv_of_sep_lt_p Hs Hsep Hnlt), apply le_ps Hs Hsep, @@ -234,19 +234,19 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_ rewrite [right_distrib, *pnat_cancel', add.comm], apply rat.add_le_add_left, apply inv_ge_of_le, - apply pnat.le_of_lt, + apply le_of_lt, apply Hnlt, - rewrite [(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)), - (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))], + rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)), + (s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt))], rewrite [(!div_sub_div Hspm Hspn), div_eq_mul_one_div, abs_mul, *one_mul, *mul_one], apply le.trans, apply mul_le_mul, apply Hs, rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hspn), abs_mul], apply mul_le_mul, - rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)), + rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)), apply le_ps Hs Hsep, - rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)), + rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)), apply le_ps Hs Hsep, apply abs_nonneg, apply le_of_lt !rat_of_pnat_is_pos, @@ -262,13 +262,13 @@ theorem s_inv_ne_zero {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) rewrite (s_inv_of_sep_gt_p Hs Hsep H), apply one_div_ne_zero, apply s_ne_zero_of_ge_p, - apply pnat.le_trans, + apply le.trans, apply H, apply pnat.mul_le_mul_left end) else (begin - rewrite (s_inv_of_sep_lt_p Hs Hsep (pnat.lt_of_not_le H)), + rewrite (s_inv_of_sep_lt_p Hs Hsep (lt_of_not_ge H)), apply one_div_ne_zero, apply s_ne_zero_of_ge_p, apply pnat.mul_le_mul_left @@ -292,10 +292,10 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : apply Rsi, apply abs_nonneg, have Hp : (K₂ s (s_inv Hs)) * 2 * n ≥ ps Hs Hsep, begin - apply pnat.le_trans, - apply pnat.max_left, + apply le.trans, + apply le_max_left, rotate 1, - apply pnat.le_trans, + apply le.trans, apply Hn, apply pnat.mul_le_mul_left end, @@ -315,17 +315,17 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : apply add_le_add, apply inv_ge_of_le, apply pnat_mul_le_mul_left', - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, - apply pnat.max_right, + apply le_max_right, apply inv_ge_of_le, apply pnat_mul_le_mul_left', - apply pnat.le_trans, - apply pnat.max_right, + apply le.trans, + apply le_max_right, rotate 1, - apply pnat.le_trans, + apply le.trans, apply Hn, apply pnat.mul_le_mul_right end diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 25ada2763..b8ae1553d 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -58,7 +58,7 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → ( apply lt_of_lt_of_le, apply inv_add_lt_left, apply HN, - apply pnat.le_of_lt, + apply le_of_lt, apply lt_add_left end @@ -94,11 +94,11 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s) rotate 1, apply add_le_add, rotate 1, - apply HN (max (pceil ((2)/ε)) N) !pnat.max_right, + apply HN (max (pceil ((2)/ε)) N) !le_max_right, rotate_right 1, apply neg_le_neg, apply inv_ge_of_le, - apply pnat.max_left, + apply le_max_left, rewrite -neg_add, apply neg_le_neg, apply le.trans, @@ -146,17 +146,17 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He rotate 1, apply sub_le_sub_right, apply HNs, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hm, rotate_right 1, - apply pnat.max_left, + apply le_max_left, have Hms : m⁻¹ ≤ (2 * 2 * n)⁻¹, begin apply inv_ge_of_le, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hm; - apply pnat.max_right + apply le_max_right end, have Hms' : m⁻¹ + m⁻¹ ≤ (2 * 2 * n)⁻¹ + (2 * 2 * n)⁻¹, from add_le_add Hms Hms, apply le.trans, @@ -492,13 +492,13 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po rotate 1, apply mul_le_mul, apply HNs, - apply pnat.le_trans, - apply pnat.max_left Ns Nt, + apply le.trans, + apply le_max_left Ns Nt, rewrite -pnat.mul_assoc, apply pnat.mul_le_mul_left, apply HNt, - apply pnat.le_trans, - apply pnat.max_right Ns Nt, + apply le.trans, + apply le_max_right Ns Nt, rewrite -pnat.mul_assoc, apply pnat.mul_le_mul_left, apply rat.le_of_lt, @@ -506,8 +506,8 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po apply rat.le_trans, rotate 1, apply HNs, - apply pnat.le_trans, - apply pnat.max_left Ns Nt, + apply le.trans, + apply le_max_left Ns Nt, rewrite -pnat.mul_assoc, apply pnat.mul_le_mul_left, rewrite pnat.inv_mul_eq_mul_inv, @@ -517,11 +517,11 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po apply inv_lt_one_of_gt, apply dec_trivial, apply inv_ge_of_le, - apply pnat.max_left, + apply le_max_left, apply pnat.inv_pos, apply rat.le_of_lt zero_lt_one, apply inv_ge_of_le, - apply pnat.max_right, + apply le_max_right, apply pnat.inv_pos, repeat (apply le_of_lt; apply pnat.inv_pos) end @@ -789,22 +789,22 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r rotate 1, apply add_le_add, apply HNt, - apply pnat.le_trans, + apply le.trans, apply pnat.mul_le_mul_left 2, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, - apply pnat.max_left, + apply le_max_left, apply HNu, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, - apply pnat.max_right, + apply le_max_right, rewrite [-pnat.add_halves Nt, -sub_eq_add_neg, add_sub_cancel], apply inv_ge_of_le, - apply pnat.max_left + apply le_max_left end theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) @@ -827,22 +827,22 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r rotate 1, apply add_le_add, apply HNt, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, - apply pnat.max_right, + apply le_max_right, apply HNu, - apply pnat.le_trans, + apply le.trans, apply pnat.mul_le_mul_left 2, - apply pnat.le_trans, + apply le.trans, rotate 1, apply Hn, rotate_right 1, - apply pnat.max_left, + apply le_max_left, rewrite [-pnat.add_halves Nu, neg_add_cancel_left], apply inv_ge_of_le, - apply pnat.max_left + apply le_max_left end theorem le_of_le_reprs {s t : seq} (Hs : regular s) (Ht : regular t) @@ -884,7 +884,7 @@ theorem nat_inv_lt_rat {a : ℚ} (H : a > 0) : ∃ n : ℕ+, n⁻¹ < a := apply div_two_lt_of_pos H, rewrite -(one_div_one_div (a / (1 + 1))), apply pceil_helper, - apply pnat.le_refl, + apply le.refl, apply one_div_pos_of_pos, apply div_pos_of_pos_of_pos H dec_trivial end