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

refactor(library/data/nat): prove auxiliary theorems about < and sub asap for the definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-22 09:36:33 -08:00
parent 29a0d3109b
commit 9c9f5bba1a
2 changed files with 48 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
library/data/nat/decl.lean
View file

@ -232,15 +232,21 @@ namespace nat
definition max_a_a (a : nat) : a = max a a :=
eq.rec_on !if_t_t rfl
definition max.eq_right {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (if_pos H) rfl
definition max.eq_right {a b : nat} (H : a < b) : max a b = b :=
if_pos H
definition max.eq_left {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (if_neg H) rfl
definition max.eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
if_neg H
definition max.eq_right_symm {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (max.eq_right H) rfl
definition max.eq_left_symm {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (max.eq_left H) rfl
definition max.left (a b : nat) : a ≤ max a b :=
by_cases
(λ h : a < b, le.of_lt (eq.rec_on (max.eq_right h) h))
(λ h : a < b, le.of_lt (eq.rec_on (max.eq_right_symm h) h))
(λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
definition max.right (a b : nat) : b ≤ max a b :=
@ -249,7 +255,7 @@ namespace nat
(λ h : ¬ a < b, or.rec_on (not_lt h)
(λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
(λ h : b < a,
have aux : a = max a b, from max.eq_left (lt.asymm h),
have aux : a = max a b, from max.eq_left_symm (lt.asymm h),
eq.rec_on aux (le.of_lt h)))
definition gt a b := lt b a
@ -274,4 +280,38 @@ namespace nat
rec_on b zero (λ b₁ r, r + a)
notation a * b := mul a b
definition sub.succ_succ (a b : nat) : succ a - succ b = a - b :=
induction_on b
rfl
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
definition sub.succ_succ_symm (a b : nat) : a - b = succ a - succ b :=
eq.rec_on (sub.succ_succ a b) rfl
definition sub.zero_left (a : nat) : zero - a = zero :=
induction_on a
rfl
(λ a₁ (ih : zero - a₁ = zero),
eq.rec_on ih (eq.refl (pred (zero - a₁))))
definition sub.zero_left_symm (a : nat) : zero = zero - a :=
eq.rec_on (sub.zero_left a) rfl
definition sub.lt {a b : nat} : zero < a → zero < b → a - b < a :=
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
λa h₁, lt.rec_on h₁
(λb h₂, lt.cases_on h₂
(lt.base zero)
(λ b₁ bpos,
eq.rec_on (sub.succ_succ_symm zero b₁)
(eq.rec_on (sub.zero_left_symm b₁) (lt.base zero))))
(λa₁ apos ih b h₂, lt.cases_on h₂
(lt.base a₁)
(λ b₁ bpos,
eq.rec_on (sub.succ_succ_symm a₁ b₁)
(lt.trans (@ih b₁ bpos) (lt.base a₁)))),
λ h₁ h₂, aux h₁ h₂
end nat

23
library/data/nat/sub.lean
View file

@ -36,18 +36,7 @@ induction_on n !sub_zero_right
... = 0 : pred.zero)
theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m :=
induction_on m
(calc
succ n - 1 = pred (succ n - 0) : !sub_succ_right
... = pred (succ n) : {!sub_zero_right}
... = n : !pred.succ
... = n - 0 : !sub_zero_right⁻¹)
(take k : nat,
assume IH : succ n - succ k = n - k,
calc
succ n - succ (succ k) = pred (succ n - succ k) : !sub_succ_right
... = pred (n - k) : {IH}
... = n - succ k : !sub_succ_right⁻¹)
sub.succ_succ n m
theorem sub_self (n : ℕ) : n - n = 0 :=
induction_on n !sub_zero_right (take k IH, !sub_succ_succ ⬝ IH)
@ -290,15 +279,7 @@ have H2 : k - n + n = m + n, from
add.cancel_right H2
theorem sub_lt {x y : ℕ} (xpos : x > 0) (ypos : y > 0) : x - y < x :=
obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos,
obtain (y' : ℕ) (yeq : y = succ y'), from pos_imp_eq_succ ypos,
have xsuby_eq : x - y = x' - y', from calc
x - y = succ x' - y : {xeq}
... = succ x' - succ y' : {yeq}
... = x' - y' : !sub_succ_succ,
have H1 : x' - y' ≤ x', from !sub_le_self,
have H2 : x' < succ x', from !self_lt_succ,
show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt.trans H1 H2
sub.lt xpos ypos
theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k :=
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,