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

chore(library/data/{pnat, real}): rename pnat theorems

Browse source
This commit is contained in:
Rob Lewis 2015-06-16 14:55:02 +10:00 committed by Leonardo de Moura
parent ff0ba6687e
commit 8d0518444d
5 changed files with 153 additions and 163 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

94
library/data/pnat.lean
View file

@ -13,7 +13,7 @@ are those needed for that construction.
import data.rat.order data.nat import data.rat.order data.nat
open nat rat open nat rat
section pnat namespace pnat
inductive pnat : Type := inductive pnat : Type :=
pos : Π n : nat, n > 0 → pnat pos : Π n : nat, n > 0 → pnat
@ -62,7 +62,7 @@ definition pnat_lt_decidable [instance] {p q : pnat} : decidable (p < q) :=
pnat.rec_on p (λ n H, pnat.rec_on q pnat.rec_on p (λ n H, pnat.rec_on q
(λ m H2, if Hl : n < m then decidable.inl Hl else decidable.inr Hl)) (λ m H2, if Hl : n < m then decidable.inl Hl else decidable.inr Hl))
theorem ple.trans {p q r : pnat} (H1 : p ≤ q) (H2 : q ≤ r) : p ≤ r := nat.le.trans H1 H2 theorem le.trans {p q r : pnat} (H1 : p ≤ q) (H2 : q ≤ r) : p ≤ r := nat.le.trans H1 H2
definition max (p q : pnat) := definition max (p q : pnat) :=
pnat.pos (nat.max (p~) (q~)) (nat.lt_of_lt_of_le (!nat_of_pnat_pos) (!le_max_right)) pnat.pos (nat.max (p~) (q~)) (nat.lt_of_lt_of_le (!nat_of_pnat_pos) (!le_max_right))
@ -79,35 +79,35 @@ theorem max_eq_left {a b : ℕ+} (H : ¬ a < b) : max a b = a :=
have Hnat : nat.max a~ b~ = a~, from nat.max_eq_left H, have Hnat : nat.max a~ b~ = a~, from nat.max_eq_left H,
pnat.eq Hnat pnat.eq Hnat
theorem pnat.le_of_lt {a b : ℕ+} (H : a < b) : a ≤ b := nat.le_of_lt H theorem le_of_lt {a b : ℕ+} (H : a < b) : a ≤ b := nat.le_of_lt H
theorem pnat.not_lt_of_le {a b : ℕ+} (H : a ≤ b) : ¬ (b < a) := nat.not_lt_of_ge H theorem not_lt_of_ge {a b : ℕ+} (H : a ≤ b) : ¬ (b < a) := nat.not_lt_of_ge H
theorem pnat.le_of_not_lt {a b : ℕ+} (H : ¬ a < b) : b ≤ a := nat.le_of_not_gt H theorem le_of_not_gt {a b : ℕ+} (H : ¬ a < b) : b ≤ a := nat.le_of_not_gt H
theorem pnat.eq_of_le_of_ge {a b : ℕ+} (H1 : a ≤ b) (H2 : b ≤ a) : a = b := theorem eq_of_le_of_ge {a b : ℕ+} (H1 : a ≤ b) (H2 : b ≤ a) : a = b :=
pnat.eq (nat.eq_of_le_of_ge H1 H2) pnat.eq (nat.eq_of_le_of_ge H1 H2)
theorem pnat.le.refl (a : ℕ+) : a ≤ a := !nat.le.refl theorem le.refl (a : ℕ+) : a ≤ a := !nat.le.refl
notation 2 := pnat.pos 2 dec_trivial notation 2 := pnat.pos 2 dec_trivial
notation 3 := pnat.pos 3 dec_trivial notation 3 := pnat.pos 3 dec_trivial
definition pone : pnat := pnat.pos 1 dec_trivial definition pone : pnat := pnat.pos 1 dec_trivial
definition pnat.to_rat [reducible] (n : ℕ+) : ℚ := definition rat_of_pnat [reducible] (n : ℕ+) : ℚ :=
pnat.rec_on n (λ n H, of_nat n) pnat.rec_on n (λ n H, of_nat n)
theorem pnat.to_rat_of_nat (n : ℕ+) : pnat.to_rat n = of_nat n~ := theorem pnat.to_rat_of_nat (n : ℕ+) : rat_of_pnat n = of_nat n~ :=
pnat.rec_on n (λ n H, rfl) pnat.rec_on n (λ n H, rfl)
-- these will come in rat -- these will come in rat
theorem rat_of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial theorem rat_of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial
theorem rat_of_pnat_ge_one (n : ℕ+) : pnat.to_rat n ≥ 1 := theorem rat_of_pnat_ge_one (n : ℕ+) : rat_of_pnat n ≥ 1 :=
pnat.rec_on n (λ m h, (iff.mp' !of_nat_le_of_nat) (succ_le_of_lt h)) pnat.rec_on n (λ m h, (iff.mp' !of_nat_le_of_nat) (succ_le_of_lt h))
theorem rat_of_pnat_is_pos (n : ℕ+) : pnat.to_rat n > 0 := theorem rat_of_pnat_is_pos (n : ℕ+) : rat_of_pnat n > 0 :=
pnat.rec_on n (λ m h, (iff.mp' !of_nat_pos) h) pnat.rec_on n (λ m h, (iff.mp' !of_nat_pos) h)
theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n := theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n :=
@ -116,25 +116,25 @@ theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : m ≤ n) : of_nat m ≤ of_nat n
theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : m < n) : of_nat m < of_nat n := theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : m < n) : of_nat m < of_nat n :=
(iff.mp' !of_nat_lt_of_nat) H (iff.mp' !of_nat_lt_of_nat) H
theorem pnat_le_to_rat_le {m n : ℕ+} (H : m ≤ n) : pnat.to_rat m ≤ pnat.to_rat n := theorem rat_of_pnat_le_of_pnat_le {m n : ℕ+} (H : m ≤ n) : rat_of_pnat m ≤ rat_of_pnat n :=
begin begin
rewrite *pnat.to_rat_of_nat, rewrite *pnat.to_rat_of_nat,
apply of_nat_le_of_nat_of_le H apply of_nat_le_of_nat_of_le H
end end
theorem pnat_lt_to_rat_lt {m n : ℕ+} (H : m < n) : pnat.to_rat m < pnat.to_rat n := theorem rat_of_pnat_lt_of_pnat_lt {m n : ℕ+} (H : m < n) : rat_of_pnat m < rat_of_pnat n :=
begin begin
rewrite *pnat.to_rat_of_nat, rewrite *pnat.to_rat_of_nat,
apply of_nat_lt_of_nat_of_lt H apply of_nat_lt_of_nat_of_lt H
end end
theorem rat_le_to_pnat_le {m n : ℕ+} (H : pnat.to_rat m ≤ pnat.to_rat n) : m ≤ n := theorem pnat_le_of_rat_of_pnat_le {m n : ℕ+} (H : rat_of_pnat m ≤ rat_of_pnat n) : m ≤ n :=
begin begin
rewrite *pnat.to_rat_of_nat at H, rewrite *pnat.to_rat_of_nat at H,
apply (iff.mp !of_nat_le_of_nat) H apply (iff.mp !of_nat_le_of_nat) H
end end
definition inv (n : ℕ+) : ℚ := (1 : ℚ) / pnat.to_rat n definition inv (n : ℕ+) : ℚ := (1 : ℚ) / rat_of_pnat n
postfix `⁻¹` := inv postfix `⁻¹` := inv
theorem inv_pos (n : ℕ+) : n⁻¹ > 0 := div_pos_of_pos !rat_of_pnat_is_pos theorem inv_pos (n : ℕ+) : n⁻¹ > 0 := div_pos_of_pos !rat_of_pnat_is_pos
@ -165,9 +165,7 @@ theorem add_invs_nonneg (m n : ℕ+) : 0 ≤ m⁻¹ + n⁻¹ :=
repeat apply inv_pos repeat apply inv_pos
end end
set_option pp.coercions true theorem one_mul (n : ℕ+) : pone * n = n :=
theorem pnat_one_mul (n : ℕ+) : pone * n = n :=
begin begin
apply pnat.eq, apply pnat.eq,
rewrite [↑pone, ↑mul, ↑nat_of_pnat, one_mul] rewrite [↑pone, ↑mul, ↑nat_of_pnat, one_mul]
@ -176,19 +174,19 @@ theorem pnat_one_mul (n : ℕ+) : pone * n = n :=
theorem pone_le (n : ℕ+) : pone ≤ n := theorem pone_le (n : ℕ+) : pone ≤ n :=
succ_le_of_lt (nat_of_pnat_pos n) succ_le_of_lt (nat_of_pnat_pos n)
theorem pnat_to_rat_mul (a b : ℕ+) : pnat.to_rat (a * b) = pnat.to_rat a * pnat.to_rat b := theorem pnat_to_rat_mul (a b : ℕ+) : rat_of_pnat (a * b) = rat_of_pnat a * rat_of_pnat b :=
by rewrite *pnat.to_rat_of_nat by rewrite *pnat.to_rat_of_nat
theorem mul_lt_mul_left (a b c : ℕ+) (H : a < b) : a * c < b * c := theorem mul_lt_mul_left (a b c : ℕ+) (H : a < b) : a * c < b * c :=
nat.mul_lt_mul_of_pos_right H !nat_of_pnat_pos nat.mul_lt_mul_of_pos_right H !nat_of_pnat_pos
theorem half_shrink_strong (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ := theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ :=
begin begin
rewrite ↑inv, rewrite ↑inv,
apply div_lt_div_of_lt, apply div_lt_div_of_lt,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
have H : n~ < (2 * n)~, begin have H : n~ < (2 * n)~, begin
rewrite -pnat_one_mul at {1}, rewrite -one_mul at {1},
apply mul_lt_mul_left, apply mul_lt_mul_left,
apply dec_trivial apply dec_trivial
end, end,
@ -197,24 +195,24 @@ theorem half_shrink_strong (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ :=
apply H apply H
end end
theorem half_shrink (n : ℕ+) : (2 * n)⁻¹ ≤ n⁻¹ := le_of_lt !half_shrink_strong theorem inv_two_mul_le_inv (n : ℕ+) : (2 * n)⁻¹ ≤ n⁻¹ := rat.le_of_lt !inv_two_mul_lt_inv
theorem inv_ge_of_le {p q : ℕ+} (H : p ≤ q) : q⁻¹ ≤ p⁻¹ := theorem inv_ge_of_le {p q : ℕ+} (H : p ≤ q) : q⁻¹ ≤ p⁻¹ :=
div_le_div_of_le !rat_of_pnat_is_pos (pnat_le_to_rat_le H) div_le_div_of_le !rat_of_pnat_is_pos (rat_of_pnat_le_of_pnat_le H)
theorem inv_gt_of_lt {p q : ℕ+} (H : p < q) : q⁻¹ < p⁻¹ := theorem inv_gt_of_lt {p q : ℕ+} (H : p < q) : q⁻¹ < p⁻¹ :=
div_lt_div_of_lt !rat_of_pnat_is_pos (pnat_lt_to_rat_lt H) div_lt_div_of_lt !rat_of_pnat_is_pos (rat_of_pnat_lt_of_pnat_lt H)
theorem ge_of_inv_le {p q : ℕ+} (H : p⁻¹ ≤ q⁻¹) : q ≤ p := theorem ge_of_inv_le {p q : ℕ+} (H : p⁻¹ ≤ q⁻¹) : q ≤ p :=
rat_le_to_pnat_le (le_of_div_le !rat_of_pnat_is_pos H) pnat_le_of_rat_of_pnat_le (le_of_div_le !rat_of_pnat_is_pos H)
theorem two_mul (p : ℕ+) : pnat.to_rat (2 * p) = (1 + 1) * pnat.to_rat p := theorem two_mul (p : ℕ+) : rat_of_pnat (2 * p) = (1 + 1) * rat_of_pnat p :=
by rewrite pnat_to_rat_mul by rewrite pnat_to_rat_mul
theorem padd_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ := theorem add_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ :=
begin begin
rewrite [↑inv, -(@add_halves (1 / (pnat.to_rat p))), *div_div_eq_div_mul'], rewrite [↑inv, -(@add_halves (1 / (rat_of_pnat p))), *div_div_eq_div_mul'],
have H : pnat.to_rat (2 * p) = pnat.to_rat p * (1 + 1), by rewrite [rat.mul.comm, two_mul], have H : rat_of_pnat (2 * p) = rat_of_pnat p * (1 + 1), by rewrite [rat.mul.comm, two_mul],
rewrite *H rewrite *H
end end
@ -222,14 +220,14 @@ theorem add_halves_double (m n : ℕ+) :
m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) := m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) :=
have simp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b), have simp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b),
by intros; rewrite [rat.add.assoc, -(rat.add.assoc a b b), {_+b}rat.add.comm, -*rat.add.assoc], by intros; rewrite [rat.add.assoc, -(rat.add.assoc a b b), {_+b}rat.add.comm, -*rat.add.assoc],
by rewrite [-padd_halves m, -padd_halves n, simp] by rewrite [-add_halves m, -add_halves n, simp]
theorem pnat_div_helper {p q : ℕ+} : (p * q)⁻¹ = p⁻¹ * q⁻¹ := theorem inv_mul_eq_mul_inv {p q : ℕ+} : (p * q)⁻¹ = p⁻¹ * q⁻¹ :=
by rewrite [↑inv, pnat_to_rat_mul, one_div_mul_one_div'''] by rewrite [↑inv, pnat_to_rat_mul, one_div_mul_one_div''']
theorem inv_mul_le_inv (p q : ℕ+) : (p * q)⁻¹ ≤ q⁻¹ := theorem inv_mul_le_inv (p q : ℕ+) : (p * q)⁻¹ ≤ q⁻¹ :=
begin begin
rewrite [pnat_div_helper, -{q⁻¹}rat.one_mul at {2}], rewrite [inv_mul_eq_mul_inv, -{q⁻¹}rat.one_mul at {2}],
apply rat.mul_le_mul, apply rat.mul_le_mul,
apply inv_le_one, apply inv_le_one,
apply rat.le.refl, apply rat.le.refl,
@ -239,39 +237,39 @@ theorem inv_mul_le_inv (p q : ℕ+) : (p * q)⁻¹ ≤ q⁻¹ :=
end end
theorem pnat_mul_le_mul_left' (a b c : ℕ+) (H : a ≤ b) : c * a ≤ c * b := theorem pnat_mul_le_mul_left' (a b c : ℕ+) (H : a ≤ b) : c * a ≤ c * b :=
nat.mul_le_mul_of_nonneg_left H (le_of_lt !nat_of_pnat_pos) nat.mul_le_mul_of_nonneg_left H (nat.le_of_lt !nat_of_pnat_pos)
theorem pnat_mul_assoc (a b c : ℕ+) : a * b * c = a * (b * c) := theorem mul.assoc (a b c : ℕ+) : a * b * c = a * (b * c) :=
pnat.eq !nat.mul.assoc pnat.eq !nat.mul.assoc
theorem pnat_mul_comm (a b : ℕ+) : a * b = b * a := theorem mul.comm (a b : ℕ+) : a * b = b * a :=
pnat.eq !nat.mul.comm pnat.eq !nat.mul.comm
theorem pnat_add_assoc (a b c : ℕ+) : a + b + c = a + (b + c) := theorem add.assoc (a b c : ℕ+) : a + b + c = a + (b + c) :=
pnat.eq !nat.add.assoc pnat.eq !nat.add.assoc
theorem pnat.mul_le_mul_left (p q : ℕ+) : q ≤ p * q := theorem mul_le_mul_left (p q : ℕ+) : q ≤ p * q :=
begin begin
rewrite [-pnat_one_mul at {1}, pnat_mul_comm, pnat_mul_comm p], rewrite [-one_mul at {1}, mul.comm, mul.comm p],
apply pnat_mul_le_mul_left', apply pnat_mul_le_mul_left',
apply pone_le apply pone_le
end end
theorem pnat.mul_le_mul_right (p q : ℕ+) : p ≤ p * q := theorem mul_le_mul_right (p q : ℕ+) : p ≤ p * q :=
by rewrite pnat_mul_comm; apply pnat.mul_le_mul_left by rewrite mul.comm; apply mul_le_mul_left
theorem one_lt_two : pone < 2 := dec_trivial theorem one_lt_two : pone < 2 := dec_trivial
theorem pnat.lt_of_not_le {p q : ℕ+} (H : ¬ p ≤ q) : q < p := theorem pnat.lt_of_not_le {p q : ℕ+} (H : ¬ p ≤ q) : q < p :=
nat.lt_of_not_ge H nat.lt_of_not_ge H
theorem pnat.inv_cancel (p : ℕ+) : pnat.to_rat p * p⁻¹ = (1 : ℚ) := theorem inv_cancel_left (p : ℕ+) : rat_of_pnat p * p⁻¹ = (1 : ℚ) :=
mul_one_div_cancel (ne.symm (rat.ne_of_lt !rat_of_pnat_is_pos)) mul_one_div_cancel (ne.symm (rat.ne_of_lt !rat_of_pnat_is_pos))
theorem pnat.inv_cancel_right (p : ℕ+) : p⁻¹ * pnat.to_rat p = (1 : ℚ) := theorem inv_cancel_right (p : ℕ+) : p⁻¹ * rat_of_pnat p = (1 : ℚ) :=
by rewrite rat.mul.comm; apply pnat.inv_cancel by rewrite rat.mul.comm; apply inv_cancel_left
theorem pnat_lt_add_left (p q : ℕ+) : p < p + q := theorem lt_add_left (p q : ℕ+) : p < p + q :=
begin begin
have H : p~ < p~ + q~, begin have H : p~ < p~ + q~, begin
rewrite -nat.add_zero at {1}, rewrite -nat.add_zero at {1},
@ -282,9 +280,9 @@ theorem pnat_lt_add_left (p q : ℕ+) : p < p + q :=
end end
theorem inv_add_lt_left (p q : ℕ+) : (p + q)⁻¹ < p⁻¹ := theorem inv_add_lt_left (p q : ℕ+) : (p + q)⁻¹ < p⁻¹ :=
by apply inv_gt_of_lt; apply pnat_lt_add_left by apply inv_gt_of_lt; apply lt_add_left
theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ pnat.to_rat n := theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ rat_of_pnat n :=
begin begin
apply rat.div_le_of_le_mul, apply rat.div_le_of_le_mul,
apply rat.lt_of_lt_of_le, apply rat.lt_of_lt_of_le,
@ -296,10 +294,10 @@ theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ pnat.to_
apply H apply H
end end
theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (pnat.to_rat n * pnat.to_rat n) = m⁻¹ := theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_pnat n) = m⁻¹ :=
begin begin
have simp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from sorry, -- simp have simp : ∀ a b c : ℚ, (a * a * (b * b * c)) = (a * b) * (a * b) * c, from sorry, -- simp
rewrite [rat.mul.comm, *pnat_div_helper, simp, *pnat.inv_cancel, *rat.one_mul] rewrite [rat.mul.comm, *inv_mul_eq_mul_inv, simp, *inv_cancel_left, *rat.one_mul]
end end

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

@ -99,7 +99,7 @@ theorem rewrite_helper7 (a b c d x : ℚ) :
theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹)
(H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) : (H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) :
(pnat.to_rat k) * a + b * (pnat.to_rat k) ≤ m⁻¹ + n⁻¹ := sorry (rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ := sorry
theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) := theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) :=
sorry sorry
@ -144,7 +144,7 @@ theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
intros [j, n, Hn], intros [j, n, Hn],
apply rat.le.trans, apply rat.le.trans,
apply H n, apply H n,
rewrite -(padd_halves j), rewrite -(add_halves j),
apply rat.add_le_add, apply rat.add_le_add,
apply inv_ge_of_le Hn, apply inv_ge_of_le Hn,
apply inv_ge_of_le Hn apply inv_ge_of_le Hn
@ -206,7 +206,7 @@ theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε :=
existsi (pceil (1 / ε)), existsi (pceil (1 / ε)),
rewrite -(rat.div_div (rat.ne_of_gt Hε)) at {2}, rewrite -(rat.div_div (rat.ne_of_gt Hε)) at {2},
apply pceil_helper, apply pceil_helper,
apply pnat.le.refl apply le.refl
end end
theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) : theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
@ -235,7 +235,7 @@ theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regula
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn, have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn,
have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn, have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn,
rewrite -(padd_halves j), rewrite -(add_halves j),
apply rat.add_le_add, apply rat.add_le_add,
repeat assumption repeat assumption
end end
@ -245,7 +245,7 @@ theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regula
definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial
theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ pnat.to_rat (K s) := theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
calc calc
abs (s n) = abs (s n - s pone + s pone) : by rewrite rat.sub_add_cancel abs (s n) = abs (s n - s pone + s pone) : by rewrite rat.sub_add_cancel
... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs ... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs
@ -263,7 +263,7 @@ definition K₂ (s t : seq) := max (K s) (K t)
theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s := theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
if H : K s < K t then if H : K s < K t then
(have H1 [visible] : K₂ s t = K t, from max_eq_right H, (have H1 [visible] : K₂ s t = K t, from max_eq_right H,
have H2 [visible] : K₂ t s = K t, from max_eq_left (pnat.not_lt_of_le (pnat.le_of_lt H)), have H2 [visible] : K₂ t s = K t, from max_eq_left (not_lt_of_ge (le_of_lt H)),
by rewrite [H1, -H2]) by rewrite [H1, -H2])
else else
(have H1 [visible] : K₂ s t = K s, from max_eq_left H, (have H1 [visible] : K₂ s t = K s, from max_eq_left H,
@ -271,20 +271,20 @@ theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
(have H2 [visible] : K₂ t s = K s, from max_eq_right J, by rewrite [H1, -H2]) (have H2 [visible] : K₂ t s = K s, from max_eq_right J, by rewrite [H1, -H2])
else else
(have Heq [visible] : K t = K s, from (have Heq [visible] : K t = K s, from
pnat.eq_of_le_of_ge (pnat.le_of_not_lt H) (pnat.le_of_not_lt J), eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt J),
by rewrite [↑K₂, Heq])) by rewrite [↑K₂, Heq]))
theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) : theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) :
abs (s n) ≤ pnat.to_rat (K₂ s t) := abs (s n) ≤ rat_of_pnat (K₂ s t) :=
calc calc
abs (s n) ≤ pnat.to_rat (K s) : canon_bound Hs n abs (s n) ≤ rat_of_pnat (K s) : canon_bound Hs n
... ≤ pnat.to_rat (K₂ s t) : pnat_le_to_rat_le (!max_left) ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!max_left)
theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) : theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) :
abs (t n) ≤ pnat.to_rat (K₂ s t) := abs (t n) ≤ rat_of_pnat (K₂ s t) :=
calc calc
abs (t n) ≤ pnat.to_rat (K t) : canon_bound Ht n abs (t n) ≤ rat_of_pnat (K t) : canon_bound Ht n
... ≤ pnat.to_rat (K₂ s t) : pnat_le_to_rat_le (!max_right) ... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!max_right)
definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n)) definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n))
@ -361,8 +361,8 @@ theorem s_add_assoc (s t u : seq) (Hs : regular s) (Hu : regular u) :
apply rat.le.trans, apply rat.le.trans,
rotate 1, rotate 1,
apply rat.add_le_add_right, apply rat.add_le_add_right,
apply half_shrink, apply inv_two_mul_le_inv,
rewrite [-(padd_halves (2 * n)), -(padd_halves n), factor_lemma_2], rewrite [-(add_halves (2 * n)), -(add_halves n), factor_lemma_2],
apply rat.add_le_add, apply rat.add_le_add,
apply Hs, apply Hs,
apply Hu apply Hu
@ -406,7 +406,7 @@ theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
apply abs_nonneg apply abs_nonneg
end end
definition Kq (s : seq) := pnat.to_rat (K s) + 1 definition Kq (s : seq) := rat_of_pnat (K s) + 1
theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s := theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :=
begin begin
intros, intros,
@ -421,7 +421,7 @@ theorem Kq_bound_nonneg {s : seq} (H : regular s) : 0 ≤ Kq s :=
rat.le.trans !abs_nonneg (Kq_bound H 2) rat.le.trans !abs_nonneg (Kq_bound H 2)
theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s := theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
have H1 : 0 ≤ pnat.to_rat (K s), from rat.le.trans (!abs_nonneg) (canon_bound H 2), have H1 : 0 ≤ rat_of_pnat (K s), from rat.le.trans (!abs_nonneg) (canon_bound H 2),
add_pos_of_nonneg_of_pos H1 rat.zero_lt_one add_pos_of_nonneg_of_pos H1 rat.zero_lt_one
theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
@ -492,7 +492,7 @@ theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regula
fapply exists.intro, fapply exists.intro,
rotate 1, rotate 1,
intros, intros,
rewrite [↑smul, *DK_rewrite, *TK_rewrite, -*pnat_mul_assoc, -*rat.mul.assoc], rewrite [↑smul, *DK_rewrite, *TK_rewrite, -*pnat.mul.assoc, -*rat.mul.assoc],
apply rat.le.trans, apply rat.le.trans,
apply s_mul_assoc_lemma, apply s_mul_assoc_lemma,
apply rat.le.trans, apply rat.le.trans,
@ -538,7 +538,7 @@ theorem s_zero_add (s : seq) (H : regular s) : sadd zero s ≡ s :=
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
apply rat.add_le_add, apply rat.add_le_add,
apply half_shrink, apply inv_two_mul_le_inv,
apply rat.le.refl apply rat.le.refl
end end
@ -550,7 +550,7 @@ theorem s_add_zero (s : seq) (H : regular s) : sadd s zero ≡ s :=
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
apply rat.add_le_add, apply rat.add_le_add,
apply half_shrink, apply inv_two_mul_le_inv,
apply rat.le.refl apply rat.le.refl
end end
@ -594,16 +594,16 @@ theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) : theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) :
∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ := ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ :=
begin begin
existsi pceil (((pnat.to_rat (K s)) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * existsi pceil (((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) *
(pnat.to_rat (K t))) * (pnat.to_rat j)), (rat_of_pnat (K t))) * (rat_of_pnat j)),
intros n Hn, intros n Hn,
rewrite rewrite_helper4, rewrite rewrite_helper4,
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.le.trans, apply rat.le.trans,
rotate 1, rotate 1,
show n⁻¹ * ((pnat.to_rat (K s)) * (b⁻¹ + c⁻¹)) + show n⁻¹ * ((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹)) +
n⁻¹ * ((a⁻¹ + c⁻¹) * (pnat.to_rat (K t))) ≤ j⁻¹, begin n⁻¹ * ((a⁻¹ + c⁻¹) * (rat_of_pnat (K t))) ≤ j⁻¹, begin
rewrite -rat.left_distrib, rewrite -rat.left_distrib,
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_right, apply rat.mul_le_mul_of_nonneg_right,
@ -631,7 +631,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
apply abs_nonneg, apply abs_nonneg,
apply rat.le_of_lt, apply rat.le_of_lt,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
rewrite [*pnat_div_helper, -rat.right_distrib, -rat.mul.assoc, rat.mul.comm], rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, -rat.mul.assoc, rat.mul.comm],
apply rat.mul_le_mul_of_nonneg_left, apply rat.mul_le_mul_of_nonneg_left,
apply rat.le.refl, apply rat.le.refl,
apply rat.le_of_lt, apply rat.le_of_lt,
@ -644,7 +644,7 @@ theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c :
apply Ht, apply Ht,
apply abs_nonneg, apply abs_nonneg,
apply add_invs_nonneg, apply add_invs_nonneg,
rewrite [*pnat_div_helper, -rat.right_distrib, mul.comm _ n⁻¹, rat.mul.assoc], rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, mul.comm _ n⁻¹, rat.mul.assoc],
apply rat.mul_le_mul, apply rat.mul_le_mul,
apply rat.le.refl, apply rat.le.refl,
apply rat.le.refl, apply rat.le.refl,
@ -661,16 +661,7 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular
smul s (sadd t u) ≡ sadd (smul s t) (smul s u) := smul s (sadd t u) ≡ sadd (smul s t) (smul s u) :=
begin begin
apply eq_of_bdd, apply eq_of_bdd,
apply reg_mul_reg, repeat (assumption | apply reg_add_reg | apply reg_mul_reg),
assumption,
apply reg_add_reg,
repeat assumption,
apply reg_add_reg,
repeat assumption,
apply reg_mul_reg,
repeat assumption,
apply reg_mul_reg,
repeat assumption,
intros, intros,
let exh1 := λ a b c, mul_bound_helper Hs Ht a b c (2 * j), let exh1 := λ a b c, mul_bound_helper Hs Ht a b c (2 * j),
apply exists.elim, apply exists.elim,
@ -684,16 +675,16 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular
intros N2 HN2, intros N2 HN2,
existsi max N1 N2, existsi max N1 N2,
intros n Hn, intros n Hn,
rewrite [↑sadd at *, ↑smul, rewrite_helper3, -padd_halves j, -*pnat_mul_assoc at *], rewrite [↑sadd at *, ↑smul, rewrite_helper3, -add_halves j, -*pnat.mul.assoc at *],
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.add_le_add, apply rat.add_le_add,
apply HN1, apply HN1,
apply ple.trans, apply le.trans,
apply max_left N1 N2, apply max_left N1 N2,
apply Hn, apply Hn,
apply HN2, apply HN2,
apply ple.trans, apply le.trans,
apply max_right N1 N2, apply max_right N1 N2,
apply Hn apply Hn
end end
@ -717,7 +708,7 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
apply Kq_bound Hs, apply Kq_bound Hs,
let HN' := λ n, (!rat.sub_zero ▸ HN n), let HN' := λ n, (!rat.sub_zero ▸ HN n),
apply HN', apply HN',
apply ple.trans Hn, apply le.trans Hn,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
apply abs_nonneg, apply abs_nonneg,
apply rat.le_of_lt (Kq_bound_pos Hs), apply rat.le_of_lt (Kq_bound_pos Hs),
@ -761,10 +752,10 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
let He' := λ a b c, !rat.sub_zero ▸ (He a b c), let He' := λ a b c, !rat.sub_zero ▸ (He a b c),
apply (He' _ _ Hn), apply (He' _ _ Hn),
apply Ht, apply Ht,
rewrite [simp, padd_halves, -(padd_halves j), -(padd_halves (2 * j)), -*rat.add.assoc], rewrite [simp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc],
apply rat.add_le_add_right, apply rat.add_le_add_right,
apply add_le_add_three, apply add_le_add_three,
repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply half_shrink) repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv)
end end
theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero := theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero :=
@ -913,13 +904,13 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
intro Hz, intro Hz,
rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz], rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz],
let H := Hz (2 * 2), let H := Hz (2 * 2),
rewrite [rat.zero_sub at H, abs_neg at H, padd_halves at H], rewrite [rat.zero_sub at H, abs_neg at H, add_halves at H],
have H' : pone⁻¹ ≤ 2⁻¹, from calc have H' : pone⁻¹ ≤ 2⁻¹, from calc
pone⁻¹ = 1 : by rewrite -pone_inv pone⁻¹ = 1 : by rewrite -pone_inv
... = abs 1 : abs_of_pos zero_lt_one ... = abs 1 : abs_of_pos zero_lt_one
... ≤ 2⁻¹ : H, ... ≤ 2⁻¹ : H,
let H'' := ge_of_inv_le H', let H'' := ge_of_inv_le H',
apply absurd (one_lt_two) (pnat.not_lt_of_le H'') apply absurd (one_lt_two) (not_lt_of_ge H'')
end end
--------------------------------------------- ---------------------------------------------

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

