refactor(library/standard/data/nat): stylistic changes
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
b5db9a4797
commit
b832b2e33e
2 changed files with 650 additions and 697 deletions
|
|
@ -50,39 +50,39 @@ theorem zero_le (n : ℕ) : 0 ≤ n :=
|
|||
le_intro (add_zero_left n)
|
||||
|
||||
theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
|
||||
add_eq_zero_left Hk
|
||||
obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
|
||||
add_eq_zero_left Hk
|
||||
|
||||
theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
|
||||
not_intro
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from le_zero H,
|
||||
absurd H2 (succ_ne_zero n))
|
||||
not_intro
|
||||
(assume H : succ n ≤ 0,
|
||||
have H2 : succ n = 0, from le_zero H,
|
||||
absurd H2 (succ_ne_zero n))
|
||||
|
||||
theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
|
||||
obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
|
||||
obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2,
|
||||
le_intro
|
||||
(calc
|
||||
n + (l1 + l2) = n + l1 + l2 : symm (add_assoc n l1 l2)
|
||||
... = m + l2 : {Hl1}
|
||||
... = k : Hl2)
|
||||
obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1,
|
||||
obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2,
|
||||
le_intro
|
||||
(calc
|
||||
n + (l1 + l2) = n + l1 + l2 : symm (add_assoc n l1 l2)
|
||||
... = m + l2 : {Hl1}
|
||||
... = k : Hl2)
|
||||
|
||||
theorem le_antisym {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),
|
||||
have L1 : k + l = 0, from
|
||||
add_cancel_left
|
||||
(calc
|
||||
n + (k + l) = n + k + l : symm (add_assoc n k l)
|
||||
... = m + l : {Hk}
|
||||
... = n : Hl
|
||||
... = n + 0 : symm (add_zero_right n)),
|
||||
have L2 : k = 0, from add_eq_zero_left L1,
|
||||
calc
|
||||
n = n + 0 : symm (add_zero_right n)
|
||||
... = n + k : {symm L2}
|
||||
... = m : Hk
|
||||
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 : symm (add_assoc n k l)
|
||||
... = m + l : {Hk}
|
||||
... = n : Hl
|
||||
... = n + 0 : symm (add_zero_right n)),
|
||||
have L2 : k = 0, from add_eq_zero_left L1,
|
||||
calc
|
||||
n = n + 0 : symm (add_zero_right n)
|
||||
... = n + k : {symm L2}
|
||||
... = m : Hk
|
||||
|
||||
-- ### interaction with addition
|
||||
|
||||
|
|
@ -93,34 +93,34 @@ theorem le_add_left (n m : ℕ) : n ≤ m + n :=
|
|||
le_intro (add_comm n m)
|
||||
|
||||
theorem add_le_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 n l
|
||||
... = k + m : {Hl})
|
||||
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
|
||||
le_intro
|
||||
(calc
|
||||
k + n + l = k + (n + l) : add_assoc k n l
|
||||
... = k + m : {Hl})
|
||||
|
||||
theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k
|
||||
:= (add_comm k m) ▸ (add_comm k n) ▸ (add_le_left H k)
|
||||
theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k :=
|
||||
add_comm k m ▸ add_comm k n ▸ add_le_left H k
|
||||
|
||||
theorem add_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n + m ≤ k + l
|
||||
:= le_trans (add_le_right H1 m) (add_le_left H2 k)
|
||||
theorem add_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n + m ≤ k + l :=
|
||||
le_trans (add_le_right H1 m) (add_le_left H2 k)
|
||||
|
||||
|
||||
theorem add_le_cancel_left {n m k : ℕ} (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 : symm (add_assoc k n l)
|
||||
... = k + m : Hl))
|
||||
obtain (l : ℕ) (Hl : k + n + l = k + m), from (le_elim H),
|
||||
le_intro (add_cancel_left
|
||||
(calc
|
||||
k + (n + l) = k + n + l : symm (add_assoc k n l)
|
||||
... = k + m : Hl))
|
||||
|
||||
theorem add_le_cancel_right {n m k : ℕ} (H : n + k ≤ m + k) : n ≤ m :=
|
||||
add_le_cancel_left (add_comm m k ▸ add_comm n k ▸ H)
|
||||
|
||||
theorem add_le_inv {n m k l : ℕ} (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤ l :=
|
||||
obtain (a : ℕ) (Ha : k + a = n), from le_elim H2,
|
||||
have H3 : k + (a + m) ≤ k + l, from (add_assoc k a m) ▸ (symm Ha) ▸ H1,
|
||||
have H4 : a + m ≤ l, from add_le_cancel_left H3,
|
||||
show m ≤ l, from le_trans (le_add_left m a) H4
|
||||
obtain (a : ℕ) (Ha : k + a = n), from le_elim H2,
|
||||
have H3 : k + (a + m) ≤ k + l, from (add_assoc k a m) ▸ (symm Ha) ▸ H1,
|
||||
have H4 : a + m ≤ l, from add_le_cancel_left H3,
|
||||
show m ≤ l, from le_trans (le_add_left m a) H4
|
||||
|
||||
-- add_rewrite le_add_right le_add_left
|
||||
|
||||
|
|
@ -139,104 +139,104 @@ theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m :=
|
|||
le_trans H (self_le_succ m)
|
||||
|
||||
theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H),
|
||||
discriminate
|
||||
(assume H3 : k = 0,
|
||||
have Heq : n = m,
|
||||
from calc
|
||||
n = n + 0 : symm (add_zero_right n)
|
||||
... = n + k : {symm H3}
|
||||
... = m : Hk,
|
||||
or_intro_right _ Heq)
|
||||
(take l : nat,
|
||||
assume H3 : k = succ l,
|
||||
have Hlt : succ n ≤ m, from
|
||||
(le_intro
|
||||
(calc
|
||||
succ n + l = n + succ l : add_move_succ n l
|
||||
... = n + k : {symm H3}
|
||||
... = m : Hk)),
|
||||
or_intro_left _ Hlt)
|
||||
obtain (k : ℕ) (Hk : n + k = m), from (le_elim H),
|
||||
discriminate
|
||||
(assume H3 : k = 0,
|
||||
have Heq : n = m,
|
||||
from calc
|
||||
n = n + 0 : symm (add_zero_right n)
|
||||
... = n + k : {symm H3}
|
||||
... = m : Hk,
|
||||
or_intro_right _ Heq)
|
||||
(take l : nat,
|
||||
assume H3 : k = succ l,
|
||||
have Hlt : succ n ≤ m, from
|
||||
(le_intro
|
||||
(calc
|
||||
succ n + l = n + succ l : add_move_succ n l
|
||||
... = n + k : {symm H3}
|
||||
... = m : Hk)),
|
||||
or_intro_left _ Hlt)
|
||||
|
||||
theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m :=
|
||||
resolve_left (le_imp_succ_le_or_eq H1) H2
|
||||
|
||||
theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
|
||||
or_imp_or_left (le_imp_succ_le_or_eq H)
|
||||
(take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2)
|
||||
(take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2)
|
||||
|
||||
theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m :=
|
||||
obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
|
||||
and_intro
|
||||
(have H3 : n + succ k = m,
|
||||
from calc
|
||||
n + succ k = succ n + k : symm (add_move_succ n k)
|
||||
... = m : H2,
|
||||
show n ≤ m, from le_intro H3)
|
||||
(assume H3 : n = m,
|
||||
have H4 : succ n ≤ n, from subst (symm H3) H,
|
||||
have H5 : succ n = n, from le_antisym H4 (self_le_succ n),
|
||||
show false, from absurd H5 (succ_ne_self n))
|
||||
and_intro
|
||||
(have H3 : n + succ k = m,
|
||||
from calc
|
||||
n + succ k = succ n + k : symm (add_move_succ n k)
|
||||
... = m : H2,
|
||||
show n ≤ m, from le_intro H3)
|
||||
(assume H3 : n = m,
|
||||
have H4 : succ n ≤ n, from subst (symm H3) H,
|
||||
have H5 : succ n = n, from le_antisym H4 (self_le_succ n),
|
||||
show false, from absurd H5 (succ_ne_self n))
|
||||
|
||||
theorem le_pred_self (n : ℕ) : pred n ≤ n :=
|
||||
case n
|
||||
(subst (symm pred_zero) (le_refl 0))
|
||||
(take k : ℕ, subst (symm (pred_succ k)) (self_le_succ k))
|
||||
(subst (symm pred_zero) (le_refl 0))
|
||||
(take k : ℕ, subst (symm (pred_succ k)) (self_le_succ k))
|
||||
|
||||
theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
|
||||
discriminate
|
||||
(take Hn : n = 0,
|
||||
have H2 : pred n = 0,
|
||||
from calc
|
||||
pred n = pred 0 : {Hn}
|
||||
... = 0 : pred_zero,
|
||||
subst (symm H2) (zero_le (pred m)))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
have H2 : pred n + l = pred m,
|
||||
from calc
|
||||
pred n + l = pred (succ k) + l : {Hn}
|
||||
... = k + l : {pred_succ k}
|
||||
... = pred (succ (k + l)) : symm (pred_succ (k + l))
|
||||
... = pred (succ k + l) : {symm (add_succ_left k l)}
|
||||
... = pred (n + l) : {symm Hn}
|
||||
... = pred m : {Hl},
|
||||
le_intro H2)
|
||||
(take Hn : n = 0,
|
||||
have H2 : pred n = 0,
|
||||
from calc
|
||||
pred n = pred 0 : {Hn}
|
||||
... = 0 : pred_zero,
|
||||
subst (symm H2) (zero_le (pred m)))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
have H2 : pred n + l = pred m,
|
||||
from calc
|
||||
pred n + l = pred (succ k) + l : {Hn}
|
||||
... = k + l : {pred_succ k}
|
||||
... = pred (succ (k + l)) : symm (pred_succ (k + l))
|
||||
... = pred (succ k + l) : {symm (add_succ_left k l)}
|
||||
... = pred (n + l) : {symm Hn}
|
||||
... = pred m : {Hl},
|
||||
le_intro H2)
|
||||
|
||||
theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m :=
|
||||
discriminate
|
||||
(take Hn : n = 0,
|
||||
or_inl (subst (symm Hn) (zero_le m)))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
have H2 : pred n = k,
|
||||
from calc
|
||||
pred n = pred (succ k) : {Hn}
|
||||
... = k : pred_succ k,
|
||||
have H3 : k ≤ m, from subst H2 H,
|
||||
have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3,
|
||||
show n ≤ m ∨ n = succ m, from
|
||||
or_imp_or H4
|
||||
(take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5)
|
||||
(take H5 : k = m, show n = succ m, from subst H5 Hn))
|
||||
(take Hn : n = 0,
|
||||
or_inl (subst (symm Hn) (zero_le m)))
|
||||
(take k : ℕ,
|
||||
assume Hn : n = succ k,
|
||||
have H2 : pred n = k,
|
||||
from calc
|
||||
pred n = pred (succ k) : {Hn}
|
||||
... = k : pred_succ k,
|
||||
have H3 : k ≤ m, from subst H2 H,
|
||||
have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3,
|
||||
show n ≤ m ∨ n = succ m, from
|
||||
or_imp_or H4
|
||||
(take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5)
|
||||
(take H5 : k = m, show n = succ m, from subst H5 Hn))
|
||||
|
||||
|
||||
-- ### interaction with multiplication
|
||||
|
||||
theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
|
||||
have H2 : k * n + k * l = k * m, from
|
||||
calc
|
||||
k * n + k * l = k * (n + l) : by simp
|
||||
... = k * m : {Hl},
|
||||
le_intro H2
|
||||
obtain (l : ℕ) (Hl : n + l = m), from (le_elim H),
|
||||
have H2 : k * n + k * l = k * m, from
|
||||
calc
|
||||
k * n + k * l = k * (n + l) : by simp
|
||||
... = k * m : {Hl},
|
||||
le_intro H2
|
||||
|
||||
theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k
|
||||
:= mul_comm k m ▸ mul_comm k n ▸ (mul_le_left H k)
|
||||
theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k :=
|
||||
mul_comm k m ▸ mul_comm k n ▸ (mul_le_left H k)
|
||||
|
||||
theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l
|
||||
:= le_trans (mul_le_right H1 m) (mul_le_left H2 k)
|
||||
theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
|
||||
le_trans (mul_le_right H1 m) (mul_le_left H2 k)
|
||||
|
||||
-- mul_le_[left|right]_inv below
|
||||
|
||||
|
|
@ -291,8 +291,8 @@ not_succ_zero_le n
|
|||
|
||||
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
||||
discriminate
|
||||
(take (Hm : m = 0), absurd_elim _ (subst Hm H) (not_lt_zero n))
|
||||
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
|
||||
(take (Hm : m = 0), absurd_elim _ (subst Hm H) (not_lt_zero n))
|
||||
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
|
||||
|
||||
-- ### interaction with le
|
||||
|
||||
|
|
@ -342,115 +342,113 @@ le_imp_not_gt (lt_imp_le H)
|
|||
|
||||
-- ### interaction with addition
|
||||
|
||||
theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m
|
||||
:= add_succ_right k n ▸ add_le_left H k
|
||||
theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m :=
|
||||
add_succ_right k n ▸ add_le_left H k
|
||||
|
||||
theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k
|
||||
:= add_comm k m ▸ add_comm k n ▸ add_lt_left H k
|
||||
theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k :=
|
||||
add_comm k m ▸ add_comm k n ▸ add_lt_left H k
|
||||
|
||||
theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l
|
||||
:= le_lt_trans (add_le_right H1 m) (add_lt_left H2 k)
|
||||
theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l :=
|
||||
le_lt_trans (add_le_right H1 m) (add_lt_left H2 k)
|
||||
|
||||
theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l
|
||||
:= lt_le_trans (add_lt_right H1 m) (add_le_left H2 k)
|
||||
theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l :=
|
||||
lt_le_trans (add_lt_right H1 m) (add_le_left H2 k)
|
||||
|
||||
theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l
|
||||
:= add_lt_le H1 (lt_imp_le H2)
|
||||
theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l :=
|
||||
add_lt_le H1 (lt_imp_le H2)
|
||||
|
||||
theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m
|
||||
:= add_le_cancel_left (add_succ_right k n⁻¹ ▸ H)
|
||||
theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m :=
|
||||
add_le_cancel_left (add_succ_right k n⁻¹ ▸ H)
|
||||
|
||||
theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m
|
||||
:= add_lt_cancel_left (add_comm m k ▸ add_comm n k ▸ H)
|
||||
theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m :=
|
||||
add_lt_cancel_left (add_comm m k ▸ add_comm n k ▸ H)
|
||||
|
||||
-- ### interaction with successor (see also the interaction with le)
|
||||
|
||||
theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m
|
||||
:= add_one m ▸ add_one n ▸ add_lt_right H 1
|
||||
theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m :=
|
||||
add_one m ▸ add_one n ▸ add_lt_right H 1
|
||||
|
||||
theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) : n < m
|
||||
:= add_lt_cancel_right (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) : n < m :=
|
||||
add_lt_cancel_right (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H)
|
||||
|
||||
theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m
|
||||
:= lt_trans H (self_lt_succ m)
|
||||
:= lt_trans H (self_lt_succ m)
|
||||
|
||||
-- ### totality of lt and le
|
||||
|
||||
theorem le_or_gt (n m : ℕ) : n ≤ m ∨ n > m
|
||||
:= induction_on n
|
||||
(or_inl (zero_le m))
|
||||
(take (k : ℕ),
|
||||
assume IH : k ≤ m ∨ m < k,
|
||||
or_elim IH
|
||||
(assume H : k ≤ m,
|
||||
obtain (l : ℕ) (Hl : k + l = m), from le_elim H,
|
||||
discriminate
|
||||
(assume H2 : l = 0,
|
||||
have H3 : m = k,
|
||||
from calc
|
||||
m = k + l : symm Hl
|
||||
... = k + 0 : {H2}
|
||||
... = k : add_zero_right k,
|
||||
have H4 : m < succ k, from subst H3 (self_lt_succ m),
|
||||
or_inr H4)
|
||||
(take l2 : ℕ,
|
||||
assume H2 : l = succ l2,
|
||||
have H3 : succ k + l2 = m,
|
||||
from calc
|
||||
succ k + l2 = k + succ l2 : add_move_succ k l2
|
||||
... = k + l : {symm H2}
|
||||
... = m : Hl,
|
||||
or_inl (le_intro H3)))
|
||||
(assume H : m < k, or_inr (lt_imp_lt_succ H)))
|
||||
theorem le_or_gt (n m : ℕ) : n ≤ m ∨ n > m :=
|
||||
induction_on n
|
||||
(or_inl (zero_le m))
|
||||
(take (k : ℕ),
|
||||
assume IH : k ≤ m ∨ m < k,
|
||||
or_elim IH
|
||||
(assume H : k ≤ m,
|
||||
obtain (l : ℕ) (Hl : k + l = m), from le_elim H,
|
||||
discriminate
|
||||
(assume H2 : l = 0,
|
||||
have H3 : m = k,
|
||||
from calc
|
||||
m = k + l : symm Hl
|
||||
... = k + 0 : {H2}
|
||||
... = k : add_zero_right k,
|
||||
have H4 : m < succ k, from subst H3 (self_lt_succ m),
|
||||
or_inr H4)
|
||||
(take l2 : ℕ,
|
||||
assume H2 : l = succ l2,
|
||||
have H3 : succ k + l2 = m,
|
||||
from calc
|
||||
succ k + l2 = k + succ l2 : add_move_succ k l2
|
||||
... = k + l : {symm H2}
|
||||
... = m : Hl,
|
||||
or_inl (le_intro H3)))
|
||||
(assume H : m < k, or_inr (lt_imp_lt_succ H)))
|
||||
|
||||
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m
|
||||
:= or_imp_or_left (le_or_gt n m) (assume H : n ≤ m, le_imp_lt_or_eq H)
|
||||
theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
|
||||
or_imp_or_left (le_or_gt n m) (assume H : n ≤ m, le_imp_lt_or_eq H)
|
||||
|
||||
theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
|
||||
iff_elim_left (or_assoc _ _ _) (trichotomy_alt n m)
|
||||
|
||||
theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n
|
||||
:= or_imp_or_right (le_or_gt n m) (assume H : m < n, lt_imp_le H)
|
||||
theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
|
||||
or_imp_or_right (le_or_gt n m) (assume H : m < n, lt_imp_le H)
|
||||
|
||||
theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m
|
||||
:= resolve_left (le_or_gt m n) H
|
||||
theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m :=
|
||||
resolve_left (le_or_gt m n) H
|
||||
|
||||
theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m
|
||||
:= resolve_right (le_or_gt n m) H
|
||||
theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
|
||||
resolve_right (le_or_gt n m) H
|
||||
|
||||
-- Note: interaction with multiplication under "positivity"
|
||||
|
||||
-- ### misc
|
||||
|
||||
theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n
|
||||
:=
|
||||
have H1 : ∀n, ∀m, m < n → P m, from
|
||||
take n,
|
||||
induction_on n
|
||||
(show ∀m, m < 0 → P m, from take m H, absurd_elim _ H (not_lt_zero _))
|
||||
(take n',
|
||||
assume IH : ∀m, m < n' → P m,
|
||||
have H2: P n', from H n' IH,
|
||||
show ∀m, m < succ n' → P m, from
|
||||
take m,
|
||||
assume H3 : m < succ n',
|
||||
or_elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
|
||||
(assume H4: m < n', IH _ H4)
|
||||
(assume H4: m = n', H4⁻¹ ▸ H2)),
|
||||
H1 _ _ (self_lt_succ n)
|
||||
theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
|
||||
have H1 : ∀n, ∀m, m < n → P m, from
|
||||
take n,
|
||||
induction_on n
|
||||
(show ∀m, m < 0 → P m, from take m H, absurd_elim _ H (not_lt_zero _))
|
||||
(take n',
|
||||
assume IH : ∀m, m < n' → P m,
|
||||
have H2: P n', from H n' IH,
|
||||
show ∀m, m < succ n' → P m, from
|
||||
take m,
|
||||
assume H3 : m < succ n',
|
||||
or_elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
|
||||
(assume H4: m < n', IH _ H4)
|
||||
(assume H4: m = n', H4⁻¹ ▸ H2)),
|
||||
H1 _ _ (self_lt_succ n)
|
||||
|
||||
theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
|
||||
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a
|
||||
:=
|
||||
strong_induction_on a (
|
||||
take n,
|
||||
show (∀m, m < n → P m) → P n, from
|
||||
case n
|
||||
(assume H : (∀m, m < 0 → P m), show P 0, from H0)
|
||||
(take n,
|
||||
assume H : (∀m, m < succ n → P m),
|
||||
show P (succ n), from
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1))))
|
||||
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
|
||||
strong_induction_on a (
|
||||
take n,
|
||||
show (∀m, m < n → P m) → P n, from
|
||||
case n
|
||||
(assume H : (∀m, m < 0 → P m), show P 0, from H0)
|
||||
(take n,
|
||||
assume H : (∀m, m < succ n → P m),
|
||||
show P (succ n), from
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1))))
|
||||
|
||||
-- Positivity
|
||||
-- ---------
|
||||
|
|
@ -461,136 +459,127 @@ theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
|
|||
|
||||
-- See also succ_pos.
|
||||
|
||||
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y
|
||||
:= case y H0 (take y', H1 _ (succ_pos _))
|
||||
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y :=
|
||||
case y H0 (take y', H1 _ (succ_pos _))
|
||||
|
||||
theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0
|
||||
:= or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
|
||||
theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
|
||||
or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
|
||||
|
||||
theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0
|
||||
:= H⁻¹ ▸ (succ_pos m)
|
||||
theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
|
||||
H⁻¹ ▸ (succ_pos m)
|
||||
|
||||
theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0
|
||||
:= or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
|
||||
theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
|
||||
|
||||
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l
|
||||
:= lt_imp_eq_succ H
|
||||
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
||||
lt_imp_eq_succ H
|
||||
|
||||
theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
|
||||
:= (add_zero_right n) ▸ (add_lt_left H n)
|
||||
theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n :=
|
||||
(add_zero_right n) ▸ (add_lt_left H n)
|
||||
|
||||
theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n
|
||||
:= (add_comm n k) ▸ (add_pos_right n H)
|
||||
theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n :=
|
||||
(add_comm n k) ▸ (add_pos_right n H)
|
||||
|
||||
-- ### multiplication
|
||||
|
||||
theorem mul_pos {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0
|
||||
:=
|
||||
obtain (k : ℕ) (Hk : n = succ k), from pos_imp_eq_succ Hn,
|
||||
obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm,
|
||||
succ_imp_pos (calc
|
||||
n * m = succ k * m : {Hk}
|
||||
... = succ k * succ l : {Hl}
|
||||
... = succ k * l + succ k : mul_succ_right (succ k) l
|
||||
... = succ (succ k * l + k) : add_succ_right _ _)
|
||||
theorem mul_pos {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0 :=
|
||||
obtain (k : ℕ) (Hk : n = succ k), from pos_imp_eq_succ Hn,
|
||||
obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm,
|
||||
succ_imp_pos (calc
|
||||
n * m = succ k * m : {Hk}
|
||||
... = succ k * succ l : {Hl}
|
||||
... = succ k * l + succ k : mul_succ_right (succ k) l
|
||||
... = succ (succ k * l + k) : add_succ_right _ _)
|
||||
|
||||
theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0
|
||||
:=
|
||||
discriminate
|
||||
(assume H2 : n = 0,
|
||||
have H3 : n * m = 0,
|
||||
from calc
|
||||
n * m = 0 * m : {H2}
|
||||
... = 0 : mul_zero_left m,
|
||||
have H4 : 0 > 0, from H3 ▸ H,
|
||||
absurd_elim _ H4 (lt_irrefl 0))
|
||||
(take l : nat,
|
||||
assume Hl : n = succ l,
|
||||
Hl⁻¹ ▸ (succ_pos l))
|
||||
theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0 :=
|
||||
discriminate
|
||||
(assume H2 : n = 0,
|
||||
have H3 : n * m = 0,
|
||||
from calc
|
||||
n * m = 0 * m : {H2}
|
||||
... = 0 : mul_zero_left m,
|
||||
have H4 : 0 > 0, from H3 ▸ H,
|
||||
absurd_elim _ H4 (lt_irrefl 0))
|
||||
(take l : nat,
|
||||
assume Hl : n = succ l,
|
||||
Hl⁻¹ ▸ (succ_pos l))
|
||||
|
||||
theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0
|
||||
:= mul_pos_imp_pos_left ((mul_comm n m) ▸ H)
|
||||
theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 :=
|
||||
mul_pos_imp_pos_left ((mul_comm n m) ▸ H)
|
||||
|
||||
-- See also mul_eq_one below.
|
||||
|
||||
-- ### interaction of mul with le and lt
|
||||
|
||||
theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m
|
||||
:=
|
||||
have H2 : k * n < k * n + k, from add_pos_right (k * n) Hk,
|
||||
have H3 : k * n + k ≤ k * m, from (mul_succ_right k n) ▸ (mul_le_left H k),
|
||||
lt_le_trans H2 H3
|
||||
theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
|
||||
have H2 : k * n < k * n + k, from add_pos_right (k * n) Hk,
|
||||
have H3 : k * n + k ≤ k * m, from (mul_succ_right k n) ▸ (mul_le_left H k),
|
||||
lt_le_trans H2 H3
|
||||
|
||||
theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k
|
||||
:= subst (mul_comm k m) (subst (mul_comm k n) (mul_lt_left Hk H))
|
||||
theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k :=
|
||||
subst (mul_comm k m) (subst (mul_comm k n) (mul_lt_left Hk H))
|
||||
|
||||
theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l
|
||||
:= le_lt_trans (mul_le_right H1 m) (mul_lt_left Hk H2)
|
||||
theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l :=
|
||||
le_lt_trans (mul_le_right H1 m) (mul_lt_left Hk H2)
|
||||
|
||||
theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l
|
||||
:= le_lt_trans (mul_le_left H2 n) (mul_lt_right Hl H1)
|
||||
theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l :=
|
||||
le_lt_trans (mul_le_left H2 n) (mul_lt_right Hl H1)
|
||||
|
||||
theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l
|
||||
:=
|
||||
have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
|
||||
have H4 : k * m < k * l, from mul_lt_left (le_lt_trans (zero_le n) H1) H2,
|
||||
le_lt_trans H3 H4
|
||||
theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
|
||||
have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
|
||||
have H4 : k * m < k * l, from mul_lt_left (le_lt_trans (zero_le n) H1) H2,
|
||||
le_lt_trans H3 H4
|
||||
|
||||
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m
|
||||
:=
|
||||
or_elim (le_or_gt m n)
|
||||
(assume H2 : m ≤ n,
|
||||
have H3 : k * m ≤ k * n, from mul_le_left H2 k,
|
||||
absurd_elim _ H3 (lt_imp_not_ge H))
|
||||
(assume H2 : n < m, H2)
|
||||
theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
|
||||
or_elim (le_or_gt m n)
|
||||
(assume H2 : m ≤ n,
|
||||
have H3 : k * m ≤ k * n, from mul_le_left H2 k,
|
||||
absurd_elim _ H3 (lt_imp_not_ge H))
|
||||
(assume H2 : n < m, H2)
|
||||
|
||||
theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m
|
||||
:= mul_lt_cancel_left ((mul_comm m k) ▸ (mul_comm n k) ▸ H)
|
||||
theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
|
||||
mul_lt_cancel_left ((mul_comm m k) ▸ (mul_comm n k) ▸ H)
|
||||
|
||||
theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m
|
||||
:=
|
||||
have H2 : k * n < k * m + k, from le_lt_trans H (add_pos_right _ Hk),
|
||||
have H3 : k * n < k * succ m, from (mul_succ_right k m)⁻¹ ▸ H2,
|
||||
have H4 : n < succ m, from mul_lt_cancel_left H3,
|
||||
show n ≤ m, from lt_succ_imp_le H4
|
||||
theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
|
||||
have H2 : k * n < k * m + k, from le_lt_trans H (add_pos_right _ Hk),
|
||||
have H3 : k * n < k * succ m, from (mul_succ_right k m)⁻¹ ▸ H2,
|
||||
have H4 : n < succ m, from mul_lt_cancel_left H3,
|
||||
show n ≤ m, from lt_succ_imp_le H4
|
||||
|
||||
theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n ≤ k
|
||||
:= mul_le_cancel_left Hm ((mul_comm k m) ▸ (mul_comm n m) ▸ H)
|
||||
theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n ≤ k :=
|
||||
mul_le_cancel_left Hm ((mul_comm k m) ▸ (mul_comm n m) ▸ H)
|
||||
|
||||
theorem mul_cancel_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k
|
||||
:=
|
||||
have H2 : n * m ≤ n * k, from H ▸ (le_refl (n * m)),
|
||||
have H3 : n * k ≤ n * m, from H ▸ (le_refl (n * m)),
|
||||
have H4 : m ≤ k, from mul_le_cancel_left Hn H2,
|
||||
have H5 : k ≤ m, from mul_le_cancel_left Hn H3,
|
||||
le_antisym H4 H5
|
||||
theorem mul_cancel_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
|
||||
have H2 : n * m ≤ n * k, from H ▸ (le_refl (n * m)),
|
||||
have H3 : n * k ≤ n * m, from H ▸ (le_refl (n * m)),
|
||||
have H4 : m ≤ k, from mul_le_cancel_left Hn H2,
|
||||
have H5 : k ≤ m, from mul_le_cancel_left Hn H3,
|
||||
le_antisym H4 H5
|
||||
|
||||
theorem mul_cancel_left_or {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k
|
||||
:=
|
||||
or_imp_or_right (zero_or_pos n)
|
||||
(assume Hn : n > 0, mul_cancel_left Hn H)
|
||||
theorem mul_cancel_left_or {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
|
||||
or_imp_or_right (zero_or_pos n)
|
||||
(assume Hn : n > 0, mul_cancel_left Hn H)
|
||||
|
||||
theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k
|
||||
:= mul_cancel_left Hm (subst (subst H (mul_comm n m)) (mul_comm k m))
|
||||
theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
|
||||
mul_cancel_left Hm (subst (subst H (mul_comm n m)) (mul_comm k m))
|
||||
|
||||
theorem mul_cancel_right_or {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k
|
||||
:= mul_cancel_left_or (subst (subst H (mul_comm n m)) (mul_comm k m))
|
||||
theorem mul_cancel_right_or {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k :=
|
||||
mul_cancel_left_or (subst (subst H (mul_comm n m)) (mul_comm k m))
|
||||
|
||||
theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1
|
||||
:=
|
||||
have H2 : n * m > 0, from H⁻¹ ▸ succ_pos 0,
|
||||
have H3 : n > 0, from mul_pos_imp_pos_left H2,
|
||||
have H4 : m > 0, from mul_pos_imp_pos_right H2,
|
||||
or_elim (le_or_gt n 1)
|
||||
(assume H5 : n ≤ 1,
|
||||
show n = 1, from le_antisym H5 H3)
|
||||
(assume H5 : n > 1,
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
|
||||
have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6,
|
||||
absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7))
|
||||
theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
|
||||
have H2 : n * m > 0, from H⁻¹ ▸ succ_pos 0,
|
||||
have H3 : n > 0, from mul_pos_imp_pos_left H2,
|
||||
have H4 : m > 0, from mul_pos_imp_pos_right H2,
|
||||
or_elim (le_or_gt n 1)
|
||||
(assume H5 : n ≤ 1,
|
||||
show n = 1, from le_antisym H5 H3)
|
||||
(assume H5 : n > 1,
|
||||
have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
|
||||
have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6,
|
||||
absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7))
|
||||
|
||||
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1
|
||||
:= mul_eq_one_left ((mul_comm n m) ▸ H)
|
||||
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
|
||||
mul_eq_one_left ((mul_comm n m) ▸ H)
|
||||
|
||||
--- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
|
||||
--- := and_intro (mul_eq_one_left H) (mul_eq_one_right H)
|
||||
|
|
|
|||
|
|
@ -27,15 +27,14 @@ theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
|
|||
|
||||
opaque_hint (hiding sub)
|
||||
|
||||
theorem sub_zero_left (n : ℕ) : 0 - n = 0
|
||||
:=
|
||||
induction_on n (sub_zero_right 0)
|
||||
(take k : nat,
|
||||
assume IH : 0 - k = 0,
|
||||
calc
|
||||
0 - succ k = pred (0 - k) : sub_succ_right 0 k
|
||||
... = pred 0 : {IH}
|
||||
... = 0 : pred_zero)
|
||||
theorem sub_zero_left (n : ℕ) : 0 - n = 0 :=
|
||||
induction_on n (sub_zero_right 0)
|
||||
(take k : nat,
|
||||
assume IH : 0 - k = 0,
|
||||
calc
|
||||
0 - succ k = pred (0 - k) : sub_succ_right 0 k
|
||||
... = pred 0 : {IH}
|
||||
... = 0 : pred_zero)
|
||||
--(
|
||||
--theorem sub_succ_left (n m : ℕ) : pred (succ n - m) = n - m
|
||||
-- :=
|
||||
|
|
@ -50,322 +49,301 @@ theorem sub_zero_left (n : ℕ) : 0 - n = 0
|
|||
--)
|
||||
|
||||
--succ_sub_succ
|
||||
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 (succ n) 0
|
||||
... = pred (succ n) : {sub_zero_right (succ n)}
|
||||
... = n : pred_succ n
|
||||
... = n - 0 : symm (sub_zero_right n))
|
||||
(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 (succ n) (succ k)
|
||||
... = pred (n - k) : {IH}
|
||||
... = n - succ k : symm (sub_succ_right n k))
|
||||
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 (succ n) 0
|
||||
... = pred (succ n) : {sub_zero_right (succ n)}
|
||||
... = n : pred_succ n
|
||||
... = n - 0 : symm (sub_zero_right n))
|
||||
(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 (succ n) (succ k)
|
||||
... = pred (n - k) : {IH}
|
||||
... = n - succ k : symm (sub_succ_right n k))
|
||||
|
||||
theorem sub_self (n : ℕ) : n - n = 0
|
||||
:= induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH)
|
||||
theorem sub_self (n : ℕ) : n - n = 0 :=
|
||||
induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH)
|
||||
|
||||
-- TODO: add_sub_add_right
|
||||
theorem sub_add_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m
|
||||
:=
|
||||
induction_on k
|
||||
(calc
|
||||
(n + 0) - (m + 0) = n - (m + 0) : {add_zero_right _}
|
||||
... = n - m : {add_zero_right _})
|
||||
(take l : nat,
|
||||
assume IH : (n + l) - (m + l) = n - m,
|
||||
calc
|
||||
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right _ _}
|
||||
... = succ (n + l) - succ (m + l) : {add_succ_right _ _}
|
||||
... = (n + l) - (m + l) : sub_succ_succ _ _
|
||||
... = n - m : IH)
|
||||
theorem sub_add_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
|
||||
induction_on k
|
||||
(calc
|
||||
(n + 0) - (m + 0) = n - (m + 0) : {add_zero_right _}
|
||||
... = n - m : {add_zero_right _})
|
||||
(take l : nat,
|
||||
assume IH : (n + l) - (m + l) = n - m,
|
||||
calc
|
||||
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right _ _}
|
||||
... = succ (n + l) - succ (m + l) : {add_succ_right _ _}
|
||||
... = (n + l) - (m + l) : sub_succ_succ _ _
|
||||
... = n - m : IH)
|
||||
|
||||
theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m
|
||||
:= add_comm m k ▸ add_comm n k ▸ sub_add_add_right n k m
|
||||
theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
|
||||
add_comm m k ▸ add_comm n k ▸ sub_add_add_right n k m
|
||||
|
||||
-- TODO: add_sub_inv
|
||||
theorem sub_add_left (n m : ℕ) : n + m - m = n
|
||||
:=
|
||||
induction_on m
|
||||
((add_zero_right n)⁻¹ ▸ sub_zero_right n)
|
||||
(take k : ℕ,
|
||||
assume IH : n + k - k = n,
|
||||
calc
|
||||
n + succ k - succ k = succ (n + k) - succ k : {add_succ_right n k}
|
||||
... = n + k - k : sub_succ_succ _ _
|
||||
... = n : IH)
|
||||
theorem sub_add_left (n m : ℕ) : n + m - m = n :=
|
||||
induction_on m
|
||||
((add_zero_right n)⁻¹ ▸ sub_zero_right n)
|
||||
(take k : ℕ,
|
||||
assume IH : n + k - k = n,
|
||||
calc
|
||||
n + succ k - succ k = succ (n + k) - succ k : {add_succ_right n k}
|
||||
... = n + k - k : sub_succ_succ _ _
|
||||
... = n : IH)
|
||||
|
||||
-- TODO: add_sub_inv'
|
||||
theorem sub_add_left2 (n m : ℕ) : n + m - n = m
|
||||
:= add_comm m n ▸ sub_add_left m n
|
||||
theorem sub_add_left2 (n m : ℕ) : n + m - n = m :=
|
||||
add_comm m n ▸ sub_add_left m n
|
||||
|
||||
theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k)
|
||||
:=
|
||||
induction_on k
|
||||
(calc
|
||||
n - m - 0 = n - m : sub_zero_right _
|
||||
... = n - (m + 0) : {symm (add_zero_right m)})
|
||||
(take l : nat,
|
||||
assume IH : n - m - l = n - (m + l),
|
||||
calc
|
||||
n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l
|
||||
... = pred (n - (m + l)) : {IH}
|
||||
... = n - succ (m + l) : symm (sub_succ_right n (m + l))
|
||||
... = n - (m + succ l) : {symm (add_succ_right m l)})
|
||||
theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
|
||||
induction_on k
|
||||
(calc
|
||||
n - m - 0 = n - m : sub_zero_right _
|
||||
... = n - (m + 0) : {symm (add_zero_right m)})
|
||||
(take l : nat,
|
||||
assume IH : n - m - l = n - (m + l),
|
||||
calc
|
||||
n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l
|
||||
... = pred (n - (m + l)) : {IH}
|
||||
... = n - succ (m + l) : symm (sub_succ_right n (m + l))
|
||||
... = n - (m + succ l) : {symm (add_succ_right m l)})
|
||||
|
||||
theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k
|
||||
:=
|
||||
calc
|
||||
succ n - m - succ k = succ n - (m + succ k) : sub_sub _ _ _
|
||||
... = succ n - succ (m + k) : {add_succ_right m k}
|
||||
... = n - (m + k) : sub_succ_succ _ _
|
||||
... = n - m - k : symm (sub_sub n m k)
|
||||
theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k :=
|
||||
calc
|
||||
succ n - m - succ k = succ n - (m + succ k) : sub_sub _ _ _
|
||||
... = succ n - succ (m + k) : {add_succ_right m k}
|
||||
... = n - (m + k) : sub_succ_succ _ _
|
||||
... = n - m - k : symm (sub_sub n m k)
|
||||
|
||||
theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0
|
||||
:=
|
||||
calc
|
||||
n - (n + m) = n - n - m : symm (sub_sub n n m)
|
||||
... = 0 - m : {sub_self n}
|
||||
... = 0 : sub_zero_left m
|
||||
theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0 :=
|
||||
calc
|
||||
n - (n + m) = n - n - m : symm (sub_sub n n m)
|
||||
... = 0 - m : {sub_self n}
|
||||
... = 0 : sub_zero_left m
|
||||
|
||||
theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n
|
||||
:=
|
||||
calc
|
||||
m - n - k = m - (n + k) : sub_sub m n k
|
||||
... = m - (k + n) : {add_comm n k}
|
||||
... = m - k - n : symm (sub_sub m k n)
|
||||
theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n :=
|
||||
calc
|
||||
m - n - k = m - (n + k) : sub_sub m n k
|
||||
... = m - (k + n) : {add_comm n k}
|
||||
... = m - k - n : symm (sub_sub m k n)
|
||||
|
||||
theorem sub_one (n : ℕ) : n - 1 = pred n
|
||||
:=
|
||||
calc
|
||||
n - 1 = pred (n - 0) : sub_succ_right n 0
|
||||
... = pred n : {sub_zero_right n}
|
||||
theorem sub_one (n : ℕ) : n - 1 = pred n :=
|
||||
calc
|
||||
n - 1 = pred (n - 0) : sub_succ_right n 0
|
||||
... = pred n : {sub_zero_right n}
|
||||
|
||||
theorem succ_sub_one (n : ℕ) : succ n - 1 = n
|
||||
:= trans (sub_succ_succ n 0) (sub_zero_right n)
|
||||
theorem succ_sub_one (n : ℕ) : succ n - 1 = n :=
|
||||
trans (sub_succ_succ n 0) (sub_zero_right n)
|
||||
|
||||
-- add_rewrite sub_add_left
|
||||
|
||||
-- ### interaction with multiplication
|
||||
|
||||
theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m
|
||||
:=
|
||||
induction_on n
|
||||
(calc
|
||||
pred 0 * m = 0 * m : {pred_zero}
|
||||
... = 0 : mul_zero_left _
|
||||
... = 0 - m : symm (sub_zero_left m)
|
||||
... = 0 * m - m : {symm (mul_zero_left m)})
|
||||
(take k : nat,
|
||||
assume IH : pred k * m = k * m - m,
|
||||
calc
|
||||
pred (succ k) * m = k * m : {pred_succ k}
|
||||
... = k * m + m - m : symm (sub_add_left _ _)
|
||||
... = succ k * m - m : {symm (mul_succ_left k m)})
|
||||
theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
|
||||
induction_on n
|
||||
(calc
|
||||
pred 0 * m = 0 * m : {pred_zero}
|
||||
... = 0 : mul_zero_left _
|
||||
... = 0 - m : symm (sub_zero_left m)
|
||||
... = 0 * m - m : {symm (mul_zero_left m)})
|
||||
(take k : nat,
|
||||
assume IH : pred k * m = k * m - m,
|
||||
calc
|
||||
pred (succ k) * m = k * m : {pred_succ k}
|
||||
... = k * m + m - m : symm (sub_add_left _ _)
|
||||
... = succ k * m - m : {symm (mul_succ_left k m)})
|
||||
|
||||
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n
|
||||
:=
|
||||
calc n * pred m = pred m * n : mul_comm _ _
|
||||
... = m * n - n : mul_pred_left m n
|
||||
... = n * m - n : {mul_comm m n}
|
||||
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
|
||||
calc n * pred m = pred m * n : mul_comm _ _
|
||||
... = m * n - n : mul_pred_left m n
|
||||
... = n * m - n : {mul_comm m n}
|
||||
|
||||
theorem mul_sub_distr_right (n m k : ℕ) : (n - m) * k = n * k - m * k
|
||||
:=
|
||||
induction_on m
|
||||
(calc
|
||||
(n - 0) * k = n * k : {sub_zero_right n}
|
||||
... = n * k - 0 : symm (sub_zero_right _)
|
||||
... = n * k - 0 * k : {symm (mul_zero_left _)})
|
||||
(take l : nat,
|
||||
assume IH : (n - l) * k = n * k - l * k,
|
||||
calc
|
||||
(n - succ l) * k = pred (n - l) * k : {sub_succ_right n l}
|
||||
... = (n - l) * k - k : mul_pred_left _ _
|
||||
... = n * k - l * k - k : {IH}
|
||||
... = n * k - (l * k + k) : sub_sub _ _ _
|
||||
... = n * k - (succ l * k) : {symm (mul_succ_left l k)})
|
||||
theorem mul_sub_distr_right (n m k : ℕ) : (n - m) * k = n * k - m * k :=
|
||||
induction_on m
|
||||
(calc
|
||||
(n - 0) * k = n * k : {sub_zero_right n}
|
||||
... = n * k - 0 : symm (sub_zero_right _)
|
||||
... = n * k - 0 * k : {symm (mul_zero_left _)})
|
||||
(take l : nat,
|
||||
assume IH : (n - l) * k = n * k - l * k,
|
||||
calc
|
||||
(n - succ l) * k = pred (n - l) * k : {sub_succ_right n l}
|
||||
... = (n - l) * k - k : mul_pred_left _ _
|
||||
... = n * k - l * k - k : {IH}
|
||||
... = n * k - (l * k + k) : sub_sub _ _ _
|
||||
... = n * k - (succ l * k) : {symm (mul_succ_left l k)})
|
||||
|
||||
theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k
|
||||
:=
|
||||
calc
|
||||
n * (m - k) = (m - k) * n : mul_comm _ _
|
||||
... = m * n - k * n : mul_sub_distr_right _ _ _
|
||||
... = n * m - k * n : {mul_comm _ _}
|
||||
... = n * m - n * k : {mul_comm _ _}
|
||||
theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k :=
|
||||
calc
|
||||
n * (m - k) = (m - k) * n : mul_comm _ _
|
||||
... = m * n - k * n : mul_sub_distr_right _ _ _
|
||||
... = n * m - k * n : {mul_comm _ _}
|
||||
... = n * m - n * k : {mul_comm _ _}
|
||||
|
||||
-- ### interaction with inequalities
|
||||
|
||||
theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n)
|
||||
:=
|
||||
sub_induction n m
|
||||
(take k,
|
||||
assume H : 0 ≤ k,
|
||||
calc
|
||||
succ k - 0 = succ k : sub_zero_right (succ k)
|
||||
... = succ (k - 0) : {symm (sub_zero_right k)})
|
||||
(take k,
|
||||
assume H : succ k ≤ 0,
|
||||
absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k l,
|
||||
assume IH : k ≤ l → succ l - k = succ (l - k),
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ (succ l) - succ k = succ l - k : sub_succ_succ (succ l) k
|
||||
... = succ (l - k) : IH (succ_le_cancel H)
|
||||
... = succ (succ l - succ k) : {symm (sub_succ_succ l k)})
|
||||
theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) :=
|
||||
sub_induction n m
|
||||
(take k,
|
||||
assume H : 0 ≤ k,
|
||||
calc
|
||||
succ k - 0 = succ k : sub_zero_right (succ k)
|
||||
... = succ (k - 0) : {symm (sub_zero_right k)})
|
||||
(take k,
|
||||
assume H : succ k ≤ 0,
|
||||
absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k l,
|
||||
assume IH : k ≤ l → succ l - k = succ (l - k),
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ (succ l) - succ k = succ l - k : sub_succ_succ (succ l) k
|
||||
... = succ (l - k) : IH (succ_le_cancel H)
|
||||
... = succ (succ l - succ k) : {symm (sub_succ_succ l k)})
|
||||
|
||||
theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0
|
||||
:= obtain (k : ℕ) (Hk : n + k = m), from le_elim H, Hk ▸ sub_add_right_eq_zero n k
|
||||
theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0 :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le_elim H, Hk ▸ sub_add_right_eq_zero n k
|
||||
|
||||
theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
|
||||
:=
|
||||
sub_induction n m
|
||||
(take k,
|
||||
assume H : 0 ≤ k,
|
||||
calc
|
||||
0 + (k - 0) = k - 0 : add_zero_left (k - 0)
|
||||
... = k : sub_zero_right k)
|
||||
(take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k l,
|
||||
assume IH : k ≤ l → k + (l - k) = l,
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k}
|
||||
... = succ (k + (l - k)) : add_succ_left k (l - k)
|
||||
... = succ l : {IH (succ_le_cancel H)})
|
||||
theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m :=
|
||||
sub_induction n m
|
||||
(take k,
|
||||
assume H : 0 ≤ k,
|
||||
calc
|
||||
0 + (k - 0) = k - 0 : add_zero_left (k - 0)
|
||||
... = k : sub_zero_right k)
|
||||
(take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k l,
|
||||
assume IH : k ≤ l → k + (l - k) = l,
|
||||
take H : succ k ≤ succ l,
|
||||
calc
|
||||
succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k}
|
||||
... = succ (k + (l - k)) : add_succ_left k (l - k)
|
||||
... = succ l : {IH (succ_le_cancel H)})
|
||||
|
||||
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n
|
||||
:= add_comm m (n - m) ▸ add_sub_le
|
||||
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
|
||||
add_comm m (n - m) ▸ add_sub_le
|
||||
|
||||
theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n
|
||||
:=
|
||||
calc
|
||||
n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
|
||||
... = n : add_zero_right n
|
||||
theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
|
||||
calc
|
||||
n + (m - n) = n + 0 : {le_imp_sub_eq_zero H}
|
||||
... = n : add_zero_right n
|
||||
|
||||
theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m
|
||||
:= add_comm m (n - m) ▸ add_sub_ge
|
||||
theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
|
||||
add_comm m (n - m) ▸ add_sub_ge
|
||||
|
||||
theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n)
|
||||
:=
|
||||
or_elim (le_total n m)
|
||||
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
|
||||
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl n)
|
||||
theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) :=
|
||||
or_elim (le_total n m)
|
||||
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
|
||||
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl n)
|
||||
|
||||
theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n)
|
||||
:= or_elim (le_total n m)
|
||||
(assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m))
|
||||
(assume H : m ≤ n, subst (symm (add_sub_ge H)) H)
|
||||
theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) :=
|
||||
or_elim (le_total n m)
|
||||
(assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m))
|
||||
(assume H : m ≤ n, subst (symm (add_sub_ge H)) H)
|
||||
|
||||
theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k)
|
||||
: P (n - m)
|
||||
:= or_elim (le_total n m)
|
||||
(assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3))
|
||||
(assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3))
|
||||
: P (n - m) :=
|
||||
or_elim (le_total n m)
|
||||
(assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3))
|
||||
(assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3))
|
||||
|
||||
theorem sub_le_self (n m : ℕ) : n - m ≤ n
|
||||
:=
|
||||
sub_split
|
||||
(assume H : n ≤ m, zero_le n)
|
||||
(take k : ℕ, assume H : m + k = n, le_intro (subst (add_comm m k) H))
|
||||
theorem sub_le_self (n m : ℕ) : n - m ≤ n :=
|
||||
sub_split
|
||||
(assume H : n ≤ m, zero_le n)
|
||||
(take k : ℕ, assume H : m + k = n, le_intro (subst (add_comm m k) H))
|
||||
|
||||
theorem le_elim_sub (n m : ℕ) (H : n ≤ m) : ∃k, m - k = n
|
||||
:=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
|
||||
exists_intro k
|
||||
(calc
|
||||
m - k = n + k - k : {symm Hk}
|
||||
... = n : sub_add_left n k)
|
||||
theorem le_elim_sub (n m : ℕ) (H : n ≤ m) : ∃k, m - k = n :=
|
||||
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
|
||||
exists_intro k
|
||||
(calc
|
||||
m - k = n + k - k : {symm Hk}
|
||||
... = n : sub_add_left n k)
|
||||
|
||||
theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k)
|
||||
:= have l1 : k ≤ m → n + m - k = n + (m - k), from
|
||||
sub_induction k m
|
||||
(take m : ℕ,
|
||||
assume H : 0 ≤ m,
|
||||
calc
|
||||
n + m - 0 = n + m : sub_zero_right (n + m)
|
||||
... = n + (m - 0) : {symm (sub_zero_right m)})
|
||||
(take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k m,
|
||||
assume IH : k ≤ m → n + m - k = n + (m - k),
|
||||
take H : succ k ≤ succ m,
|
||||
calc
|
||||
n + succ m - succ k = succ (n + m) - succ k : {add_succ_right n m}
|
||||
... = n + m - k : sub_succ_succ (n + m) k
|
||||
... = n + (m - k) : IH (succ_le_cancel H)
|
||||
... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}),
|
||||
l1 H
|
||||
theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
|
||||
have l1 : k ≤ m → n + m - k = n + (m - k), from
|
||||
sub_induction k m
|
||||
(take m : ℕ,
|
||||
assume H : 0 ≤ m,
|
||||
calc
|
||||
n + m - 0 = n + m : sub_zero_right (n + m)
|
||||
... = n + (m - 0) : {symm (sub_zero_right m)})
|
||||
(take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
|
||||
(take k m,
|
||||
assume IH : k ≤ m → n + m - k = n + (m - k),
|
||||
take H : succ k ≤ succ m,
|
||||
calc
|
||||
n + succ m - succ k = succ (n + m) - succ k : {add_succ_right n m}
|
||||
... = n + m - k : sub_succ_succ (n + m) k
|
||||
... = n + (m - k) : IH (succ_le_cancel H)
|
||||
... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}),
|
||||
l1 H
|
||||
|
||||
theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m
|
||||
:= sub_split
|
||||
(assume H1 : n ≤ m, assume H2 : 0 = 0, H1)
|
||||
(take k : ℕ,
|
||||
assume H1 : m + k = n,
|
||||
assume H2 : k = 0,
|
||||
have H3 : n = m, from subst (add_zero_right m) (subst H2 (symm H1)),
|
||||
subst H3 (le_refl n))
|
||||
theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m :=
|
||||
sub_split
|
||||
(assume H1 : n ≤ m, assume H2 : 0 = 0, H1)
|
||||
(take k : ℕ,
|
||||
assume H1 : m + k = n,
|
||||
assume H2 : k = 0,
|
||||
have H3 : n = m, from subst (add_zero_right m) (subst H2 (symm H1)),
|
||||
subst H3 (le_refl n))
|
||||
|
||||
theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
|
||||
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n)
|
||||
:= or_elim (le_total n m)
|
||||
(assume H3 : n ≤ m,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹)))
|
||||
(assume H3 : m ≤ n,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹)))
|
||||
(H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
|
||||
or_elim (le_total n m)
|
||||
(assume H3 : n ≤ m,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹)))
|
||||
(assume H3 : m ≤ n,
|
||||
le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹)))
|
||||
|
||||
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m
|
||||
:=
|
||||
have H2 : k - n + n = m + n, from
|
||||
calc
|
||||
k - n + n = k : add_sub_ge_left (le_intro H)
|
||||
... = n + m : symm H
|
||||
... = m + n : add_comm n m,
|
||||
add_cancel_right H2
|
||||
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m :=
|
||||
have H2 : k - n + n = m + n, from
|
||||
calc
|
||||
k - n + n = k : add_sub_ge_left (le_intro H)
|
||||
... = n + m : symm H
|
||||
... = m + n : add_comm n m,
|
||||
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
|
||||
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
|
||||
|
||||
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,
|
||||
or_elim (le_total n k)
|
||||
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le (m - k))
|
||||
(assume H2 : k ≤ n,
|
||||
have H3 : n - k + l = m - k, from
|
||||
calc
|
||||
n - k + l = l + (n - k) : by simp
|
||||
... = l + n - k : symm (add_sub_assoc H2 l)
|
||||
... = n + l - k : {add_comm l n}
|
||||
... = m - k : {Hl},
|
||||
le_intro H3)
|
||||
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,
|
||||
or_elim (le_total n k)
|
||||
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le (m - k))
|
||||
(assume H2 : k ≤ n,
|
||||
have H3 : n - k + l = m - k, from
|
||||
calc
|
||||
n - k + l = l + (n - k) : by simp
|
||||
... = l + n - k : symm (add_sub_assoc H2 l)
|
||||
... = n + l - k : {add_comm l n}
|
||||
... = m - k : {Hl},
|
||||
le_intro H3)
|
||||
|
||||
theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n
|
||||
:=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
sub_split
|
||||
(assume H2 : k ≤ m, zero_le (k - n))
|
||||
(take m' : ℕ,
|
||||
assume Hm : m + m' = k,
|
||||
have H3 : n ≤ k, from le_trans H (le_intro Hm),
|
||||
have H4 : m' + l + n = k - n + n, from
|
||||
calc
|
||||
m' + l + n = n + l + m' : by simp
|
||||
... = m + m' : {Hl}
|
||||
... = k : Hm
|
||||
... = k - n + n : symm (add_sub_ge_left H3),
|
||||
le_intro (add_cancel_right H4))
|
||||
theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n :=
|
||||
obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
|
||||
sub_split
|
||||
(assume H2 : k ≤ m, zero_le (k - n))
|
||||
(take m' : ℕ,
|
||||
assume Hm : m + m' = k,
|
||||
have H3 : n ≤ k, from le_trans H (le_intro Hm),
|
||||
have H4 : m' + l + n = k - n + n, from
|
||||
calc
|
||||
m' + l + n = n + l + m' : by simp
|
||||
... = m + m' : {Hl}
|
||||
... = k : Hm
|
||||
... = k - n + n : symm (add_sub_ge_left H3),
|
||||
le_intro (add_cancel_right H4))
|
||||
|
||||
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m
|
||||
-- :=
|
||||
|
|
@ -375,26 +353,25 @@ theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n
|
|||
-- :=
|
||||
-- _
|
||||
|
||||
theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k)
|
||||
:=
|
||||
sub_split
|
||||
(assume H : n ≤ m, (add_zero_left (m - k))⁻¹ ▸ sub_le_right H k)
|
||||
(take mn : ℕ,
|
||||
assume Hmn : m + mn = n,
|
||||
sub_split
|
||||
(assume H : m ≤ k,
|
||||
have H2 : n - k ≤ n - m, from sub_le_left H n,
|
||||
have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2,
|
||||
show n - k ≤ mn + 0, from (add_zero_right mn)⁻¹ ▸ H3)
|
||||
(take km : ℕ,
|
||||
assume Hkm : k + km = m,
|
||||
have H : k + (mn + km) = n, from
|
||||
calc
|
||||
k + (mn + km) = k + km + mn : by simp
|
||||
... = m + mn : {Hkm}
|
||||
... = n : Hmn,
|
||||
have H2 : n - k = mn + km, from sub_intro H,
|
||||
H2 ▸ (le_refl (n - k))))
|
||||
theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
|
||||
sub_split
|
||||
(assume H : n ≤ m, (add_zero_left (m - k))⁻¹ ▸ sub_le_right H k)
|
||||
(take mn : ℕ,
|
||||
assume Hmn : m + mn = n,
|
||||
sub_split
|
||||
(assume H : m ≤ k,
|
||||
have H2 : n - k ≤ n - m, from sub_le_left H n,
|
||||
have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2,
|
||||
show n - k ≤ mn + 0, from (add_zero_right mn)⁻¹ ▸ H3)
|
||||
(take km : ℕ,
|
||||
assume Hkm : k + km = m,
|
||||
have H : k + (mn + km) = n, from
|
||||
calc
|
||||
k + (mn + km) = k + km + mn : by simp
|
||||
... = m + mn : {Hkm}
|
||||
... = n : Hmn,
|
||||
have H2 : n - k = mn + km, from sub_intro H,
|
||||
H2 ▸ (le_refl (n - k))))
|
||||
|
||||
|
||||
-- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
|
||||
|
|
@ -420,129 +397,116 @@ theorem right_le_max (n m : ℕ) : m ≤ max n m := le_add_sub_right n m
|
|||
|
||||
definition dist (n m : ℕ) := (n - m) + (m - n)
|
||||
|
||||
theorem dist_comm (n m : ℕ) : dist n m = dist m n
|
||||
:= add_comm (n - m) (m - n)
|
||||
theorem dist_comm (n m : ℕ) : dist n m = dist m n :=
|
||||
add_comm (n - m) (m - n)
|
||||
|
||||
theorem dist_self (n : ℕ) : dist n n = 0
|
||||
:=
|
||||
calc
|
||||
(n - n) + (n - n) = 0 + 0 : by simp
|
||||
... = 0 : by simp
|
||||
theorem dist_self (n : ℕ) : dist n n = 0 :=
|
||||
calc
|
||||
(n - n) + (n - n) = 0 + 0 : by simp
|
||||
... = 0 : by simp
|
||||
|
||||
theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m
|
||||
:=
|
||||
have H2 : n - m = 0, from add_eq_zero_left H,
|
||||
have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
|
||||
have H4 : m - n = 0, from add_eq_zero_right H,
|
||||
have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
|
||||
le_antisym H3 H5
|
||||
theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
|
||||
have H2 : n - m = 0, from add_eq_zero_left H,
|
||||
have H3 : n ≤ m, from sub_eq_zero_imp_le H2,
|
||||
have H4 : m - n = 0, from add_eq_zero_right H,
|
||||
have H5 : m ≤ n, from sub_eq_zero_imp_le H4,
|
||||
le_antisym H3 H5
|
||||
|
||||
theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n
|
||||
:=
|
||||
calc
|
||||
dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H}
|
||||
... = m - n : add_zero_left (m - n)
|
||||
theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
|
||||
calc
|
||||
dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H}
|
||||
... = m - n : add_zero_left (m - n)
|
||||
|
||||
theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m
|
||||
:= dist_comm m n ▸ dist_le H
|
||||
theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
|
||||
dist_comm m n ▸ dist_le H
|
||||
|
||||
theorem dist_zero_right (n : ℕ) : dist n 0 = n
|
||||
:= trans (dist_ge (zero_le n)) (sub_zero_right n)
|
||||
theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
|
||||
trans (dist_ge (zero_le n)) (sub_zero_right n)
|
||||
|
||||
theorem dist_zero_left (n : ℕ) : dist 0 n = n
|
||||
:= trans (dist_le (zero_le n)) (sub_zero_right n)
|
||||
theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
|
||||
trans (dist_le (zero_le n)) (sub_zero_right n)
|
||||
|
||||
theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m
|
||||
:=
|
||||
calc
|
||||
dist k n = k - n : dist_ge (le_intro H)
|
||||
... = m : sub_intro H
|
||||
theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
|
||||
calc
|
||||
dist k n = k - n : dist_ge (le_intro H)
|
||||
... = m : sub_intro H
|
||||
|
||||
theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m
|
||||
:=
|
||||
calc
|
||||
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : refl _
|
||||
... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _}
|
||||
... = (n - m) + (m - n) : {sub_add_add_right _ _ _}
|
||||
theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
|
||||
calc
|
||||
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : refl _
|
||||
... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _}
|
||||
... = (n - m) + (m - n) : {sub_add_add_right _ _ _}
|
||||
|
||||
theorem dist_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m :=
|
||||
add_comm m k ▸ add_comm n k ▸ dist_add_right n k m
|
||||
|
||||
-- add_rewrite dist_self dist_add_right dist_add_left dist_zero_left dist_zero_right
|
||||
|
||||
theorem dist_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n
|
||||
:=
|
||||
theorem dist_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n :=
|
||||
calc
|
||||
dist n m + m = n - m + m : {dist_ge H}
|
||||
... = n : add_sub_ge_left H
|
||||
|
||||
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=
|
||||
calc
|
||||
dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k)
|
||||
... = dist (k + l) (k + m) : {H}
|
||||
... = dist l m : dist_add_left k l m
|
||||
|
||||
theorem dist_sub_move_add {n m : ℕ} (H : n ≥ m) (k : ℕ) : dist (n - m) k = dist n (k + m) :=
|
||||
have H2 : n - m + (k + m) = k + n, from
|
||||
calc
|
||||
dist n m + m = n - m + m : {dist_ge H}
|
||||
... = n : add_sub_ge_left H
|
||||
n - m + (k + m) = n - m + m + k : by simp
|
||||
... = n + k : {add_sub_ge_left H}
|
||||
... = k + n : by simp,
|
||||
dist_eq_intro H2
|
||||
|
||||
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m
|
||||
:=
|
||||
calc
|
||||
dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k)
|
||||
... = dist (k + l) (k + m) : {H}
|
||||
... = dist l m : dist_add_left k l m
|
||||
|
||||
theorem dist_sub_move_add {n m : ℕ} (H : n ≥ m) (k : ℕ) : dist (n - m) k = dist n (k + m)
|
||||
:=
|
||||
have H2 : n - m + (k + m) = k + n, from
|
||||
calc
|
||||
n - m + (k + m) = n - m + m + k : by simp
|
||||
... = n + k : {add_sub_ge_left H}
|
||||
... = k + n : by simp,
|
||||
dist_eq_intro H2
|
||||
|
||||
theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k
|
||||
:= subst (subst (dist_sub_move_add H n) (dist_comm (k - m) n)) (dist_comm k (n + m))
|
||||
theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k :=
|
||||
subst (subst (dist_sub_move_add H n) (dist_comm (k - m) n)) (dist_comm k (n + m))
|
||||
|
||||
--triangle inequality formulated with dist
|
||||
theorem triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k
|
||||
:=
|
||||
have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
|
||||
by simp,
|
||||
H ▸ add_le (sub_triangle_inequality n m k) (sub_triangle_inequality k m n)
|
||||
theorem triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
|
||||
have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
|
||||
by simp,
|
||||
H ▸ add_le (sub_triangle_inequality n m k) (sub_triangle_inequality k m n)
|
||||
|
||||
theorem dist_add_le_add_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l
|
||||
:=
|
||||
have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
|
||||
calc
|
||||
_ = dist n k + dist (k + m) (k + l) : {dist_add_right n m k}
|
||||
... = _ : {dist_add_left k m l},
|
||||
H ▸ (triangle_inequality (n + m) (k + m) (k + l))
|
||||
theorem dist_add_le_add_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
|
||||
have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
|
||||
calc
|
||||
_ = dist n k + dist (k + m) (k + l) : {dist_add_right n m k}
|
||||
... = _ : {dist_add_left k m l},
|
||||
H ▸ (triangle_inequality (n + m) (k + m) (k + l))
|
||||
|
||||
--interaction with multiplication
|
||||
|
||||
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m
|
||||
:=
|
||||
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
|
||||
by simp
|
||||
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
|
||||
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
|
||||
by simp
|
||||
|
||||
theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k
|
||||
:=
|
||||
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
|
||||
by simp
|
||||
theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
|
||||
have H : ∀n m, dist n m = n - m + (m - n), from take n m, refl _,
|
||||
by simp
|
||||
|
||||
-- add_rewrite dist_mul_right dist_mul_left dist_comm
|
||||
|
||||
--needed to prove |a| * |b| = |a * b| in int
|
||||
theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k)
|
||||
:=
|
||||
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
|
||||
take k l : ℕ,
|
||||
assume H : k ≥ l,
|
||||
have H2 : m * k ≥ m * l, from mul_le_left H m,
|
||||
have H3 : n * l + m * k ≥ m * l, from le_trans H2 (le_add_left _ _),
|
||||
calc
|
||||
dist n m * dist k l = dist n m * (k - l) : {dist_ge H}
|
||||
... = dist (n * (k - l)) (m * (k - l)) : symm (dist_mul_right n (k - l) m)
|
||||
... = dist (n * k - n * l) (m * k - m * l) : by simp
|
||||
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_move_add (mul_le_left H n) _
|
||||
... = dist (n * k) (n * l + (m * k - m * l)) : {add_comm _ _}
|
||||
... = dist (n * k) (n * l + m * k - m * l) : {symm (add_sub_assoc H2 (n * l))}
|
||||
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _,
|
||||
or_elim (le_total k l)
|
||||
(assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
|
||||
(assume H : l ≤ k, aux k l H)
|
||||
theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
|
||||
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
|
||||
take k l : ℕ,
|
||||
assume H : k ≥ l,
|
||||
have H2 : m * k ≥ m * l, from mul_le_left H m,
|
||||
have H3 : n * l + m * k ≥ m * l, from le_trans H2 (le_add_left _ _),
|
||||
calc
|
||||
dist n m * dist k l = dist n m * (k - l) : {dist_ge H}
|
||||
... = dist (n * (k - l)) (m * (k - l)) : symm (dist_mul_right n (k - l) m)
|
||||
... = dist (n * k - n * l) (m * k - m * l) : by simp
|
||||
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_move_add (mul_le_left H n) _
|
||||
... = dist (n * k) (n * l + (m * k - m * l)) : {add_comm _ _}
|
||||
... = dist (n * k) (n * l + m * k - m * l) : {symm (add_sub_assoc H2 (n * l))}
|
||||
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _,
|
||||
or_elim (le_total k l)
|
||||
(assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
|
||||
(assume H : l ≤ k, aux k l H)
|
||||
|
||||
opaque_hint (hiding dist)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue