lean2/library/data/pnat.lean

397 lines
12 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
Basic facts about the positive natural numbers.
Developed primarily for use in the construction of . For the most part, the only theorems here
are those needed for that construction.
-/
import data.rat.order data.nat
open nat rat subtype eq.ops
open algebra
namespace pnat
definition pnat := { n : | n > 0 }
notation `+` := pnat
definition pos (n : ) (H : n > 0) : + := tag n H
definition nat_of_pnat (p : +) : := elt_of p
reserve postfix `~`:std.prec.max_plus
local postfix ~ := nat_of_pnat
theorem pnat_pos (p : +) : p~ > 0 := has_property p
protected definition add (p q : +) : + :=
tag (p~ + q~) (add_pos (pnat_pos p) (pnat_pos q))
protected definition mul (p q : +) : + :=
tag (p~ * q~) (mul_pos (pnat_pos p) (pnat_pos q))
protected definition le (p q : +) := p~ ≤ q~
protected definition lt (p q : +) := p~ < q~
definition pnat_has_add [instance] [reducible] : has_add pnat :=
has_add.mk pnat.add
definition pnat_has_mul [instance] [reducible] : has_mul pnat :=
has_mul.mk pnat.mul
definition pnat_has_le [instance] [reducible] : has_le pnat :=
has_le.mk pnat.le
definition pnat_has_lt [instance] [reducible] : has_lt pnat :=
has_lt.mk pnat.lt
definition pnat_has_one [instance] [reducible] : 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)) :=
rfl
protected lemma le_def (p q : +) : (p ≤ q) = (p~ ≤ q~) :=
rfl
protected lemma lt_def (p q : +) : (p < q) = (p~ < q~) :=
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
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_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 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 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 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 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
notation 2 := (tag 2 dec_trivial : +)
notation 3 := (tag 3 dec_trivial : +)
definition pone : + := tag 1 dec_trivial
definition rat_of_pnat [reducible] (n : +) : :=
n~
theorem pnat.to_rat_of_nat (n : +) : rat_of_pnat n = of_nat n~ :=
rfl
-- these will come in rat
theorem rat_of_nat_nonneg (n : ) : 0 ≤ of_nat n :=
trivial
theorem rat_of_pnat_ge_one (n : +) : rat_of_pnat n ≥ 1 :=
of_nat_le_of_nat_of_le (pnat_pos n)
theorem rat_of_pnat_is_pos (n : +) : rat_of_pnat n > 0 :=
of_nat_lt_of_nat_of_lt (pnat_pos n)
theorem of_nat_le_of_nat_of_le {m n : } (H : m ≤ n) : of_nat m ≤ of_nat n :=
of_nat_le_of_nat_of_le H
theorem of_nat_lt_of_nat_of_lt {m n : } (H : m < n) : of_nat m < of_nat n :=
of_nat_lt_of_nat_of_lt H
theorem rat_of_pnat_le_of_pnat_le {m n : +} (H : m ≤ n) : rat_of_pnat m ≤ rat_of_pnat n :=
begin rewrite pnat.le_def at H, exact of_nat_le_of_nat_of_le H end
theorem rat_of_pnat_lt_of_pnat_lt {m n : +} (H : m < n) : rat_of_pnat m < rat_of_pnat n :=
begin rewrite pnat.lt_def at H, exact of_nat_lt_of_nat_of_lt H end
theorem pnat_le_of_rat_of_pnat_le {m n : +} (H : rat_of_pnat m ≤ rat_of_pnat n) : m ≤ n :=
begin rewrite pnat.le_def, exact le_of_of_nat_le_of_nat H end
definition inv (n : +) : :=
(1 : ) / rat_of_pnat n
local postfix `⁻¹` := inv
protected theorem inv_pos (n : +) : n⁻¹ > 0 := one_div_pos_of_pos !rat_of_pnat_is_pos
theorem inv_le_one (n : +) : n⁻¹ ≤ (1 : ) :=
begin
unfold inv,
change 1 / rat_of_pnat n ≤ 1 / 1,
apply one_div_le_one_div_of_le,
apply algebra.zero_lt_one,
apply rat_of_pnat_ge_one
end
theorem inv_lt_one_of_gt {n : +} (H : n~ > 1) : n⁻¹ < (1 : ) :=
begin
unfold inv,
change 1 / rat_of_pnat n < 1 / 1,
apply one_div_lt_one_div_of_lt,
apply algebra.zero_lt_one,
rewrite pnat.to_rat_of_nat,
apply (of_nat_lt_of_nat_of_lt H)
end
theorem pone_inv : pone⁻¹ = 1 := rfl
theorem add_invs_nonneg (m n : +) : 0 ≤ m⁻¹ + n⁻¹ :=
begin
apply le_of_lt,
apply add_pos,
repeat apply pnat.inv_pos
end
protected theorem one_mul (n : +) : pone * n = n :=
begin
apply pnat.eq,
unfold pone,
rewrite [pnat.mul_def, ↑nat_of_pnat, algebra.one_mul]
end
theorem pone_le (n : +) : pone ≤ n :=
begin rewrite pnat.le_def, exact succ_le_of_lt (pnat_pos n) end
theorem pnat_to_rat_mul (a b : +) : rat_of_pnat (a * b) = rat_of_pnat a * rat_of_pnat b := rfl
theorem mul_lt_mul_left {a b c : +} (H : a < b) : a * c < b * c :=
begin rewrite [pnat.lt_def at *], exact mul_lt_mul_of_pos_right H !pnat_pos end
theorem one_lt_two : pone < 2 :=
!nat.le_refl
theorem inv_two_mul_lt_inv (n : +) : (2 * n)⁻¹ < n⁻¹ :=
begin
rewrite ↑inv,
apply one_div_lt_one_div_of_lt,
apply rat_of_pnat_is_pos,
have H : n~ < (2 * n)~, begin
rewrite -pnat.one_mul at {1},
rewrite -pnat.lt_def,
apply mul_lt_mul_left,
apply one_lt_two
end,
apply of_nat_lt_of_nat_of_lt,
apply H
end
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⁻¹ :=
one_div_le_one_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⁻¹ :=
one_div_lt_one_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 :=
pnat_le_of_rat_of_pnat_le (le_of_one_div_le_one_div !rat_of_pnat_is_pos H)
theorem two_mul (p : +) : rat_of_pnat (2 * p) = (1 + 1) * rat_of_pnat p :=
by rewrite pnat_to_rat_mul
theorem add_halves (p : +) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ :=
begin
rewrite [↑inv, -(add_halves (1 / (rat_of_pnat p))), algebra.div_div_eq_div_mul],
have H : rat_of_pnat (2 * p) = rat_of_pnat p * (1 + 1), by rewrite [rat.mul_comm, two_mul],
rewrite *H
end
theorem add_halves_double (m n : +) :
m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) :=
have hsimp [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 rewrite [-add_halves m, -add_halves n, hsimp]
protected theorem inv_mul_eq_mul_inv {p q : +} : (p * q)⁻¹ = p⁻¹ * q⁻¹ :=
begin rewrite [↑inv, pnat_to_rat_mul, algebra.one_div_mul_one_div] end
protected theorem inv_mul_le_inv (p q : +) : (p * q)⁻¹ ≤ q⁻¹ :=
begin
rewrite [pnat.inv_mul_eq_mul_inv, -{q⁻¹}rat.one_mul at {2}],
apply algebra.mul_le_mul,
apply inv_le_one,
apply le.refl,
apply le_of_lt,
apply pnat.inv_pos,
apply rat.le_of_lt rat.zero_lt_one
end
theorem pnat_mul_le_mul_left' (a b c : +) : a ≤ b → c * a ≤ c * b :=
begin
rewrite +pnat.le_def, intro H,
apply mul_le_mul_of_nonneg_left H,
apply algebra.le_of_lt,
apply pnat_pos
end
protected theorem mul_assoc (a b c : +) : a * b * c = a * (b * c) :=
pnat.eq !mul.assoc
protected theorem mul_comm (a b : +) : a * b = b * a :=
pnat.eq !mul.comm
protected theorem add_assoc (a b c : +) : a + b + c = a + (b + c) :=
pnat.eq !add.assoc
protected theorem mul_le_mul_left (p q : +) : q ≤ p * q :=
begin
rewrite [-pnat.one_mul at {1}, pnat.mul_comm, pnat.mul_comm p],
apply pnat_mul_le_mul_left',
apply pone_le
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))
protected theorem inv_cancel_right (p : +) : p⁻¹ * rat_of_pnat p = (1 : ) :=
by rewrite rat.mul_comm; apply pnat.inv_cancel_left
theorem lt_add_left (p q : +) : p < p + q :=
begin
have H : p~ < p~ + q~, begin
rewrite -nat.add_zero at {1},
apply nat.add_lt_add_left,
apply pnat_pos
end,
apply H
end
theorem inv_add_lt_left (p q : +) : (p + q)⁻¹ < p⁻¹ :=
by apply inv_gt_of_lt; apply lt_add_left
theorem div_le_pnat (q : ) (n : +) (H : q ≥ n⁻¹) : 1 / q ≤ rat_of_pnat n :=
begin
apply algebra.div_le_of_le_mul,
apply algebra.lt_of_lt_of_le,
apply pnat.inv_pos,
rotate 1,
apply H,
apply le_mul_of_div_le,
apply rat_of_pnat_is_pos,
apply H
end
theorem pnat_cancel' (n m : +) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_pnat n) = m⁻¹ :=
assert hsimp : ∀ a b c : , (a * a * (b * b * c)) = (a * b) * (a * b) * c,
begin
intro a b c,
rewrite[-*rat.mul_assoc],
exact (!mul.right_comm ▸ rfl),
end,
by rewrite [rat.mul_comm, *pnat.inv_mul_eq_mul_inv, hsimp, *pnat.inv_cancel_left, *rat.one_mul]
definition pceil (a : ) : + := tag (ubound a) !ubound_pos
theorem pceil_helper {a : } {n : +} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a :=
algebra.le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a))
theorem inv_pceil_div (a b : ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a :=
assert (pceil (a / b))⁻¹ ≤ 1 / (1 / (b / a)),
begin
apply one_div_le_one_div_of_le,
show 0 < 1 / (b / a), from
one_div_pos_of_pos (div_pos_of_pos_of_pos Hb Ha),
show 1 / (b / a) ≤ rat_of_pnat (pceil (a / b)),
begin
rewrite div_div_eq_mul_div,
rewrite algebra.one_mul,
apply ubound_ge
end
end,
begin
rewrite one_div_one_div at this,
exact this
end
theorem sep_by_inv {a b : } : a > b → ∃ N : +, a > (b + N⁻¹ + N⁻¹) :=
begin
change b < a → ∃ N : +, (b + N⁻¹ + N⁻¹) < a,
intro H,
apply exists.elim (exists_add_lt_and_pos_of_lt H),
intro c Hc,
existsi (pceil ((1 + 1 + 1) / c)),
apply algebra.lt.trans,
rotate 1,
apply and.left Hc,
rewrite rat.add_assoc,
apply rat.add_lt_add_left,
rewrite -(algebra.add_halves c) at {3},
apply add_lt_add,
repeat (apply algebra.lt_of_le_of_lt;
apply inv_pceil_div;
apply dec_trivial;
apply and.right Hc;
apply div_lt_div_of_pos_of_lt_of_pos;
apply two_pos;
exact dec_trivial;
apply and.right Hc)
end
theorem nonneg_of_ge_neg_invs (a : ) : (∀ n : +, -n⁻¹ ≤ a) → 0 ≤ a :=
begin
intro H,
apply algebra.le_of_not_gt,
suppose a < 0,
have H2 : 0 < -a, from neg_pos_of_neg this,
(algebra.not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc
(pceil (of_num 2 / -a))⁻¹ ≤ -a / of_num 2
: !inv_pceil_div dec_trivial H2
... < -a / 1
: div_lt_div_of_pos_of_lt_of_pos dec_trivial dec_trivial H2
... = -a : !div_one))
end
theorem pnat_bound {ε : } (Hε : ε > 0) : ∃ p : +, p⁻¹ ≤ ε :=
begin
existsi (pceil (1 / ε)),
rewrite -(one_div_one_div ε) at {2},
apply pceil_helper,
apply pnat.le_refl,
apply one_div_pos_of_pos Hε
end
theorem p_add_fractions (n : +) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ :=
assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
by rewrite[*pnat.inv_mul_eq_mul_inv,-*right_distrib,T,rat.one_mul]
theorem rat_power_two_le (k : +) : rat_of_pnat k ≤ 2^k~ :=
!binary_nat_bound
end pnat