@ -11,13 +11,14 @@ At this point, we no longer proceed constructively: this file makes heavy use of
Here, we show that ℝ is complete. Here, we show that ℝ is complete.
-/ -/
import data.real.basic data.real.order data.real.division data.rat data.nat logic.axioms.classical import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat logic.axioms.classical
open -[coercions] rat open -[coercions] rat
local notation 0 := rat.of_num 0 local notation 0 := rat.of_num 0
local notation 1 := rat.of_num 1 local notation 1 := rat.of_num 1
open -[coercions] nat open -[coercions] nat
open algebra open algebra
open eq.ops open eq.ops
open pnat
local notation 2 := pnat.pos (nat.of_num 2) dec_trivial local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
@ -47,7 +48,7 @@ theorem rat_approx_l1 {s : seq} (H : regular s) :
intro m Hm, intro m Hm,
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
rewrite -(padd_halves n), rewrite -(add_halves n),
apply rat.add_le_add_right, apply rat.add_le_add_right,
apply inv_ge_of_le Hm apply inv_ge_of_le Hm
end end
@ -73,9 +74,9 @@ theorem rat_approx {s : seq} (H : regular s) :
rotate 1, rotate 1,
apply rat.sub_le_sub_left, apply rat.sub_le_sub_left,
apply HN, apply HN,
apply ple.trans, apply pnat.le.trans,
apply Hp, apply Hp,
rewrite -*pnat_mul_assoc, rewrite -*pnat.mul.assoc,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
rewrite [sub_self, -neg_zero], rewrite [sub_self, -neg_zero],
apply neg_le_neg, apply neg_le_neg,
@ -112,7 +113,7 @@ theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : s_le (s_abs (sadd s
apply rat.le.trans, apply rat.le.trans,
apply Hs, apply Hs,
apply rat.add_le_add_right, apply rat.add_le_add_right,
rewrite -*pnat_mul_assoc, rewrite -*pnat.mul.assoc,
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat.mul_le_mul_left apply pnat.mul_le_mul_left
end end
@ -185,7 +186,7 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
apply rat.le.trans, apply rat.le.trans,
apply rat.add_le_add, apply rat.add_le_add,
repeat (apply inv_ge_of_le; apply Hn), repeat (apply inv_ge_of_le; apply Hn),
rewrite padd_halves, rewrite pnat.add_halves,
apply rat.le.refl apply rat.le.refl
end end
@ -217,7 +218,7 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
apply rat.le.trans, apply rat.le.trans,
apply rat.add_le_add, apply rat.add_le_add,
repeat (apply inv_ge_of_le; apply Hn), repeat (apply inv_ge_of_le; apply Hn),
rewrite padd_halves, rewrite pnat.add_halves,
apply rat.le.refl, apply rat.le.refl,
intro Hneg, intro Hneg,
let Hneg' := lt_of_not_ge Hneg, let Hneg' := lt_of_not_ge Hneg,
@ -253,7 +254,7 @@ theorem add_consts (a b : ℚ) : const a + const b = const (a + b) :=
theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts
theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) :=
by rewrite [add_consts, padd_halves] by rewrite [add_consts, pnat.add_halves]
theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b := theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b :=
s.r_const_le_const_of_le s.r_const_le_const_of_le
@ -353,10 +354,10 @@ theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m
rotate 1, rotate 1,
apply Nb_spec_right, apply Nb_spec_right,
rotate 1, rotate 1,
apply ple.trans, apply pnat.le.trans,
apply Hmn, apply Hmn,
apply Nb_spec_right, apply Nb_spec_right,
rewrite [*add_consts, rat.add.assoc, padd_halves], rewrite [*add_consts, rat.add.assoc, pnat.add_halves],
apply const_le_const_of_le, apply const_le_const_of_le,
apply rat.add_le_add_right, apply rat.add_le_add_right,
apply inv_ge_of_le, apply inv_ge_of_le,
@ -421,18 +422,18 @@ theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
apply algebra.le.trans, apply algebra.le.trans,
apply algebra.add_le_add_three, apply algebra.add_le_add_three,
apply Hc, apply Hc,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply Nb_spec_right, apply Nb_spec_right,
have HMk : M (2 * k) ≤ Nb M n, begin have HMk : M (2 * k) ≤ Nb M n, begin
apply ple.trans, apply pnat.le.trans,
apply Nb_spec_right, apply Nb_spec_right,
apply ple.trans, apply pnat.le.trans,
apply Hn, apply Hn,
apply ple.trans, apply pnat.le.trans,
apply pnat.mul_le_mul_left 3, apply mul_le_mul_left 3,
apply Nb_spec_left apply Nb_spec_left
end, end,
apply HMk, apply HMk,
@ -446,18 +447,18 @@ theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
apply rat.le.refl, apply rat.le.refl,
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat_mul_le_mul_left', apply pnat_mul_le_mul_left',
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply Nb_spec_left, apply Nb_spec_left,
apply inv_ge_of_le, apply inv_ge_of_le,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply Nb_spec_left, apply Nb_spec_left,
rewrite [-*pnat_mul_assoc, p_add_fractions], rewrite [-*pnat.mul.assoc, p_add_fractions],
apply rat.le.refl apply rat.le.refl
end end

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

@ -157,7 +157,7 @@ theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n :
begin begin
apply eq.trans, apply eq.trans,
apply dif_pos Hsep, apply dif_pos Hsep,
apply dif_neg (pnat.not_lt_of_le Hn) apply dif_neg (pnat.not_lt_of_ge Hn)
end end
theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+} theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
@ -170,7 +170,7 @@ theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
s_inv_of_sep_gt_p Hs (sep_zero_of_pos Hs Hpos) Hn s_inv_of_sep_gt_p Hs (sep_zero_of_pos Hs Hpos) Hn
theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) : theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
abs (s_inv Hs n) ≤ (pnat.to_rat (ps Hs Hsep)) := abs (s_inv Hs n) ≤ (rat_of_pnat (ps Hs Hsep)) :=
if Hn : n < ps Hs Hsep then if Hn : n < ps Hs Hsep then
(begin (begin
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hn), abs_one_div], rewrite [(s_inv_of_sep_lt_p Hs Hsep Hn), abs_one_div],
@ -183,7 +183,7 @@ theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
rewrite [(s_inv_of_sep_gt_p Hs Hsep (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 div_le_pnat,
apply ps_spec, apply ps_spec,
rewrite pnat_mul_assoc, rewrite pnat.mul.assoc,
apply pnat.mul_le_mul_right apply pnat.mul_le_mul_right
end) end)
@ -217,13 +217,13 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
rewrite ↑regular, rewrite ↑regular,
intros, intros,
have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from
s_ne_zero_of_ge_p Hs Hsep !pnat.mul_le_mul_left, s_ne_zero_of_ge_p Hs Hsep !mul_le_mul_left,
have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from
s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * n ≥ ps Hs Hsep, by s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * n ≥ ps Hs Hsep, by
rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right), rewrite pnat.mul.assoc; apply pnat.mul_le_mul_right),
have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from
s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * m ≥ ps Hs Hsep, by s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * m ≥ ps Hs Hsep, by
rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right), rewrite pnat.mul.assoc; apply pnat.mul_le_mul_right),
apply @decidable.cases_on (m < (ps Hs Hsep)) _ _, apply @decidable.cases_on (m < (ps Hs Hsep)) _ _,
intro Hmlt, intro Hmlt,
apply @decidable.cases_on (n < (ps Hs Hsep)) _ _, apply @decidable.cases_on (n < (ps Hs Hsep)) _ _,
@ -233,7 +233,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply add_invs_nonneg, apply add_invs_nonneg,
intro Hnlt, intro Hnlt,
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt), rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt 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], rewrite [(div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply rat.mul_le_mul,
@ -242,7 +242,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply rat.mul_le_mul, apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt), rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hnlt)), rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
apply abs_nonneg, apply abs_nonneg,
apply le_of_lt !rat_of_pnat_is_pos, apply le_of_lt !rat_of_pnat_is_pos,
@ -257,14 +257,14 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply @decidable.cases_on (n < (ps Hs Hsep)) _ _, apply @decidable.cases_on (n < (ps Hs Hsep)) _ _,
intro Hnlt, intro Hnlt,
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hnlt), rewrite [(s_inv_of_sep_lt_p Hs Hsep Hnlt),
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt 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], rewrite [(div_sub_div Hspm Hsp), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply rat.mul_le_mul,
apply Hs, apply Hs,
xrewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul], xrewrite [-(mul_one 1), -(div_mul_div Hspm Hsp), abs_mul],
apply rat.mul_le_mul, apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hmlt)), rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_lt_p Hs Hsep Hnlt), rewrite -(s_inv_of_sep_lt_p Hs Hsep Hnlt),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
@ -278,17 +278,17 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply pnat.le_of_lt, apply pnat.le_of_lt,
apply Hnlt, apply Hnlt,
intro Hnlt, intro Hnlt,
rewrite [(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hnlt)), rewrite [(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hmlt))], (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], rewrite [(div_sub_div Hspm Hspn), div_eq_mul_one_div, abs_mul, *one_mul, *mul_one],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply rat.mul_le_mul,
apply Hs, apply Hs,
xrewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul], xrewrite [-(mul_one 1), -(div_mul_div Hspm Hspn), abs_mul],
apply rat.mul_le_mul, apply rat.mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hmlt)), rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hmlt)),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hnlt)), rewrite -(s_inv_of_sep_gt_p Hs Hsep (le_of_not_gt Hnlt)),
apply le_ps Hs Hsep, apply le_ps Hs Hsep,
apply abs_nonneg, apply abs_nonneg,
apply le_of_lt !rat_of_pnat_is_pos, apply le_of_lt !rat_of_pnat_is_pos,
@ -304,7 +304,7 @@ 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), rewrite (s_inv_of_sep_gt_p Hs Hsep H),
apply one_div_ne_zero, apply one_div_ne_zero,
apply s_ne_zero_of_ge_p, apply s_ne_zero_of_ge_p,
apply ple.trans, apply pnat.le.trans,
apply H, apply H,
apply pnat.mul_le_mul_left apply pnat.mul_le_mul_left
end) end)
@ -333,40 +333,40 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
apply Rsi, apply Rsi,
apply abs_nonneg, apply abs_nonneg,
have Hp : (K₂ s (s_inv Hs)) * 2 * n ≥ ps Hs Hsep, begin have Hp : (K₂ s (s_inv Hs)) * 2 * n ≥ ps Hs Hsep, begin
apply ple.trans, apply pnat.le.trans,
apply max_left, apply max_left,
rotate 1, rotate 1,
apply ple.trans, apply pnat.le.trans,
apply Hn, apply Hn,
apply pnat.mul_le_mul_left apply pnat.mul_le_mul_left
end, end,
have Hnz' : s (((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n)) ≠ 0, from have Hnz' : s (((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n)) ≠ 0, from
s_ne_zero_of_ge_p Hs Hsep s_ne_zero_of_ge_p Hs Hsep
(show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n), (show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n),
by rewrite *pnat_mul_assoc; apply pnat.mul_le_mul_right), by rewrite *pnat.mul.assoc; apply pnat.mul_le_mul_right),
xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')], xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_left, apply rat.mul_le_mul_of_nonneg_left,
apply Hs, apply Hs,
apply le_of_lt, apply le_of_lt,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
xrewrite [rat.mul.left_distrib, pnat_mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat_mul_assoc, xrewrite [rat.mul.left_distrib, mul.comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul.assoc,
*(@pnat_div_helper (K₂ s (s_inv Hs))), -*rat.mul.assoc, *pnat.inv_cancel, *(@inv_mul_eq_mul_inv (K₂ s (s_inv Hs))), -*rat.mul.assoc, *inv_cancel_left,
*one_mul, -(padd_halves j)], *one_mul, -(add_halves j)],
apply rat.add_le_add, apply rat.add_le_add,
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat_mul_le_mul_left', apply pnat_mul_le_mul_left',
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply max_right, apply max_right,
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat_mul_le_mul_left', apply pnat_mul_le_mul_left',
apply ple.trans, apply pnat.le.trans,
apply max_right, apply max_right,
rotate 1, rotate 1,
apply ple.trans, apply pnat.le.trans,
apply Hn, apply Hn,
apply pnat.mul_le_mul_right apply pnat.mul_le_mul_right
end end

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

