lean2/library/standard/data/nat/sub.lean

513 lines
17 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

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

--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
import data.nat.order
import tools.fake_simplifier
using nat eq_ops tactic
using helper_tactics
using fake_simplifier
namespace nat
-- data.nat.basic2
-- ===============
--
-- More basic operations on the natural numbers.
-- subtraction
-- -----------
definition sub (n m : ) : nat := nat_rec n (fun m x, pred x) m
infixl `-` : 65 := sub
theorem sub_zero_right (n : ) : n - 0 = n
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_succ_left (n m : ) : pred (succ n - m) = n - m
-- :=
-- induction_on m
-- (calc
-- pred (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 : pred (succ n - k) = n - k,
-- _)
--)
--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_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_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)
-- 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_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 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_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)
-- 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_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_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 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_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_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_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))
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 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_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⁻¹)))
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_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_lt_cancel_right {n m k : ) (H : n - k < m - k) : n < m
-- :=
-- _
-- theorem sub_lt_cancel_left {n m k : ) (H : n - m < n - k) : k < m
-- :=
-- _
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
-- Max, min, iteration, and absolute difference
-- --------------------------------------------
definition max (n m : ) : := n + (m - n)
definition min (n m : ) : := m - (m - n)
theorem max_le {n m : } (H : n ≤ m) : n + (m - n) = m := add_sub_le H
theorem max_ge {n m : } (H : n ≥ m) : n + (m - n) = n := add_sub_ge H
theorem left_le_max (n m : ) : n ≤ n + (m - n) := le_add_sub_left n m
theorem right_le_max (n m : ) : m ≤ max n m := le_add_sub_right n m
-- ### absolute difference
-- This section is still incomplete
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_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_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_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_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_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 :=
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
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))
--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 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_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)
end nat