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

refactor(library/data/nat): cleanup for the tutorial

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-22 13:41:50 -07:00
parent 8085123119
commit fbaa8b21f6
4 changed files with 228 additions and 214 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

182
library/data/nat/order.lean
View file

@ -17,22 +17,22 @@ or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
lt.by_cases
(assume H1 : m < n, or.inl H1)
(assume H1 : m = n, or.inr H1)
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
(suppose m < n, or.inl this)
(suppose m = n, or.inr this)
(suppose m > n, absurd (lt_of_le_of_lt H this) !lt.irrefl)
theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n :=
iff.intro lt_or_eq_of_le le_of_lt_or_eq
theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
or.elim (lt_or_eq_of_le H1)
(take H3 : m < n, H3)
(take H3 : m = n, by contradiction)
(suppose m < n, this)
(suppose m = n, by contradiction)
theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n :=
iff.intro
(take H, and.intro (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
(take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H))
(suppose m < n, and.intro (le_of_lt this) (take H1, lt.irrefl _ (H1 ▸ this)))
(suppose m ≤ n ∧ m ≠ n, lt_of_le_and_ne (and.elim_left this) (and.elim_right this))
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
nat.induction_on k
@ -54,9 +54,9 @@ by induction h with m h ih;existsi 0; reflexivity;
theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
lt.by_cases
(assume H : m < n, or.inl (le_of_lt H))
(assume H : m = n, or.inl (by subst m))
(assume H : m > n, or.inr (le_of_lt H))
(suppose m < n, or.inl (le_of_lt this))
(suppose m = n, or.inl (by subst m))
(suppose m > n, or.inr (le_of_lt this))
/- addition -/
@ -94,8 +94,8 @@ theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k :=
theorem mul_le_mul_left {n m : ℕ} (k : ℕ) (H : n ≤ m) : k * n ≤ k * m :=
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
le.intro H2
have k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
le.intro this
theorem mul_le_mul_right {n m : ℕ} (k : ℕ) (H : n ≤ m) : n * k ≤ m * k :=
!mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H
@ -104,9 +104,8 @@ theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k *
le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2)
theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk,
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H),
lt_of_lt_of_le H2 H3
calc k * n < k * n + k : lt_add_of_pos_right Hk
... ≤ k * m : !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H)
theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
@ -123,27 +122,26 @@ eq.rec_on !if_t_t rfl
theorem max_le {n m k : ℕ} (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k :=
decidable.by_cases
(assume H : n < m, by rewrite [↑max, if_pos H]; apply H₂)
(assume H : ¬ n < m, by rewrite [↑max, if_neg H]; apply H₁)
(suppose n < m, by rewrite [↑max, if_pos this]; apply H₂)
(suppose ¬ n < m, by rewrite [↑max, if_neg this]; apply H₁)
theorem min_le_left (n m : ℕ) : min n m ≤ n :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H])
(assume H : ¬ n < m,
assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
by rewrite [↑min, if_neg H]; apply H')
(suppose n < m, by rewrite [↑min, if_pos this])
(suppose ¬ n < m,
assert m ≤ n, from or_resolve_right !lt_or_ge this,
by rewrite [↑min, if_neg `¬ n < m`]; apply this)
theorem min_le_right (n m : ℕ) : min n m ≤ m :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H]; apply le_of_lt H)
(assume H : ¬ n < m,
assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
by rewrite [↑min, if_neg H])
(suppose n < m, by rewrite [↑min, if_pos this]; apply le_of_lt this)
(suppose ¬ n < m,
by rewrite [↑min, if_neg `¬ n < m`])
theorem le_min {n m k : ℕ} (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H]; apply H₁)
(assume H : ¬ n < m, by rewrite [↑min, if_neg H]; apply H₂)
(suppose n < m, by rewrite [↑min, if_pos this]; apply H₁)
(suppose ¬ n < m, by rewrite [↑min, if_neg this]; apply H₂)
theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b :=
(if_pos H)⁻¹
@ -163,8 +161,8 @@ by_cases
theorem le_max_left (a b : ℕ) : a ≤ max a b :=
by_cases
(λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h))
(λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
(suppose a < b, le_of_lt (eq.rec_on (eq_max_right this) this))
(suppose ¬ a < b, eq.rec_on (eq_max_left this) !le.refl)
/- nat is an instance of a linearly ordered semiring and a lattice-/
@ -282,31 +280,31 @@ le.intro !add_one
theorem succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m :=
or.elim (lt_or_eq_of_le H)
(assume H1 : n < m, or.inl (succ_le_of_lt H1))
(assume H1 : n = m, or.inr H1)
(suppose n < m, or.inl (succ_le_of_lt this))
(suppose n = m, or.inr this)
theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m :=
nat.cases_on n
(assume H, !pred_zero⁻¹ ▸ zero_le m)
(take n',
assume H : succ n' ≤ succ m,
have H1 : n' ≤ m, from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
suppose succ n' ≤ succ m,
have n' ≤ m, from le_of_succ_le_succ this,
!pred_succ⁻¹ ▸ this)
theorem succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m :=
nat.cases_on m
(assume H, absurd H !not_succ_le_zero)
(take m',
assume H : succ n ≤ succ m',
have H1 : n ≤ m', from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
suppose succ n ≤ succ m',
have n ≤ m', from le_of_succ_le_succ this,
!pred_succ⁻¹ ▸ this)
theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
nat.cases_on n
(assume H, pred_zero⁻¹ ▸ zero_le (pred m))
(take n',
assume H : succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred H)
suppose succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred this)
theorem pre_lt_of_lt : ∀ {n m : ℕ}, n < m → pred n < m
| 0 m h := h
@ -314,12 +312,12 @@ theorem pre_lt_of_lt : ∀ {n m : ℕ}, n < m → pred n < m
theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
lt_of_not_ge
(take H1 : m ≤ n,
not_lt_of_ge (pred_le_pred_of_le H1) H)
(suppose m ≤ n,
not_lt_of_ge (pred_le_pred_of_le this) H)
theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
or_of_or_of_imp_left (succ_le_or_eq_of_le H)
(take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2)
(suppose succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ this)
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
nat.cases_on n
@ -334,8 +332,9 @@ theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : exists k, m = succ k :=
discriminate
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
(suppose m = 0, absurd (this ▸ H) !not_lt_zero)
(take l, suppose m = succ l,
exists.intro l this)
theorem lt_succ_self (n : ℕ) : n < succ n :=
lt.base n
@ -346,20 +345,20 @@ assume Plt, lt.trans Plt (self_lt_succ j)
/- other forms of induction -/
protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
have H1 : ∀ {n m : nat}, m < n → P m, from
have ∀ {n m : nat}, m < n → P m, from
take n,
nat.rec_on n
(show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero)
(take n',
assume IH : ∀ {m : nat}, m < n' → P m,
assert H2: P n', from H n' @IH,
assert P n', from H n' @IH,
show ∀m, m < succ n' → P m, from
take m,
assume H3 : m < succ n',
or.by_cases (lt_or_eq_of_le (le_of_lt_succ H3))
(assume H4: m < n', IH H4)
(assume H4: m = n', by subst m; assumption)),
H1 !lt_succ_self
suppose m < succ n',
or.by_cases (lt_or_eq_of_le (le_of_lt_succ this))
(suppose m < n', IH this)
(suppose m = n', by subst m; assumption)),
this !lt_succ_self
protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) :
P n :=
@ -371,11 +370,11 @@ nat.strong_induction_on a
(take n,
show (∀ m, m < n → P m) → P n, from
nat.cases_on n
(assume H : (∀m, m < 0 → P m), show P 0, from H0)
(suppose (∀ m, m < 0 → P m), show P 0, from H0)
(take n,
assume H : (∀m, m < succ n → P m),
suppose (∀ m, m < succ n → P m),
show P (succ n), from
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
Hind n (take m, assume H1 : m ≤ n, this _ (lt_succ_of_le H1))))
/- pos -/
@ -386,7 +385,7 @@ nat.cases_on y H0 (take y, H1 !succ_pos)
theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
or_of_or_of_imp_left
(or.swap (lt_or_eq_of_le !zero_le))
(take H : 0 = n, by subst n)
(suppose 0 = n, by subst n)
theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
or.elim !eq_zero_or_pos (take H2 : n = 0, by contradiction) (take H2 : n > 0, H2)
@ -399,9 +398,9 @@ exists_eq_succ_of_lt H
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(assume H3 : m = 0,
assert H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
ne_of_lt H2 (by subst n))
(suppose m = 0,
assert n = 0, from eq_zero_of_zero_dvd (this ▸ H1),
ne_of_lt H2 (by subst n))
/- multiplication -/
@ -420,10 +419,10 @@ lt_of_le_of_lt H3 H4
theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
have n * m ≤ n * k, by rewrite H,
have h : m ≤ k, from le_of_mul_le_mul_left this Hn,
have m ≤ k, from le_of_mul_le_mul_left this Hn,
have n * k ≤ n * m, by rewrite H,
have k ≤ m, from le_of_mul_le_mul_left this Hn,
le.antisymm h this
have k ≤ m, from le_of_mul_le_mul_left this Hn,
le.antisymm `m ≤ k` this
theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
@ -438,12 +437,12 @@ eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, by rewrite H; apply succ_pos,
or.elim (le_or_gt n 1)
(assume H5 : n ≤ 1,
(suppose n ≤ 1,
have n > 0, from pos_of_mul_pos_right H2,
show n = 1, from le.antisymm H5 (succ_le_of_lt this))
(assume H5 : n > 1,
show n = 1, from le.antisymm `n ≤ 1` (succ_le_of_lt this))
(suppose n > 1,
have m > 0, from pos_of_mul_pos_left H2,
have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt this),
have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt `n > 1`) (succ_le_of_lt this),
have 1 ≥ 2, from !mul_one ▸ H ▸ this,
absurd !lt_succ_self (not_lt_of_ge this))
@ -458,9 +457,8 @@ eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
dvd.elim H
(take m,
assume H1 : 1 = n * m,
eq_one_of_mul_eq_one_right H1⁻¹)
(take m, suppose 1 = n * m,
eq_one_of_mul_eq_one_right this⁻¹)
/- min and max -/
open decidable
@ -494,45 +492,45 @@ theorem max_succ_succ [simp] (a b : ℕ) : max (succ a) (succ b) = succ (max a b
by_cases
(suppose a < b, by unfold max; rewrite [if_pos this, if_pos (succ_lt_succ this)])
(suppose ¬ a < b,
assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold max; rewrite [if_neg this, if_neg h])
assert ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold max; rewrite [if_neg `¬ a < b`, if_neg `¬ succ a < succ b`])
theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c :=
decidable.by_cases
(assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
by rewrite (min_eq_right H'); apply H₂)
(suppose b ≤ c, by rewrite (min_eq_left this); apply H₁)
(suppose ¬ b ≤ c,
assert c ≤ b, from le_of_lt (lt_of_not_ge this),
by rewrite (min_eq_right this); apply H₂)
theorem max_lt {a b c : ℕ} (H₁ : a < c) (H₂ : b < c) : max a b < c :=
decidable.by_cases
(assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
(assume H : ¬ a ≤ b,
assert H' : b ≤ a, from le_of_lt (lt_of_not_ge H),
by rewrite (max_eq_left H'); apply H₁)
(suppose a ≤ b, by rewrite (max_eq_right this); apply H₂)
(suppose ¬ a ≤ b,
assert b ≤ a, from le_of_lt (lt_of_not_ge this),
by rewrite (max_eq_left this); apply H₁)
theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c :=
decidable.by_cases
(assume H : b ≤ c,
assert H1 : a + b ≤ a + c, from add_le_add_left H _,
by rewrite [min_eq_left H, min_eq_left H1])
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
assert H1 : a + c ≤ a + b, from add_le_add_left H' _,
by rewrite [min_eq_right H', min_eq_right H1])
(suppose b ≤ c,
assert a + b ≤ a + c, from add_le_add_left this _,
by rewrite [min_eq_left `b ≤ c`, min_eq_left this])
(suppose ¬ b ≤ c,
assert c ≤ b, from le_of_lt (lt_of_not_ge this),
assert a + c ≤ a + b, from add_le_add_left this _,
by rewrite [min_eq_right `c ≤ b`, min_eq_right this])
theorem min_add_add_right (a b c : ℕ) : min (a + c) (b + c) = min a b + c :=
by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply min_add_add_left
theorem max_add_add_left (a b c : ℕ) : max (a + b) (a + c) = a + max b c :=
decidable.by_cases
(assume H : b ≤ c,
assert H1 : a + b ≤ a + c, from add_le_add_left H _,
by rewrite [max_eq_right H, max_eq_right H1])
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
assert H1 : a + c ≤ a + b, from add_le_add_left H' _,
by rewrite [max_eq_left H', max_eq_left H1])
(suppose b ≤ c,
assert a + b ≤ a + c, from add_le_add_left this _,
by rewrite [max_eq_right `b ≤ c`, max_eq_right this])
(suppose ¬ b ≤ c,
assert c ≤ b, from le_of_lt (lt_of_not_ge this),
assert a + c ≤ a + b, from add_le_add_left this _,
by rewrite [max_eq_left `c ≤ b`, max_eq_left this])
theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c :=
by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left

54
library/data/nat/pairing.lean
View file

@ -19,54 +19,54 @@ if n - s*s < s then (n - s*s, s) else (s, n - s*s - s)
theorem mkpair_unpair (n : nat) : mkpair (pr1 (unpair n)) (pr2 (unpair n)) = n :=
let s := sqrt n in
by_cases
(λ h₁ : n - s*s < s,
(suppose n - s*s < s,
begin
esimp [unpair],
rewrite [if_pos h₁],
rewrite [if_pos this],
esimp [mkpair],
rewrite [if_pos h₁, add_sub_of_le (sqrt_lower n)]
rewrite [if_pos this, add_sub_of_le (sqrt_lower n)]
end)
(λ h₂ : ¬ n - s*s < s,
have g₁ : s ≤ n - s*s, from le_of_not_gt h₂,
assert g₂ : s + s*s ≤ n - s*s + s*s, from add_le_add_right g₁ (s*s),
assert g₃ : s*s + s ≤ n, by rewrite [sub_add_cancel (sqrt_lower n) at g₂, add.comm at g₂]; assumption,
have l₁ : n ≤ s*s + s + s, from sqrt_upper n,
have l₂ : n - s*s ≤ s + s, from calc
n - s*s ≤ (s*s + s + s) - s*s : sub_le_sub_right l₁ (s*s)
(suppose h₁ : ¬ n - s*s < s,
have s ≤ n - s*s, from le_of_not_gt h₁,
assert s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s),
assert s*s + s ≤ n, by rewrite [sub_add_cancel (sqrt_lower n) at this, add.comm at this]; assumption,
have n ≤ s*s + s + s, from sqrt_upper n,
have n - s*s ≤ s + s, from calc
n - s*s ≤ (s*s + s + s) - s*s : sub_le_sub_right this (s*s)
... = (s*s + (s+s)) - s*s : by rewrite add.assoc
... = s + s : by rewrite add_sub_cancel_left,
have l₃ : n - s*s - s ≤ s, from calc
n - s*s - s ≤ (s + s) - s : sub_le_sub_right l₂ s
have n - s*s - s ≤ s, from calc
n - s*s - s ≤ (s + s) - s : sub_le_sub_right this s
... = s : by rewrite add_sub_cancel_left,
assert l₄ : ¬ s < n - s*s - s, from not_lt_of_ge l₃,
assert h₂ : ¬ s < n - s*s - s, from not_lt_of_ge this,
begin
esimp [unpair],
rewrite [if_neg h₂], esimp,
rewrite [if_neg h₁], esimp,
esimp [mkpair],
rewrite [if_neg l₄, sub_sub, add_sub_of_le g₃],
rewrite [if_neg h₂, sub_sub, add_sub_of_le `s*s + s ≤ n`],
end)
theorem unpair_mkpair (a b : nat) : unpair (mkpair a b) = (a, b) :=
by_cases
(λ h : a < b,
assert aux₁ : a ≤ b + b, from calc
a ≤ b : le_of_lt h
(suppose a < b,
assert a ≤ b + b, from calc
a ≤ b : le_of_lt this
... ≤ b+b : !le_add_right,
begin
esimp [mkpair],
rewrite [if_pos h],
rewrite [if_pos `a < b`],
esimp [unpair],
rewrite [sqrt_offset_eq aux₁, add_sub_cancel_left, if_pos h]
rewrite [sqrt_offset_eq `a ≤ b + b`, add_sub_cancel_left, if_pos `a < b`]
end)
(λ h : ¬ a < b,
have h₁ : b ≤ a, from le_of_not_gt h,
assert aux₁ : a + b ≤ a + a, from add_le_add_left h₁ a,
have aux₂ : a + b ≥ a, from !le_add_right,
assert aux₃ : ¬ a + b < a, from not_lt_of_ge aux₂,
(suppose ¬ a < b,
have b ≤ a, from le_of_not_gt this,
assert a + b ≤ a + a, from add_le_add_left this a,
have a + b ≥ a, from !le_add_right,
assert ¬ a + b < a, from not_lt_of_ge this,
begin
esimp [mkpair],
rewrite [if_neg h],
rewrite [if_neg `¬ a < b`],
esimp [unpair],
rewrite [add.assoc (a * a) a b, sqrt_offset_eq aux₁, *add_sub_cancel_left, if_neg aux₃]
rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *add_sub_cancel_left, if_neg `¬ a + b < a`]
end)
end nat

169
library/data/nat/parity.lean
View file

@ -13,12 +13,12 @@ open decidable
definition even (n : nat) := n mod 2 = 0
definition decidable_even [instance] : ∀ n, decidable (even n) :=
λ n, !nat.has_decidable_eq
take n, !nat.has_decidable_eq
definition odd (n : nat) := ¬even n
definition decidable_odd [instance] : ∀ n, decidable (odd n) :=
λ n, decidable_not
take n, decidable_not
lemma even_of_dvd {n} : 2 ∣ n → even n :=
mod_eq_zero_of_dvd
@ -38,29 +38,34 @@ dec_trivial
lemma not_even_one : ¬ even 1 :=
dec_trivial
lemma odd_eq_not_even : ∀ n, odd n = ¬ even n :=
λ n, rfl
lemma odd_eq_not_even (n : nat) : odd n = ¬ even n :=
rfl
lemma odd_iff_not_even : ∀ n, odd n ↔ ¬ even n :=
λ n, !iff.refl
lemma odd_iff_not_even (n : nat) : odd n ↔ ¬ even n :=
!iff.refl
lemma odd_of_not_even {n} : ¬ even n → odd n :=
λ h, iff.mpr !odd_iff_not_even h
suppose ¬ even n,
iff.mpr !odd_iff_not_even this
lemma even_of_not_odd {n} : ¬ odd n → even n :=
λ h, not_not_elim (iff.mp (not_iff_not_of_iff !odd_iff_not_even) h)
suppose ¬ odd n,
not_not_elim (iff.mp (not_iff_not_of_iff !odd_iff_not_even) this)
lemma not_odd_of_even {n} : even n → ¬ odd n :=
λ h, iff.mpr (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro h)
suppose even n,
iff.mpr (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro this)
lemma not_even_of_odd {n} : odd n → ¬ even n :=
λ h, iff.mp !odd_iff_not_even h
suppose odd n,
iff.mp !odd_iff_not_even this
lemma odd_succ_of_even {n} : even n → odd (succ n) :=
λ h, by_contradiction (λ hn : ¬ odd (succ n),
suppose even n,
by_contradiction (suppose ¬ odd (succ n),
assert 0 = 1, from calc
0 = (n+1) mod 2 : even_of_not_odd hn
... = 1 mod 2 : add_mod_eq_add_mod_right 1 h,
0 = (n+1) mod 2 : even_of_not_odd this
... = 1 mod 2 : add_mod_eq_add_mod_right 1 `even n`,
by contradiction)
lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1
@ -69,64 +74,72 @@ lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1
| (n+2) h₁ h₂ := absurd (lt_of_succ_lt_succ (lt_of_succ_lt_succ h₂)) !not_lt_zero
lemma mod_eq_of_odd {n} : odd n → n mod 2 = 1 :=
λ h,
have h₁ : ¬ n mod 2 = 0, from h,
have h₂ : n mod 2 < 2, from mod_lt n dec_trivial,
eq_1_of_ne_0_lt_2 h₁ h₂
suppose odd n,
have ¬ n mod 2 = 0, from this,
have n mod 2 < 2, from mod_lt n dec_trivial,
eq_1_of_ne_0_lt_2 `¬ n mod 2 = 0` `n mod 2 < 2`
lemma odd_of_mod_eq {n} : n mod 2 = 1 → odd n :=
λ h, by_contradiction (λ hn,
assert h₁ : n mod 2 = 0, from even_of_not_odd hn,
by rewrite h at h₁; contradiction)
suppose n mod 2 = 1,
by_contradiction (suppose ¬ odd n,
assert n mod 2 = 0, from even_of_not_odd this,
by rewrite this at *; contradiction)
lemma even_succ_of_odd {n} : odd n → even (succ n) :=
λ h,
have h₁ : n mod 2 = 1, from mod_eq_of_odd h,
have h₂ : n mod 2 = 1 mod 2, from mod_eq_of_odd h,
have h₃ : (n+1) mod 2 = 0, from add_mod_eq_add_mod_right 1 h₂,
h₃
suppose odd n,
have n mod 2 = 1 mod 2, from mod_eq_of_odd this,
have (n+1) mod 2 = 0, from add_mod_eq_add_mod_right 1 this,
this
lemma odd_succ_succ_of_odd {n} : odd n → odd (succ (succ n)) :=
λ h, odd_succ_of_even (even_succ_of_odd h)
suppose odd n,
odd_succ_of_even (even_succ_of_odd this)
lemma even_succ_succ_of_even {n} : even n → even (succ (succ n)) :=
λ h, even_succ_of_odd (odd_succ_of_even h)
suppose even n,
even_succ_of_odd (odd_succ_of_even this)
lemma even_of_odd_succ {n} : odd (succ n) → even n :=
λ h, by_contradiction (λ he,
have h₁ : odd n, from odd_of_not_even he,
have h₂ : even (succ n), from even_succ_of_odd h₁,
absurd h₂ (not_even_of_odd h))
suppose odd (succ n),
by_contradiction (suppose ¬ even n,
have odd n, from odd_of_not_even this,
have even (succ n), from even_succ_of_odd this,
absurd this (not_even_of_odd `odd (succ n)`))
lemma odd_of_even_succ {n} : even (succ n) → odd n :=
λ h, by_contradiction (λ he,
have h₁ : even n, from even_of_not_odd he,
have h₂ : odd (succ n), from odd_succ_of_even h₁,
absurd h (not_even_of_odd h₂))
suppose even (succ n),
by_contradiction (suppose ¬ odd n,
have even n, from even_of_not_odd this,
have odd (succ n), from odd_succ_of_even this,
absurd `even (succ n)` (not_even_of_odd this))
lemma even_of_even_succ_succ {n} : even (succ (succ n)) → even n :=
λ h, even_of_odd_succ (odd_of_even_succ h)
suppose even (n+2),
even_of_odd_succ (odd_of_even_succ this)
lemma odd_of_odd_succ_succ {n} : odd (succ (succ n)) → odd n :=
λ h, odd_of_even_succ (even_of_odd_succ h)
suppose odd (n+2),
odd_of_even_succ (even_of_odd_succ this)
lemma dvd_of_odd {n} : odd n → 2 ∣ n+1 :=
λ h, dvd_of_even (even_succ_of_odd h)
suppose odd n,
dvd_of_even (even_succ_of_odd this)
lemma odd_of_dvd {n} : 2 ∣ n+1 → odd n :=
λ h, odd_of_even_succ (even_of_dvd h)
suppose 2 ∣ n+1,
odd_of_even_succ (even_of_dvd this)
lemma even_two_mul : ∀ n, even (2 * n) :=
λ n, even_of_dvd (dvd_mul_right 2 n)
take n, even_of_dvd (dvd_mul_right 2 n)
lemma odd_two_mul_plus_one : ∀ n, odd (2 * n + 1) :=
λ n, odd_succ_of_even (even_two_mul n)
take n, odd_succ_of_even (even_two_mul n)
lemma not_even_two_mul_plus_one : ∀ n, ¬ even (2 * n + 1) :=
λ n, not_even_of_odd (odd_two_mul_plus_one n)
take n, not_even_of_odd (odd_two_mul_plus_one n)
lemma not_odd_two_mul : ∀ n, ¬ odd (2 * n) :=
λ n, not_odd_of_even (even_two_mul n)
take n, not_odd_of_even (even_two_mul n)
lemma even_pred_of_odd : ∀ {n}, odd n → even (pred n)
| 0 h := absurd h not_odd_zero
@ -147,59 +160,61 @@ lemma exists_of_odd : ∀ {n}, odd n → ∃ k, n = 2*k + 1
exists.intro k (by subst n)
lemma even_of_exists {n} : (∃ k, n = 2 * k) → even n :=
λ h, obtain k (hk : n = 2 * k), from h,
have h₁ : 2 ∣ n, by subst n; apply dvd_mul_right,
even_of_dvd h₁
suppose ∃ k, n = 2 * k,
obtain k (hk : n = 2 * k), from this,
have 2 ∣ n, by subst n; apply dvd_mul_right,
even_of_dvd this
lemma odd_of_exists {n} : (∃ k, n = 2 * k + 1) → odd n :=
λ h, by_contradiction (λ hn,
have h₁ : even n, from even_of_not_odd hn,
have h₂ : ∃ k, n = 2 * k, from exists_of_even h₁,
assume h, by_contradiction (λ hn,
have even n, from even_of_not_odd hn,
have ∃ k, n = 2 * k, from exists_of_even this,
obtain k₁ (hk₁ : n = 2 * k₁ + 1), from h,
obtain k₂ (hk₂ : n = 2 * k₂), from h₂,
assert h₃ : (2 * k₁ + 1) mod 2 = (2 * k₂) mod 2, by rewrite [-hk₁, -hk₂],
obtain k₂ (hk₂ : n = 2 * k₂), from this,
assert (2 * k₁ + 1) mod 2 = (2 * k₂) mod 2, by rewrite [-hk₁, -hk₂],
begin
rewrite [mul_mod_right at h₃, add.comm at h₃, add_mul_mod_self_left at h₃],
rewrite [mul_mod_right at this, add.comm at this, add_mul_mod_self_left at this],
contradiction
end)
lemma even_add_of_even_of_even {n m} : even n → even m → even (n+m) :=
λ h₁ h₂,
obtain k₁ (hk₁ : n = 2 * k₁), from exists_of_even h₁,
obtain k₂ (hk₂ : m = 2 * k₂), from exists_of_even h₂,
suppose even n, suppose even m,
obtain k₁ (hk₁ : n = 2 * k₁), from exists_of_even `even n`,
obtain k₂ (hk₂ : m = 2 * k₂), from exists_of_even `even m`,
even_of_exists (exists.intro (k₁+k₂) (by rewrite [hk₁, hk₂, mul.left_distrib]))
lemma even_add_of_odd_of_odd {n m} : odd n → odd m → even (n+m) :=
λ h₁ h₂,
assert h₃ : even (succ n + succ m), from even_add_of_even_of_even (even_succ_of_odd h₁) (even_succ_of_odd h₂),
have h₄ : even(succ (succ (n + m))), by rewrite [add_succ at h₃, succ_add at h₃]; exact h₃,
even_of_even_succ_succ h₄
suppose odd n, suppose odd m,
assert even (succ n + succ m), from even_add_of_even_of_even (even_succ_of_odd `odd n`) (even_succ_of_odd `odd m`),
have even(succ (succ (n + m))), by rewrite [add_succ at this, succ_add at this]; exact this,
even_of_even_succ_succ this
lemma odd_add_of_even_of_odd {n m} : even n → odd m → odd (n+m) :=
λ h₁ h₂,
assert h₃ : even (n + succ m), from even_add_of_even_of_even h₁ (even_succ_of_odd h₂),
odd_of_even_succ h₃
suppose even n, suppose odd m,
assert even (n + succ m), from even_add_of_even_of_even `even n` (even_succ_of_odd `odd m`),
odd_of_even_succ this
lemma odd_add_of_odd_of_even {n m} : odd n → even m → odd (n+m) :=
λ h₁ h₂,
assert h₃ : odd (m+n), from odd_add_of_even_of_odd h₂ h₁,
by rewrite add.comm at h₃; exact h₃
suppose odd n, suppose even m,
assert odd (m+n), from odd_add_of_even_of_odd `even m` `odd n`,
by rewrite add.comm at this; exact this
lemma even_mul_of_even_left {n} (m) : even n → even (n*m) :=
λ h,
obtain k (hk : n = 2*k), from exists_of_even h,
even_of_exists (exists.intro (k*m) (by rewrite [hk, mul.assoc]))
suppose even n,
obtain k (hk : n = 2*k), from exists_of_even this,
even_of_exists (exists.intro (k*m) (by rewrite [hk, mul.assoc]))
lemma even_mul_of_even_right {n} (m) : even n → even (m*n) :=
λ h₁,
assert h₂ : even (n*m), from even_mul_of_even_left _ h₁,
by rewrite mul.comm at h₂; exact h₂
suppose even n,
assert even (n*m), from even_mul_of_even_left _ this,
by rewrite mul.comm at this; exact this
lemma odd_mul_of_odd_of_odd {n m} : odd n → odd m → odd (n*m) :=
λ h₁ h₂,
assert h₃ : even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd h₂),
assert h₄ : even (n * m + n), by rewrite mul_succ at h₃; exact h₃,
by_contradiction (λ hn,
assert h₅ : even (n*m), from even_of_not_odd hn,
absurd h₄ (not_even_of_odd (odd_add_of_even_of_odd h₅ h₁)))
suppose odd n, suppose odd m,
assert even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd `odd m`),
assert even (n * m + n), by rewrite mul_succ at this; exact this,
by_contradiction (suppose ¬ odd (n*m),
assert even (n*m), from even_of_not_odd this,
absurd `even (n * m + n)` (not_even_of_odd (odd_add_of_even_of_odd this `odd n`)))
end nat

37
library/data/nat/power.lean
View file

@ -32,16 +32,16 @@ end migrate_algebra
-- generalize to semirings?
theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
| 0 := !zero_le
| (succ j) := have xpos : x > 0, from lt.trans zero_lt_one H,
have xjge1 : x^j ≥ 1, from succ_le_of_lt (pow_pos_of_pos _ xpos),
have xge2 : x ≥ 2, from succ_le_of_lt H,
| (succ j) := have x > 0, from lt.trans zero_lt_one H,
have x^j ≥ 1, from succ_le_of_lt (pow_pos_of_pos _ this),
have x ≥ 2, from succ_le_of_lt H,
calc
succ j = j + 1 : rfl
... ≤ x^j + 1 : add_le_add_right (le_pow_self j)
... ≤ x^j + x^j : add_le_add_left xjge1
... ≤ x^j + x^j : add_le_add_left `x^j ≥ 1`
... = x^j * (1 + 1) : by rewrite [mul.left_distrib, *mul_one]
... = x^j * 2 : rfl
... ≤ x^j * x : mul_le_mul_left _ xge2
... ≤ x^j * x : mul_le_mul_left _ `x ≥ 2`
... = x^(succ j) : rfl
-- TODO: eventually this will be subsumed under the algebraic theorems
@ -53,17 +53,17 @@ by rewrite [*pow_succ, *pow_zero, one_mul]
theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b = c
| a 0 0 h₁ h₂ := rfl
| a (succ b) 0 h₁ h₂ :=
assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁,
absurd h₁ !lt.irrefl
assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
assert 1 < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 < 1` !lt.irrefl
| a 0 (succ c) h₁ h₂ :=
assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁,
absurd h₁ !lt.irrefl
assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
assert 1 < 1, by rewrite [this at h₁]; exact h₁,
absurd `1 < 1` !lt.irrefl
| a (succ b) (succ c) h₁ h₂ :=
assert ane0 : a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
assert beqc : pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero ane0) h₂),
by rewrite [pow_cancel_left h₁ beqc]
assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
assert pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
by rewrite [pow_cancel_left h₁ this]
theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b
| a 0 h := by rewrite [pow_succ', pow_zero, mul_one, div_self (pos_of_ne_zero h)]
@ -81,9 +81,9 @@ lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i^n) mod i = 0 :=
iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h)
lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n :=
assume Psuccdvd,
assert Pdvdsucc : p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl,
dvd.trans Pdvdsucc Psuccdvd
suppose p^(succ i) ∣ n,
assert p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl,
dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n`
lemma dvd_of_pow_succ_dvd_mul_pow {p i n : nat} (Ppos : p > 0) :
p^(succ i) ∣ (n * p^i) → p ∣ n :=
@ -100,6 +100,7 @@ lemma coprime_pow_right {a b} : ∀ n, coprime b a → coprime b (a^n)
end
lemma coprime_pow_left {a b} : ∀ n, coprime b a → coprime (b^n) a :=
λ n h, coprime_swap (coprime_pow_right n (coprime_swap h))
take n, suppose coprime b a,
coprime_swap (coprime_pow_right n (coprime_swap this))
end nat