lean2/library/data/nat/sub.lean
Leonardo de Moura d536475e49 refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 11:10:04 -07:00

496 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
-- data.nat.sub
-- ============
--
-- Subtraction on the natural numbers, as well as min, max, and distance.
import data.nat.order
import tools.fake_simplifier
using nat eq_ops tactic
using helper_tactics
using fake_simplifier
namespace nat
-- subtraction
-- -----------
definition sub (n m : ) : nat := nat_rec n (fun m x, pred x) m
infixl `-` := 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
(take k : nat,
assume IH : 0 - k = 0,
calc
0 - succ k = pred (0 - k) : sub_succ_right
... = pred 0 : {IH}
... = 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⁻¹)
theorem sub_self {n : } : n - n = 0 :=
induction_on n sub_zero_right (take k IH, trans sub_succ_succ 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 ▸ add_comm ▸ sub_add_add_right
theorem sub_add_left {n m : } : n + m - m = n :=
induction_on m
(add_zero_right⁻¹ ▸ sub_zero_right)
(take k : ,
assume IH : n + k - k = n,
calc
n + succ k - succ k = succ (n + k) - succ k : {add_succ_right}
... = n + k - k : sub_succ_succ
... = n : IH)
-- TODO: add_sub_inv'
theorem sub_add_left2 {n m : } : n + m - n = m :=
add_comm ▸ sub_add_left
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) : {add_zero_right⁻¹})
(take l : nat,
assume IH : n - m - l = n - (m + l),
calc
n - m - succ l = pred (n - m - l) : sub_succ_right
... = pred (n - (m + l)) : {IH}
... = n - succ (m + l) : sub_succ_right⁻¹
... = n - (m + succ l) : {add_succ_right⁻¹})
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}
... = n - (m + k) : sub_succ_succ
... = n - m - k : sub_sub⁻¹
theorem sub_add_right_eq_zero {n m : } : n - (n + m) = 0 :=
calc
n - (n + m) = n - n - m : sub_sub⁻¹
... = 0 - m : {sub_self}
... = 0 : sub_zero_left
theorem sub_comm {m n k : } : m - n - k = m - k - n :=
calc
m - n - k = m - (n + k) : sub_sub
... = m - (k + n) : {add_comm}
... = m - k - n : sub_sub⁻¹
theorem sub_one {n : } : n - 1 = pred n :=
calc
n - 1 = pred (n - 0) : sub_succ_right
... = pred n : {sub_zero_right}
theorem succ_sub_one {n : } : succ n - 1 = n :=
sub_succ_succ ⬝ sub_zero_right
-- 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 : sub_zero_left⁻¹
... = 0 * m - m : {mul_zero_left⁻¹})
(take k : nat,
assume IH : pred k * m = k * m - m,
calc
pred (succ k) * m = k * m : {pred_succ}
... = k * m + m - m : sub_add_left⁻¹
... = succ k * m - m : {mul_succ_left⁻¹})
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
... = n * m - n : {mul_comm}
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 * k - 0 : sub_zero_right⁻¹
... = n * k - 0 * k : {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) * k - k : mul_pred_left
... = n * k - l * k - k : {IH}
... = n * k - (l * k + k) : sub_sub
... = n * k - (succ l * k) : {mul_succ_left⁻¹})
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 - 0) : {sub_zero_right⁻¹})
(take k,
assume H : succ k ≤ 0,
absurd H not_succ_zero_le)
(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) : IH (succ_le_cancel H)
... = succ (succ l - succ k) : {sub_succ_succ⁻¹})
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
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 : sub_zero_right)
(take k, assume H : succ k ≤ 0, absurd H not_succ_zero_le)
(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}
... = succ (k + (l - k)) : add_succ_left
... = succ l : {IH (succ_le_cancel H)})
theorem add_sub_ge_left {n m : } : n ≥ m → n - m + m = n :=
add_comm ▸ 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
theorem add_sub_le_left {n m : } : n ≤ m → n - m + m = m :=
add_comm ▸ add_sub_ge
theorem le_add_sub_left {n m : } : n ≤ n + (m - n) :=
or_elim le_total
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
(assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl)
theorem le_add_sub_right {n m : } : m ≤ n + (m - n) :=
or_elim le_total
(assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ le_refl)
(assume H : m ≤ n, (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
(assume H3 : n ≤ m, (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)
(take k : , assume H : m + k = n, le_intro (add_comm ▸ 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 : {Hk⁻¹}
... = n : sub_add_left)
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 - 0) : {sub_zero_right⁻¹})
(take k : , assume H : succ k ≤ 0, absurd H not_succ_zero_le)
(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 - k : sub_succ_succ
... = n + (m - k) : IH (succ_le_cancel H)
... = n + (succ m - succ k) : {sub_succ_succ⁻¹}),
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 add_zero_right ▸ H2 ▸ H1⁻¹,
subst H3 le_refl)
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
(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 : H⁻¹
... = m + n : add_comm,
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
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le)
(assume H2 : k ≤ n,
have H3 : n - k + l = m - k, from
calc
n - k + l = l + (n - k) : by simp
... = l + n - k : (add_sub_assoc H2 l)⁻¹
... = n + l - k : {add_comm}
... = 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)
(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 : (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⁻¹ ▸ 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⁻¹ ▸ 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))
-- 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
theorem right_le_max {n m : } : m ≤ max n m := le_add_sub_right
-- ### 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
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
theorem dist_ge {n m : } (H : n ≥ m) : dist n m = n - m :=
dist_comm ▸ dist_le H
theorem dist_zero_right {n : } : dist n 0 = n :=
dist_ge zero_le ⬝ sub_zero_right
theorem dist_zero_left {n : } : dist 0 n = n :=
dist_le zero_le ⬝ sub_zero_right
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)) : rfl
... = (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 ▸ add_comm ▸ dist_add_right
-- 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) : dist_add_right⁻¹
... = dist (k + l) (k + m) : {H}
... = dist l m : dist_add_left
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 :=
(dist_sub_move_add H n ▸ dist_comm) ▸ dist_comm
--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 sub_triangle_inequality
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
dist_add_left ▸ dist_add_right ▸ rfl,
H ▸ triangle_inequality
--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, rfl,
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, rfl,
by simp
-- add_rewrite dist_mul_right dist_mul_left dist_comm
--needed to prove of_nat a * of_nat b = of_nat (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)) : dist_mul_right⁻¹
... = 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) : {(add_sub_assoc H2 (n * l))⁻¹}
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _,
or_elim le_total
(assume H : k ≤ l, dist_comm ▸ dist_comm ▸ aux l k H)
(assume H : l ≤ k, aux k l H)
end nat