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

refactor(library/data/pnat): make pnat a decidable_linear_order

Browse source
This commit is contained in:
Gabriel Ebner 2016-06-17 12:03:31 +02:00 committed by Leonardo de Moura
parent e4071639f1
commit 53236718a8
5 changed files with 121 additions and 133 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
library/data/pnat.lean
View file

@ -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))

35
library/data/real/basic.lean
View file

@ -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
---------------------------------------------

44
library/data/real/complete.lean
View file

@ -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

44
library/data/real/division.lean
View file

@ -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

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

@ -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