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

refactor(library/data/nat): use new tactics

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-25 18:14:52 -07:00
parent a4e72e5262
commit 4152ebfa23
5 changed files with 38 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/nat/choose.lean
View file

@ -25,7 +25,7 @@ private lemma lbp_zero : lbp 0 :=
private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
λ lx npx y yltsx,
or.elim (eq_or_lt_of_le yltsx)
(λ yeqx, by rewrite [yeqx]; exact npx)
(λ yeqx, by substvars; assumption)
(λ yltx, lx y yltx)
private definition gtb (a b : nat) : Prop :=
@ -36,8 +36,7 @@ local infix `≺`:50 := gtb
private lemma acc_of_px {x : nat} : p x → acc gtb x :=
assume h,
acc.intro x (λ (y : nat) (l : y ≺ x),
have h₁ : y > x, from and.elim_left l,
have h₂ : ∀ a, a < y → ¬ p a, from and.elim_right l,
obtain (h₁ : y > x) (h₂ : ∀ a, a < y → ¬ p a), from l,
absurd h (h₂ x h₁))
private lemma acc_of_acc_succ {x : nat} : acc gtb (succ x) → acc gtb x :=
@ -45,7 +44,7 @@ assume h,
acc.intro x (λ (y : nat) (l : y ≺ x),
have ygtx : x < y, from and.elim_left l,
by_cases
(λ yeqx : y = succ x, by rewrite [yeqx]; exact h)
(λ yeqx : y = succ x, by substvars; assumption)
(λ ynex : y ≠ succ x,
have ygtsx : succ x < y, from lt_of_le_and_ne (succ_lt_succ ygtx) (ne.symm ynex),
acc.inv h (and.intro ygtsx (and.elim_right l))))
@ -53,8 +52,7 @@ acc.intro x (λ (y : nat) (l : y ≺ x),
private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y :=
assume px ygtx,
acc.intro y (λ (z : nat) (l : z ≺ y),
have zgty : z > y, from and.elim_left l,
have h : ∀ a, a < z → ¬ p a, from and.elim_right l,
obtain (zgty : z > y) (h : ∀ a, a < z → ¬ p a), from l,
absurd px (h x (lt.trans ygtx zgty)))
private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gtb y
@ -62,7 +60,7 @@ private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gt
| (succ x) y asx yltsx :=
assert ax : acc gtb x, from acc_of_acc_succ asx,
by_cases
(λ yeqx : y = x, by rewrite [yeqx]; exact ax)
(λ yeqx : y = x, by substvars; assumption)
(λ ynex : y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne yltsx ynex))
parameter (ex : ∃ a, p a)
@ -73,7 +71,7 @@ private lemma acc_of_ex (x : nat) : acc gtb x :=
obtain (w : nat) (pw : p w), from ex,
lt.by_cases
(λ xltw : x < w, acc_of_acc_of_lt (acc_of_px pw) xltw)
(λ xeqw : x = w, by rewrite [xeqw]; exact (acc_of_px pw))
(λ xeqw : x = w, by subst x; exact (acc_of_px pw))
(λ xgtw : x > w, acc_of_px_of_gt pw xgtw)
private lemma wf_gtb : well_founded gtb :=

15
library/data/nat/div.lean
View file