@ -82,7 +82,7 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (
apply inv_add_lt_left, apply inv_add_lt_left,
apply HN, apply HN,
apply pnat.le_of_lt, apply pnat.le_of_lt,
apply pnat_lt_add_left apply lt_add_left
end end
theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) : theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
@ -149,13 +149,13 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
rotate 1, rotate 1,
apply ge_sub_of_abs_sub_le_right, apply ge_sub_of_abs_sub_le_right,
apply Heq, apply Heq,
have Hs4 : N⁻¹ ≤ s (2 * 2 * N), from HN _ (!pnat.mul_le_mul_left), have Hs4 : N⁻¹ ≤ s (2 * 2 * N), from HN _ (!mul_le_mul_left),
apply lt_of_lt_of_le, apply lt_of_lt_of_le,
rotate 1, rotate 1,
apply iff.mp' (rat.add_le_add_right_iff _ _ _), apply iff.mp' (rat.add_le_add_right_iff _ _ _),
apply Hs4, apply Hs4,
rewrite [*pnat_mul_assoc, padd_halves, -(padd_halves N), rat.add_sub_cancel], rewrite [*pnat.mul.assoc, pnat.add_halves, -(add_halves N), rat.add_sub_cancel],
apply half_shrink_strong apply inv_two_mul_lt_inv
end end
@ -178,14 +178,14 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
rotate 1, rotate 1,
apply rat.sub_le_sub_right, apply rat.sub_le_sub_right,
apply HNs, apply HNs,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hm, apply Hm,
rotate_right 1, rotate_right 1,
apply max_left, apply max_left,
have Hms : m⁻¹ ≤ (2 * 2 * n)⁻¹, begin have Hms : m⁻¹ ≤ (2 * 2 * n)⁻¹, begin
apply inv_ge_of_le, apply inv_ge_of_le,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hm; apply Hm;
apply max_right apply max_right
@ -195,10 +195,10 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
rotate 1, rotate 1,
apply rat.sub_le_sub_left, apply rat.sub_le_sub_left,
apply Hms', apply Hms',
rewrite [*pnat_mul_assoc, padd_halves, -neg_add, -padd_halves n], rewrite [*pnat.mul.assoc, pnat.add_halves, -neg_add, -add_halves n],
apply neg_le_neg, apply neg_le_neg,
apply rat.add_le_add_right, apply rat.add_le_add_right,
apply half_shrink apply inv_two_mul_le_inv
end end
definition s_le (a b : seq) := nonneg (sadd b (sneg a)) definition s_le (a b : seq) := nonneg (sadd b (sneg a))
@ -336,7 +336,7 @@ theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonne
begin begin
rewrite [↑nonneg at *, ↑sadd], rewrite [↑nonneg at *, ↑sadd],
intros, intros,
rewrite [-padd_halves, neg_add], rewrite [-pnat.add_halves, neg_add],
apply add_le_add, apply add_le_add,
apply Hs, apply Hs,
apply Ht apply Ht
@ -530,27 +530,27 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
rotate 1, rotate 1,
apply rat.mul_le_mul, apply rat.mul_le_mul,
apply HNs, apply HNs,
apply ple.trans, apply pnat.le.trans,
apply max_left Ns Nt, apply max_left Ns Nt,
rewrite -pnat_mul_assoc, rewrite -pnat.mul.assoc,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
apply HNt, apply HNt,
apply ple.trans, apply pnat.le.trans,
apply max_right Ns Nt, apply max_right Ns Nt,
rewrite -pnat_mul_assoc, rewrite -pnat.mul.assoc,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
apply le_of_lt, apply le_of_lt,
apply inv_pos, apply inv_pos,
apply rat.le.trans, apply rat.le.trans,
rotate 1, rotate 1,
apply HNs, apply HNs,
apply ple.trans, apply pnat.le.trans,
apply max_left Ns Nt, apply max_left Ns Nt,
rewrite -pnat_mul_assoc, rewrite -pnat.mul.assoc,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
rewrite pnat_div_helper, rewrite inv_mul_eq_mul_inv,
apply rat.mul_lt_mul, apply rat.mul_lt_mul,
rewrite [pnat_div_helper, -one_mul Ns⁻¹], rewrite [inv_mul_eq_mul_inv, -one_mul Ns⁻¹],
apply rat.mul_lt_mul, apply rat.mul_lt_mul,
apply inv_lt_one_of_gt, apply inv_lt_one_of_gt,
apply dec_trivial, apply dec_trivial,
@ -652,7 +652,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
rotate 1, rotate 1,
rewrite -neg_mul_eq_mul_neg, rewrite -neg_mul_eq_mul_neg,
apply neg_le_neg, apply neg_le_neg,
rewrite [*pnat_mul_assoc, pnat_div_helper, -mul.assoc, pnat.inv_cancel, one_mul], rewrite [*pnat.mul.assoc, inv_mul_eq_mul_inv, -mul.assoc, inv_cancel_left, one_mul],
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
intro Hsn, intro Hsn,
@ -675,7 +675,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
rotate 1, rotate 1,
rewrite -neg_mul_eq_neg_mul, rewrite -neg_mul_eq_neg_mul,
apply neg_le_neg, apply neg_le_neg,
rewrite [*pnat_mul_assoc, pnat_div_helper, mul.comm, -mul.assoc, pnat.inv_cancel, one_mul], rewrite [*pnat.mul.assoc, inv_mul_eq_mul_inv, mul.comm, -mul.assoc, inv_cancel_left, one_mul],
apply inv_ge_of_le, apply inv_ge_of_le,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
intro Htn, intro Htn,
@ -832,20 +832,20 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rotate 1, rotate 1,
apply rat.add_le_add, apply rat.add_le_add,
apply HNt, apply HNt,
apply ple.trans, apply pnat.le.trans,
apply pnat.mul_le_mul_left 2, apply mul_le_mul_left 2,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply max_left, apply max_left,
apply HNu, apply HNu,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply max_right, apply max_right,
rewrite [-padd_halves Nt, rat.add_sub_cancel], rewrite [-add_halves Nt, rat.add_sub_cancel],
apply inv_ge_of_le, apply inv_ge_of_le,
apply max_left apply max_left
end end
@ -872,20 +872,20 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rotate 1, rotate 1,
apply rat.add_le_add, apply rat.add_le_add,
apply HNt, apply HNt,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply max_right, apply max_right,
apply HNu, apply HNu,
apply ple.trans, apply pnat.le.trans,
apply pnat.mul_le_mul_left 2, apply mul_le_mul_left 2,
apply ple.trans, apply pnat.le.trans,
rotate 1, rotate 1,
apply Hn, apply Hn,
rotate_right 1, rotate_right 1,
apply max_left, apply max_left,
rewrite [-padd_halves Nu, neg_add_cancel_left], rewrite [-add_halves Nu, neg_add_cancel_left],
apply inv_ge_of_le, apply inv_ge_of_le,
apply max_left apply max_left
end end