@ -225,11 +225,11 @@ theorem mul_mod_mul_left (z x y : ℕ) : (z * x) mod (z * y) = z * (x mod y) :=
or.elim (eq_zero_or_pos z)
(assume H : z = 0,
calc
(z * x) mod (z * y) = (0 * x) mod (z * y) : H
(z * x) mod (z * y) = (0 * x) mod (z * y) : by subst z
... = 0 mod (z * y) : zero_mul
... = 0 : zero_mod
... = 0 * (x mod y) : zero_mul
... = z * (x mod y) : H)
... = z * (x mod y) : by subst z)
(assume zpos : z > 0,
or.elim (eq_zero_or_pos y)
(assume H : y = 0, by simp)
@ -618,13 +618,10 @@ theorem gcd_div {m n k : ℕ} (H1 : (k ∣ m)) (H2 : (k ∣ n)) :
or.elim (eq_zero_or_pos k)
(assume H3 : k = 0,
calc
gcd (m div k) (n div k) = gcd (m div 0) (n div k) : H3
... = gcd 0 (n div k) : div_zero
... = n div k : gcd_zero_left
... = n div 0 : H3
... = 0 : div_zero
... = gcd m n div 0 : div_zero
... = gcd m n div k : H3)
gcd (m div k) (n div k) = gcd 0 0 : by subst k; rewrite *div_zero
... = 0 : gcd_zero_left
... = gcd m n div 0 : div_zero
... = gcd m n div k : by subst k)
(assume H3 : k > 0,
eq_div_of_mul_eq H3
(calc

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

@ -33,7 +33,7 @@ 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, absurd H3 H2)
(take H3 : m = n, by contradiction)
theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n :=
iff.intro
@ -68,7 +68,7 @@ le.rec_on h
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 (H ▸ !le.refl))
(assume H : m = n, or.inl (by subst m))
(assume H : m > n, or.inr (le_of_lt H))
/- addition -/
@ -77,8 +77,8 @@ theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
le.intro
(calc
k + n + l = k + (n + l) : !add.assoc
... = k + m : {Hl})
k + n + l = k + (n + l) : add.assoc
... = k + m : by subst m)
theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
!add.comm ▸ !add.comm ▸ add_le_add_left H k
@ -87,7 +87,7 @@ theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m :=
obtain (l : ℕ) (Hl : k + n + l = k + m), from (le.elim H),
le.intro (add.cancel_left
(calc
k + (n + l) = k + n + l : (!add.assoc)⁻¹
k + (n + l) = k + n + l : add.assoc
... = k + m : Hl))
theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
@ -121,19 +121,19 @@ theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k <
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
obtain (k : ℕ) (Hk : n + k = m), from (le.elim H1),
obtain (l : ℕ) (Hl : m + l = n), from (le.elim H2),
obtain (k : ℕ) (Hk : n + k = m), from le.elim H1,
obtain (l : ℕ) (Hl : m + l = n), from le.elim H2,
have L1 : k + l = 0, from
add.cancel_left
(calc
n + (k + l) = n + k + l : (!add.assoc)⁻¹
... = m + l : {Hk}
... = n : Hl
... = n + 0 : (!add_zero)⁻¹),
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
n + (k + l) = n + k + l : add.assoc
... = m + l : by subst m
... = n : by subst n
... = n + 0 : add_zero),
assert L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
calc
n = n + 0 : (!add_zero)⁻¹
... = n + k : {L2⁻¹}
n = n + 0 : add_zero
... = n + k : by subst k
... = m : Hk
theorem zero_le (n : ℕ) : 0 ≤ n :=
@ -237,7 +237,7 @@ theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
!add_one ▸ !add_one ▸ add_le_add_right H 1
theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m :=
le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
le_of_add_le_add_right H
theorem self_le_succ (n : ℕ) : n ≤ succ n :=
le.intro !add_one
@ -319,13 +319,13 @@ have H1 : ∀ {n m : nat}, m < n → P m, from
(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,
have H2: P n', from H n' @IH,
assert H2: P n', from H n' @IH,
show ∀m, m < succ n' → P m, from
take m,
assume H3 : m < succ n',
or.elim (lt_or_eq_of_le (le_of_lt_succ H3))
(assume H4: m < n', IH H4)
(assume H4: m = n', H4⁻¹ ▸ H2)),
(assume H4: m = n', by subst m; assumption)),
H1 !lt_succ_self
protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
@ -349,10 +349,10 @@ 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, H⁻¹)
(take H : 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, absurd H2 H) (take H2 : n > 0, H2)
or.elim !eq_zero_or_pos (take H2 : n = 0, by contradiction) (take H2 : n > 0, H2)
theorem ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
ne.symm (ne_of_lt H)
@ -363,8 +363,8 @@ 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,
have H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
ne_of_lt H2 H4⁻¹)
assert H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
ne_of_lt H2 (by subst n))
/- multiplication -/
@ -382,8 +382,8 @@ have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le
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 H2 : n * m ≤ n * k, from H ▸ !le.refl,
have H3 : n * k ≤ n * m, from H ▸ !le.refl,
have H2 : n * m ≤ n * k, by rewrite H,
have H3 : n * k ≤ n * m, by rewrite H,
have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
le.antisymm H4 H5
@ -399,7 +399,7 @@ theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : ℕ} (H : n * m = k * m) : m
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, from H⁻¹ ▸ !succ_pos,
have H2 : n * m > 0, by rewrite H; apply succ_pos,
have H3 : n > 0, from pos_of_mul_pos_right H2,
have H4 : m > 0, from pos_of_mul_pos_left H2,
or.elim (le_or_gt n 1)

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

@ -29,7 +29,7 @@ by_cases
(λ 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₂]; exact g₂,
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)

2
library/init/nat.lean
View file

@ -114,7 +114,7 @@ namespace nat
inr aux)))
a
theorem le.refl (a : nat) : a ≤ a :=
theorem le.refl [refl] (a : nat) : a ≤ a :=
lt.base a
theorem le_of_lt {a b : nat} (H : a < b) : a ≤ b :=