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

refactor(library/data/int/sub): rename theorems, add theorems, clean up

Browse source
This commit is contained in:
Jeremy Avigad 2015-01-12 16:28:42 -05:00
parent 4f519be55e
commit 0dcf06000b
5 changed files with 213 additions and 238 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/algebra/group.lean
View file

@ -45,7 +45,6 @@ prefix `-` := has_neg.neg
notation 1 := !has_one.one notation 1 := !has_one.one
notation 0 := !has_zero.zero notation 0 := !has_zero.zero
/- semigroup -/ /- semigroup -/
structure semigroup [class] (A : Type) extends has_mul A := structure semigroup [class] (A : Type) extends has_mul A :=
@ -80,7 +79,6 @@ theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
a * b = c * b → a = c := a * b = c * b → a = c :=
!right_cancel_semigroup.mul_right_cancel !right_cancel_semigroup.mul_right_cancel
/- additive semigroup -/ /- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A := structure add_semigroup [class] (A : Type) extends has_add A :=
@ -127,7 +125,6 @@ theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
/- additive monoid -/ /- additive monoid -/
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A := structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
@ -139,7 +136,6 @@ theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
/- group -/ /- group -/
structure group [class] (A : Type) extends monoid A, has_inv A := structure group [class] (A : Type) extends monoid A, has_inv A :=
@ -277,7 +273,6 @@ end group
structure comm_group [class] (A : Type) extends group A, comm_monoid A structure comm_group [class] (A : Type) extends group A, comm_monoid A
/- additive group -/ /- additive group -/
structure add_group [class] (A : Type) extends add_monoid A, has_neg A := structure add_group [class] (A : Type) extends add_monoid A, has_neg A :=
@ -489,7 +484,6 @@ include s
end add_comm_group end add_comm_group
/- bundled structures -/ /- bundled structures -/
structure Semigroup := structure Semigroup :=

29
library/data/int/basic.lean
View file

@ -122,7 +122,7 @@ theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl
theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m := rfl theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m := rfl
theorem sub_nat_nat_of_ge {m n : ℕ} (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) := theorem sub_nat_nat_of_ge {m n : ℕ} (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) :=
have H1 : n - m = 0, from le_imp_sub_eq_zero H, have H1 : n - m = 0, from sub_eq_zero_of_le H,
calc calc
sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl
... = of_nat (m - n) : rfl ... = of_nat (m - n) : rfl
@ -131,7 +131,7 @@ context
reducible sub_nat_nat reducible sub_nat_nat
theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) : theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) :
sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) := sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) :=
have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_gt H))⁻¹, have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹,
calc calc
sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (of_nat (m - n)) sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (of_nat (m - n))
(take k, neg_succ_of_nat k) : H1 ▸ rfl (take k, neg_succ_of_nat k) : H1 ▸ rfl
@ -218,15 +218,15 @@ or.elim (@le_or_gt n m)
have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl, have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl,
H1⁻¹ ▸ H1⁻¹ ▸
(calc (calc
m - n + n = m : add_sub_ge_left H m - n + n = m : sub_add_cancel H
... = 0 + m : zero_add)) ... = 0 + m : zero_add))
(take H : m < n, (take H : m < n,
have H1 : repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl, have H1 : repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl,
H1⁻¹ ▸ H1⁻¹ ▸
(calc (calc
0 + n = n : zero_add 0 + n = n : zero_add
... = n - m + m : add_sub_ge_left (le_of_lt H) ... = n - m + m : sub_add_cancel (le_of_lt H)
... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_gt H))⁻¹)) ... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_lt H))⁻¹))
theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p := theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p :=
!prod.eta ▸ !repr_sub_nat_nat !prod.eta ▸ !repr_sub_nat_nat
@ -238,28 +238,28 @@ or.elim (equiv_cases Hequiv)
have H4 : pr1 q ≥ pr2 q, from and.elim_right H2, have H4 : pr1 q ≥ pr2 q, from and.elim_right H2,
have H5 : pr1 p = pr1 q - pr2 q + pr2 p, from have H5 : pr1 p = pr1 q - pr2 q + pr2 p, from
calc calc
pr1 p = pr1 p + pr2 q - pr2 q : sub_add_left pr1 p = pr1 p + pr2 q - pr2 q : add_sub_cancel
... = pr2 p + pr1 q - pr2 q : Hequiv ... = pr2 p + pr1 q - pr2 q : Hequiv
... = pr2 p + (pr1 q - pr2 q) : add_sub_assoc H4 ... = pr2 p + (pr1 q - pr2 q) : add_sub_assoc H4
... = pr1 q - pr2 q + pr2 p : add.comm, ... = pr1 q - pr2 q + pr2 p : add.comm,
have H6 : pr1 p - pr2 p = pr1 q - pr2 q, from have H6 : pr1 p - pr2 p = pr1 q - pr2 q, from
calc calc
pr1 p - pr2 p = pr1 q - pr2 q + pr2 p - pr2 p : H5 pr1 p - pr2 p = pr1 q - pr2 q + pr2 p - pr2 p : H5
... = pr1 q - pr2 q : sub_add_left, ... = pr1 q - pr2 q : add_sub_cancel,
abstr_of_ge H3 ⬝ congr_arg of_nat H6 ⬝ (abstr_of_ge H4)⁻¹) abstr_of_ge H3 ⬝ congr_arg of_nat H6 ⬝ (abstr_of_ge H4)⁻¹)
(assume H2, (assume H2,
have H3 : pr1 p < pr2 p, from and.elim_left H2, have H3 : pr1 p < pr2 p, from and.elim_left H2,
have H4 : pr1 q < pr2 q, from and.elim_right H2, have H4 : pr1 q < pr2 q, from and.elim_right H2,
have H5 : pr2 p = pr2 q - pr1 q + pr1 p, from have H5 : pr2 p = pr2 q - pr1 q + pr1 p, from
calc calc
pr2 p = pr2 p + pr1 q - pr1 q : sub_add_left pr2 p = pr2 p + pr1 q - pr1 q : add_sub_cancel
... = pr1 p + pr2 q - pr1 q : Hequiv ... = pr1 p + pr2 q - pr1 q : Hequiv
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le_of_lt H4) ... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le_of_lt H4)
... = pr2 q - pr1 q + pr1 p : add.comm, ... = pr2 q - pr1 q + pr1 p : add.comm,
have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from
calc calc
pr2 p - pr1 p = pr2 q - pr1 q + pr1 p - pr1 p : H5 pr2 p - pr1 p = pr2 q - pr1 q + pr1 p - pr1 p : H5
... = pr2 q - pr1 q : sub_add_left, ... = pr2 q - pr1 q : add_sub_cancel,
abstr_of_lt H3 ⬝ congr_arg neg_succ_of_nat (congr_arg pred H6)⬝ (abstr_of_lt H4)⁻¹) abstr_of_lt H3 ⬝ congr_arg neg_succ_of_nat (congr_arg pred H6)⬝ (abstr_of_lt H4)⁻¹)
theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) := theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ ((p ≡ p) ∧ (q ≡ q) ∧ (abstr p = abstr q)) :=
@ -289,13 +289,13 @@ or.elim (@le_or_gt n m)
(assume H : m ≥ n, (assume H : m ≥ n,
calc calc
nat_abs (abstr (m, n)) = nat_abs (of_nat (m - n)) : int.abstr_of_ge H nat_abs (abstr (m, n)) = nat_abs (of_nat (m - n)) : int.abstr_of_ge H
... = dist m n : dist_ge H) ... = dist m n : dist_eq_sub_of_ge H)
(assume H : m < n, (assume H : m < n,
calc calc
nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H
... = succ (pred (n - m)) : rfl ... = succ (pred (n - m)) : rfl
... = n - m : succ_pred_of_pos (sub_pos_of_gt H) ... = n - m : succ_pred_of_pos (sub_pos_of_lt H)
... = dist m n : dist_le (le_of_lt H)) ... = dist m n : dist_eq_sub_of_le (le_of_lt H))
end end
theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) := theorem cases_of_nat (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat n) :=
@ -418,7 +418,7 @@ calc
nat_abs (-a) = nat_abs (abstr (repr (-a))) : abstr_repr nat_abs (-a) = nat_abs (abstr (repr (-a))) : abstr_repr
... = nat_abs (abstr (pneg (repr a))) : repr_neg ... = nat_abs (abstr (pneg (repr a))) : repr_neg
... = dist (pr1 (pneg (repr a))) (pr2 (pneg (repr a))) : nat_abs_abstr ... = dist (pr1 (pneg (repr a))) (pr2 (pneg (repr a))) : nat_abs_abstr
... = dist (pr2 (pneg (repr a))) (pr1 (pneg (repr a))) : dist_comm ... = dist (pr2 (pneg (repr a))) (pr1 (pneg (repr a))) : dist.comm
... = nat_abs (abstr (repr a)) : nat_abs_abstr ... = nat_abs (abstr (repr a)) : nat_abs_abstr
... = nat_abs a : abstr_repr ... = nat_abs a : abstr_repr
@ -458,7 +458,8 @@ have H : nat_abs (a + b) = pabs (padd (repr a) (repr b)), from
... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add, ... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add,
have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr, have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr,
have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr, have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr,
have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b), from !dist_add_le_add_dist, have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b),
from !dist_add_add_le_add_dist_dist,
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3 H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
context context

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

@ -1,4 +1,4 @@
/- /-
Copyright (c) 2014 Jeremy Avigad. All rights reserved. Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
@ -46,10 +46,10 @@ theorem div_rec {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) : a div b = succ ((a
divide_def a b ⬝ if_pos (and.intro h₁ h₂) divide_def a b ⬝ if_pos (and.intro h₁ h₂)
theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
calc (x + z) div z calc
= if 0 < z ∧ z ≤ x + z then divide (x + z - z) z + 1 else 0 : !divide_def (x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def
... = divide (x + z - z) z + 1 : if_pos (and.intro H (le_add_left z x)) ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x))
... = succ (x div z) : sub_add_left ... = succ (x div z) : add_sub_cancel
theorem div_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y := theorem div_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) div z = x div z + y :=
induction_on y induction_on y
@ -89,7 +89,7 @@ theorem mod_add_self_right {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z :=
calc (x + z) mod z calc (x + z) mod z
= if 0 < z ∧ z ≤ x + z then (x + z - z) mod z else _ : modulo_def = if 0 < z ∧ z ≤ x + z then (x + z - z) mod z else _ : modulo_def
... = (x + z - z) mod z : if_pos (and.intro H (le_add_left z x)) ... = (x + z - z) mod z : if_pos (and.intro H (le_add_left z x))
... = x mod z : sub_add_left ... = x mod z : add_sub_cancel
theorem mod_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z := theorem mod_add_mul_self_right {x y z : ℕ} (H : z > 0) : (x + y * z) mod z = x mod z :=
induction_on y induction_on y
@ -167,7 +167,7 @@ by_cases_zero_pos y
... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4 ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4
... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm
... = succ x - y + y : {!(IH _ H6)⁻¹} ... = succ x - y + y : {!(IH _ H6)⁻¹}
... = succ x : add_sub_ge_left H2)⁻¹))) ... = succ x : sub_add_cancel H2)⁻¹)))
theorem mod_le {x y : ℕ} : x mod y ≤ x := theorem mod_le {x y : ℕ} : x mod y ≤ x :=
div_mod_eq⁻¹ ▸ !le_add_left div_mod_eq⁻¹ ▸ !le_add_left
@ -272,9 +272,9 @@ have H1 : z * y = x mod y + x div y * y, from
H ⬝ div_mod_eq ⬝ !add.comm, H ⬝ div_mod_eq ⬝ !add.comm,
have H2 : (z - x div y) * y = x mod y, from have H2 : (z - x div y) * y = x mod y, from
calc calc
(z - x div y) * y = z * y - x div y * y : mul_sub_distr_right (z - x div y) * y = z * y - x div y * y : mul_sub_right_distrib
... = x mod y + x div y * y - x div y * y : H1 ... = x mod y + x div y * y - x div y * y : H1
... = x mod y : sub_add_left, ... = x mod y : add_sub_cancel,
show x mod y = 0, from show x mod y = 0, from
by_cases by_cases
(assume yz : y = 0, (assume yz : y = 0,
@ -348,10 +348,10 @@ dvd_of_dvd_add_left (!add.comm ▸ H)
theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) := theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
by_cases by_cases
(assume H3 : n1 ≥ n2, (assume H3 : n1 ≥ n2,
have H4 : n1 = n1 - n2 + n2, from (add_sub_ge_left H3)⁻¹, have H4 : n1 = n1 - n2 + n2, from (sub_add_cancel H3)⁻¹,
show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2) show m | n1 - n2, from dvd_add_cancel_right (H4 ▸ H1) H2)
(assume H3 : ¬ (n1 ≥ n2), (assume H3 : ¬ (n1 ≥ n2),
have H4 : n1 - n2 = 0, from le_imp_sub_eq_zero (le_of_lt (lt_of_not_le H3)), have H4 : n1 - n2 = 0, from sub_eq_zero_of_le (le_of_lt (lt_of_not_le H3)),
show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _) show m | n1 - n2, from H4⁻¹ ▸ dvd_zero _)
-- Gcd and lcm -- Gcd and lcm

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

@ -308,6 +308,11 @@ nat.cases_on n
assume H : succ n' ≤ m, assume H : succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred H) !pred_succ⁻¹ ▸ succ_le_of_le_pred H)
theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
lt_of_not_le
(take H1 : m ≤ n,
not_lt_of_le (pred_le_pred_of_le H1) H)
theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m := theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m :=
or_of_or_of_imp_left (succ_le_or_eq_of_le H) or_of_or_of_imp_left (succ_le_or_eq_of_le H)
(take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2) (take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2)

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

@ -1,11 +1,12 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved. /-
--- Released under Apache 2.0 license as described in the file LICENSE. Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Author: Floris van Doorn Released under Apache 2.0 license as described in the file LICENSE.
-- data.nat.sub Authors: Floris van Doorn, Jeremy Avigad
-- ============ Module: data.nat.sub
--
-- Subtraction on the natural numbers, as well as min, max, and distance. Subtraction on the natural numbers, as well as min, max, and distance.
-/
import .order import .order
import tools.fake_simplifier import tools.fake_simplifier
@ -15,33 +16,30 @@ open fake_simplifier
namespace nat namespace nat
-- subtraction /- subtraction -/
-- -----------
theorem sub_zero_right (n : ℕ) : n - 0 = n := theorem sub_zero (n : ℕ) : n - 0 = n :=
rfl rfl
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) := theorem sub_succ (n m : ℕ) : n - succ m = pred (n - m) :=
rfl rfl
irreducible sub theorem zero_sub (n : ℕ) : 0 - n = 0 :=
induction_on n !sub_zero
theorem sub_zero_left (n : ℕ) : 0 - n = 0 :=
induction_on n !sub_zero_right
(take k : nat, (take k : nat,
assume IH : 0 - k = 0, assume IH : 0 - k = 0,
calc calc
0 - succ k = pred (0 - k) : !sub_succ_right 0 - succ k = pred (0 - k) : sub_succ
... = pred 0 : {IH} ... = pred 0 : IH
... = 0 : pred_zero) ... = 0 : pred_zero)
theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m := theorem succ_sub_succ (n m : ℕ) : succ n - succ m = n - m :=
succ_sub_succ_eq_sub n m succ_sub_succ_eq_sub n m
theorem sub_self (n : ℕ) : n - n = 0 := theorem sub_self (n : ℕ) : n - n = 0 :=
induction_on n !sub_zero_right (take k IH, !sub_succ_succ ⬝ IH) induction_on n !sub_zero (take k IH, !succ_sub_succ ⬝ IH)
theorem sub_add_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m := theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
induction_on k induction_on k
(calc (calc
(n + 0) - (m + 0) = n - (m + 0) : {!add_zero} (n + 0) - (m + 0) = n - (m + 0) : {!add_zero}
@ -51,183 +49,165 @@ induction_on k
calc calc
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ} (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ}
... = succ (n + l) - succ (m + l) : {!add_succ} ... = succ (n + l) - succ (m + l) : {!add_succ}
... = (n + l) - (m + l) : !sub_succ_succ ... = (n + l) - (m + l) : !succ_sub_succ
... = n - m : IH) ... = n - m : IH)
theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
!add.comm ▸ !add.comm ▸ !sub_add_add_right !add.comm ▸ !add.comm ▸ !add_sub_add_right
theorem sub_add_left (n m : ℕ) : n + m - m = n := theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
induction_on m induction_on m
(!add_zero⁻¹ ▸ !sub_zero_right) (!add_zero⁻¹ ▸ !sub_zero)
(take k : ℕ, (take k : ℕ,
assume IH : n + k - k = n, assume IH : n + k - k = n,
calc calc
n + succ k - succ k = succ (n + k) - succ k : {!add_succ} n + succ k - succ k = succ (n + k) - succ k : add_succ
... = n + k - k : !sub_succ_succ ... = n + k - k : succ_sub_succ
... = n : IH) ... = n : IH)
-- TODO: add_sub_inv' theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m :=
theorem sub_add_left2 (n m : ℕ) : n + m - n = m := !add.comm ▸ !add_sub_cancel
!add.comm ▸ !sub_add_left
theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) := theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
induction_on k induction_on k
(calc (calc
n - m - 0 = n - m : !sub_zero_right n - m - 0 = n - m : sub_zero
... = n - (m + 0) : {!add_zero⁻¹}) ... = n - (m + 0) : add_zero)
(take l : nat, (take l : nat,
assume IH : n - m - l = n - (m + l), assume IH : n - m - l = n - (m + l),
calc calc
n - m - succ l = pred (n - m - l) : !sub_succ_right n - m - succ l = pred (n - m - l) : !sub_succ
... = pred (n - (m + l)) : {IH} ... = pred (n - (m + l)) : IH
... = n - succ (m + l) : !sub_succ_right⁻¹ ... = n - succ (m + l) : sub_succ
... = n - (m + succ l) : {!add_succ⁻¹}) ... = n - (m + succ l) : {!add_succ⁻¹})
theorem succ_sub_sub (n m k : ℕ) : succ n - m - succ k = n - m - k := theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
calc calc
succ n - m - succ k = succ n - (m + succ k) : !sub_sub succ n - m - succ k = succ n - (m + succ k) : sub_sub
... = succ n - succ (m + k) : {!add_succ} ... = succ n - succ (m + k) : add_succ
... = n - (m + k) : !sub_succ_succ ... = n - (m + k) : succ_sub_succ
... = n - m - k : !sub_sub⁻¹ ... = n - m - k : sub_sub
theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0 := theorem sub_self_add (n m : ℕ) : n - (n + m) = 0 :=
calc calc
n - (n + m) = n - n - m : !sub_sub⁻¹ n - (n + m) = n - n - m : sub_sub
... = 0 - m : {!sub_self} ... = 0 - m : sub_self
... = 0 : !sub_zero_left ... = 0 : zero_sub
theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n := theorem sub.right_comm (m n k : ℕ) : m - n - k = m - k - n :=
calc calc
m - n - k = m - (n + k) : !sub_sub m - n - k = m - (n + k) : !sub_sub
... = m - (k + n) : {!add.comm} ... = m - (k + n) : {!add.comm}
... = m - k - n : !sub_sub⁻¹ ... = m - k - n : !sub_sub⁻¹
theorem sub_one (n : ℕ) : n - 1 = pred n := theorem sub_one (n : ℕ) : n - 1 = pred n :=
calc rfl
n - 1 = pred (n - 0) : !sub_succ_right
... = pred n : {!sub_zero_right}
theorem succ_sub_one (n : ℕ) : succ n - 1 = n := theorem succ_sub_one (n : ℕ) : succ n - 1 = n :=
!sub_succ_succ ⬝ !sub_zero_right rfl
-- add_rewrite sub_add_left /- interaction with multiplication -/
-- ### interaction with multiplication
theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m := theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
induction_on n induction_on n
(calc (calc
pred 0 * m = 0 * m : {pred_zero} pred 0 * m = 0 * m : pred_zero
... = 0 : !zero_mul ... = 0 : zero_mul
... = 0 - m : !sub_zero_left⁻¹ ... = 0 - m : zero_sub
... = 0 * m - m : {!zero_mul⁻¹}) ... = 0 * m - m : zero_mul)
(take k : nat, (take k : nat,
assume IH : pred k * m = k * m - m, assume IH : pred k * m = k * m - m,
calc calc
pred (succ k) * m = k * m : {!pred_succ} pred (succ k) * m = k * m : pred_succ
... = k * m + m - m : !sub_add_left⁻¹ ... = k * m + m - m : add_sub_cancel
... = succ k * m - m : {!succ_mul⁻¹}) ... = succ k * m - m : succ_mul)
theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n := theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
calc n * pred m = pred m * n : !mul.comm calc
... = m * n - n : !mul_pred_left n * pred m = pred m * n : mul.comm
... = n * 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 := theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k :=
induction_on m induction_on m
(calc (calc
(n - 0) * k = n * k : {!sub_zero_right} (n - 0) * k = n * k : sub_zero
... = n * k - 0 : !sub_zero_right⁻¹ ... = n * k - 0 : sub_zero
... = n * k - 0 * k : {!zero_mul⁻¹}) ... = n * k - 0 * k : zero_mul)
(take l : nat, (take l : nat,
assume IH : (n - l) * k = n * k - l * k, assume IH : (n - l) * k = n * k - l * k,
calc calc
(n - succ l) * k = pred (n - l) * k : {!sub_succ_right} (n - succ l) * k = pred (n - l) * k : sub_succ
... = (n - l) * k - k : !mul_pred_left ... = (n - l) * k - k : mul_pred_left
... = n * k - l * k - k : {IH} ... = n * k - l * k - k : IH
... = n * k - (l * k + k) : !sub_sub ... = n * k - (l * k + k) : sub_sub
... = n * k - (succ l * k) : {!succ_mul⁻¹}) ... = n * k - (succ l * k) : succ_mul)
theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k := theorem mul_sub_distr_left (n m k : ℕ) : n * (m - k) = n * m - n * k :=
calc calc
n * (m - k) = (m - k) * n : !mul.comm n * (m - k) = (m - k) * n : !mul.comm
... = m * n - k * n : !mul_sub_distr_right ... = m * n - k * n : !mul_sub_right_distrib
... = n * m - k * n : {!mul.comm} ... = n * m - k * n : {!mul.comm}
... = n * m - n * k : {!mul.comm} ... = n * m - n * k : {!mul.comm}
-- ### interaction with inequalities /- interaction with inequalities -/
theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) := theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) :=
sub_induction n m sub_induction n m
(take k, (take k, assume H : 0 ≤ k, rfl)
assume H : 0 ≤ k, (take k,
calc
succ k - 0 = succ k : !sub_zero_right
... = succ (k - 0) : {!sub_zero_right⁻¹})
(take k,
assume H : succ k ≤ 0, assume H : succ k ≤ 0,
absurd H !not_succ_le_zero) absurd H !not_succ_le_zero)
(take k l, (take k l,
assume IH : k ≤ l → succ l - k = succ (l - k), assume IH : k ≤ l → succ l - k = succ (l - k),
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
calc calc
succ (succ l) - succ k = succ l - k : !sub_succ_succ succ (succ l) - succ k = succ l - k : succ_sub_succ
... = succ (l - k) : IH (le_of_succ_le_succ H) ... = succ (l - k) : IH (le_of_succ_le_succ H)
... = succ (succ l - succ k) : {!sub_succ_succ⁻¹}) ... = succ (succ l - succ k) : succ_sub_succ)
theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0 := theorem sub_eq_zero_of_le {n m : ℕ} (H : n ≤ m) : n - m = 0 :=
obtain (k : ℕ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_add_right_eq_zero obtain (k : ℕ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_self_add
theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m := theorem add_sub_of_le {n m : ℕ} : n ≤ m → n + (m - n) = m :=
sub_induction n m sub_induction n m
(take k, (take k,
assume H : 0 ≤ k, assume H : 0 ≤ k,
calc calc
0 + (k - 0) = k - 0 : !zero_add 0 + (k - 0) = k - 0 : zero_add
... = k : !sub_zero_right) ... = k : sub_zero)
(take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
(take k l, (take k l,
assume IH : k ≤ l → k + (l - k) = l, assume IH : k ≤ l → k + (l - k) = l,
take H : succ k ≤ succ l, take H : succ k ≤ succ l,
calc calc
succ k + (succ l - succ k) = succ k + (l - k) : {!sub_succ_succ} succ k + (succ l - succ k) = succ k + (l - k) : succ_sub_succ
... = succ (k + (l - k)) : !add.succ_left ... = succ (k + (l - k)) : add.succ_left
... = succ l : {IH (le_of_succ_le_succ H)}) ... = succ l : IH (le_of_succ_le_succ H))
theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n := theorem add_sub_of_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
!add.comm ▸ !add_sub_le
theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
calc calc
n + (m - n) = n + 0 : {le_imp_sub_eq_zero H} n + (m - n) = n + 0 : sub_eq_zero_of_le H
... = n : !add_zero ... = n : add_zero
theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := theorem sub_add_cancel {n m : ℕ} : n ≥ m → n - m + m = n :=
!add.comm ▸ add_sub_ge !add.comm ▸ !add_sub_of_le
theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) := theorem sub_add_of_le {n m : ℕ} : n ≤ m → n - m + m = m :=
or.elim !le.total !add.comm ▸ add_sub_of_ge
(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) := theorem sub.cases {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k)
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) := : P (n - m) :=
or.elim !le.total or.elim !le.total
(assume H3 : n ≤ m, (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 H3)) (assume H3 : n ≤ m, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 H3))
(assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) (assume H3 : m ≤ n, H2 (n - m) (add_sub_of_le H3))
theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n := theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
obtain (k : ℕ) (Hk : n + k = m), from le.elim H, obtain (k : ℕ) (Hk : n + k = m), from le.elim H,
exists.intro k exists.intro k
(calc (calc
m - k = n + k - k : {Hk⁻¹} m - k = n + k - k : Hk⁻¹
... = n : !sub_add_left) ... = n : add_sub_cancel)
theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - 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 have l1 : k ≤ m → n + m - k = n + (m - k), from
@ -235,21 +215,21 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
(take m : ℕ, (take m : ℕ,
assume H : 0 ≤ m, assume H : 0 ≤ m,
calc calc
n + m - 0 = n + m : !sub_zero_right n + m - 0 = n + m : sub_zero
... = n + (m - 0) : {!sub_zero_right⁻¹}) ... = n + (m - 0) : sub_zero)
(take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
(take k m, (take k m,
assume IH : k ≤ m → n + m - k = n + (m - k), assume IH : k ≤ m → n + m - k = n + (m - k),
take H : succ k ≤ succ m, take H : succ k ≤ succ m,
calc calc
n + succ m - succ k = succ (n + m) - succ k : {!add_succ} n + succ m - succ k = succ (n + m) - succ k : add_succ
... = n + m - k : !sub_succ_succ ... = n + m - k : succ_sub_succ
... = n + (m - k) : IH (le_of_succ_le_succ H) ... = n + (m - k) : IH (le_of_succ_le_succ H)
... = n + (succ m - succ k) : {!sub_succ_succ⁻¹}), ... = n + (succ m - succ k) : succ_sub_succ),
l1 H l1 H
theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m := theorem le_of_sub_eq_zero {n m : ℕ} : n - m = 0 → n ≤ m :=
sub_split sub.cases
(assume H1 : n ≤ m, assume H2 : 0 = 0, H1) (assume H1 : n ≤ m, assume H2 : 0 = 0, H1)
(take k : ℕ, (take k : ℕ,
assume H1 : m + k = n, assume H1 : m + k = n,
@ -257,38 +237,38 @@ sub_split
have H3 : n = m, from !add_zero ▸ H2 ▸ H1⁻¹, have H3 : n = m, from !add_zero ▸ H2 ▸ H1⁻¹,
H3 ▸ !le.refl) H3 ▸ !le.refl)
theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) theorem sub_sub.cases {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) := (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
or.elim !le.total or.elim !le.total
(assume H3 : n ≤ m, (assume H3 : n ≤ m,
le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) sub_eq_zero_of_le H3⁻¹ ▸ (H2 (m - n) (add_sub_of_le H3⁻¹)))
(assume H3 : m ≤ n, (assume H3 : m ≤ n,
le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹))) sub_eq_zero_of_le H3⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3⁻¹)))
theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m := theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m :=
have H2 : k - n + n = m + n, from have H2 : k - n + n = m + n, from
calc calc
k - n + n = k : add_sub_ge_left (le.intro H) k - n + n = k : sub_add_cancel (le.intro H)
... = n + m : H⁻¹ ... = n + m : H⁻¹
... = m + n : !add.comm, ... = m + n : !add.comm,
add.cancel_right H2 add.cancel_right H2
theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k := theorem sub_le_sub_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n - k ≤ m - k :=
obtain (l : ℕ) (Hl : n + l = m), from le.elim H, obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
or.elim !le.total or.elim !le.total
(assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ !zero_le) (assume H2 : n ≤ k, (sub_eq_zero_of_le H2)⁻¹ ▸ !zero_le)
(assume H2 : k ≤ n, (assume H2 : k ≤ n,
have H3 : n - k + l = m - k, from have H3 : n - k + l = m - k, from
calc calc
n - k + l = l + (n - k) : add.comm n - k + l = l + (n - k) : add.comm
... = l + n - k : (add_sub_assoc H2 l)⁻¹ ... = l + n - k : add_sub_assoc H2 l
... = n + l - k : {!add.comm} ... = n + l - k : add.comm
... = m - k : {Hl}, ... = m - k : Hl,
le.intro H3) le.intro H3)
theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n := theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n :=
obtain (l : ℕ) (Hl : n + l = m), from le.elim H, obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
sub_split sub.cases
(assume H2 : k ≤ m, !zero_le) (assume H2 : k ≤ m, !zero_le)
(take m' : ℕ, (take m' : ℕ,
assume Hm : m + m' = k, assume Hm : m + m' = k,
@ -298,33 +278,43 @@ sub_split
m' + l + n = n + (m' + l) : add.comm m' + l + n = n + (m' + l) : add.comm
... = n + (l + m') : add.comm ... = n + (l + m') : add.comm
... = n + l + m' : add.assoc ... = n + l + m' : add.assoc
... = m + m' : {Hl} ... = m + m' : Hl
... = k : Hm ... = k : Hm
... = k - n + n : (add_sub_ge_left H3)⁻¹, ... = k - n + n : sub_add_cancel H3,
le.intro (add.cancel_right H4)) le.intro (add.cancel_right H4))
theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 := theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
have H1 : n = n - m + m, from (add_sub_ge_left (le_of_lt H))⁻¹, have H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H, have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
!lt_of_add_lt_add_right H2 !lt_of_add_lt_add_right H2
-- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n :=
-- := lt_of_not_le
-- _ (take H1 : m ≥ n,
have H2 : n - m = 0, from sub_eq_zero_of_le H1,
!lt.irrefl (H2 ▸ H))
-- theorem sub_lt_cancel_left {n m k : ℕ) (H : n - m < n - k) : k < m theorem lt_of_sub_lt_sub_right {n m k : ℕ} (H : n - k < m - k) : n < m :=
-- := lt_of_not_le
-- _ (assume H1 : m ≤ n,
have H2 : m - k ≤ n - k, from sub_le_sub_right H1 _,
not_le_of_lt H H2)
theorem sub_triangle_inequality (n m k : ℕ) : n - k ≤ (n - m) + (m - k) := theorem lt_of_sub_lt_sub_left {n m k : ℕ} (H : n - m < n - k) : k < m :=
sub_split lt_of_not_le
(assume H : n ≤ m, !zero_add⁻¹ ▸ sub_le_right H k) (assume H1 : m ≤ k,
have H2 : n - k ≤ n - m, from sub_le_sub_left H1 _,
not_le_of_lt H H2)
theorem sub_lt_sub_add_sub (n m k : ℕ) : n - k ≤ (n - m) + (m - k) :=
sub.cases
(assume H : n ≤ m, !zero_add⁻¹ ▸ sub_le_sub_right H k)
(take mn : ℕ, (take mn : ℕ,
assume Hmn : m + mn = n, assume Hmn : m + mn = n,
sub_split sub.cases
(assume H : m ≤ k, (assume H : m ≤ k,
have H2 : n - k ≤ n - m, from sub_le_left H n, have H2 : n - k ≤ n - m, from sub_le_sub_left H n,
have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2, have H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2,
show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3) show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3)
(take km : ℕ, (take km : ℕ,
assume Hkm : k + km = m, assume Hkm : k + km = m,
@ -334,23 +324,14 @@ sub_split
... = k + km + mn : add.assoc ... = k + km + mn : add.assoc
... = m + mn : Hkm ... = m + mn : Hkm
... = n : Hmn, ... = n : Hmn,
have H2 : n - k = mn + km, from sub_intro H, have H2 : n - k = mn + km, from sub_eq_of_add_eq H,
H2 ▸ !le.refl)) H2 ▸ !le.refl))
/- distance -/
-- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
-- absolute difference
-- --------------------------------------------
-- ### absolute difference
-- This section is still incomplete
definition dist [reducible] (n m : ℕ) := (n - m) + (m - n) definition dist [reducible] (n m : ℕ) := (n - m) + (m - n)
theorem dist_comm (n m : ℕ) : dist n m = dist m n := theorem dist.comm (n m : ℕ) : dist n m = dist m n :=
!add.comm !add.comm
theorem dist_self (n : ℕ) : dist n n = 0 := theorem dist_self (n : ℕ) : dist n n = 0 :=
@ -359,78 +340,75 @@ calc
... = 0 + 0 : sub_self ... = 0 + 0 : sub_self
... = 0 : rfl ... = 0 : rfl
theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m := theorem eq_of_dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H, have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
have H3 : n ≤ m, from sub_eq_zero_imp_le H2, have H3 : n ≤ m, from le_of_sub_eq_zero H2,
have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H, have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H,
have H5 : m ≤ n, from sub_eq_zero_imp_le H4, have H5 : m ≤ n, from le_of_sub_eq_zero H4,
le.antisymm H3 H5 le.antisymm H3 H5
theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n := theorem dist_eq_sub_of_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
calc calc
dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H} dist n m = 0 + (m - n) : {sub_eq_zero_of_le H}
... = m - n : !zero_add ... = m - n : zero_add
theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m := theorem dist_eq_sub_of_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
!dist_comm ▸ dist_le H !dist.comm ▸ dist_eq_sub_of_le H
theorem dist_zero_right (n : ℕ) : dist n 0 = n := theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
dist_ge !zero_le ⬝ !sub_zero_right dist_eq_sub_of_ge !zero_le ⬝ !sub_zero
theorem dist_zero_left (n : ℕ) : dist 0 n = n := theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
dist_le !zero_le ⬝ !sub_zero_right dist_eq_sub_of_le !zero_le ⬝ !sub_zero
theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m := theorem dist.intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
calc calc
dist k n = k - n : dist_ge (le.intro H) dist k n = k - n : dist_eq_sub_of_ge (le.intro H)
... = m : sub_intro H ... = m : sub_eq_of_add_eq H
theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m := theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
calc calc
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : rfl 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 + k) - (n + k)) : add_sub_add_right
... = (n - m) + (m - n) : {!sub_add_add_right} ... = (n - m) + (m - n) : add_sub_add_right
theorem dist_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m := theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m :=
!add.comm ▸ !add.comm ▸ !dist_add_right !add.comm ▸ !add.comm ▸ !dist_add_add_right
-- add_rewrite dist_self dist_add_right dist_add_left dist_zero_left dist_zero_right theorem dist_add_eq_of_ge {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 calc
dist n m + m = n - m + m : {dist_ge H} dist n m + m = n - m + m : {dist_eq_sub_of_ge H}
... = n : add_sub_ge_left H ... = n : sub_add_cancel H
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m := theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=
calc calc
dist n k = dist (n + m) (k + m) : !dist_add_right⁻¹ dist n k = dist (n + m) (k + m) : dist_add_add_right
... = dist (k + l) (k + m) : {H} ... = dist (k + l) (k + m) : H
... = dist l m : !dist_add_left ... = dist l m : dist_add_add_left
theorem dist_sub_move_add {n m : ℕ} (H : n ≥ m) (k : ℕ) : dist (n - m) k = dist n (k + m) := theorem dist_sub_eq_dist_add_left {n m : ℕ} (H : n ≥ m) (k : ℕ) :
dist (n - m) k = dist n (k + m) :=
have H2 : n - m + (k + m) = k + n, from have H2 : n - m + (k + m) = k + n, from
calc calc
n - m + (k + m) = n - m + (m + k) : add.comm n - m + (k + m) = n - m + (m + k) : add.comm
... = n - m + m + k : add.assoc ... = n - m + m + k : add.assoc
... = n + k : {add_sub_ge_left H} ... = n + k : sub_add_cancel H
... = k + n : add.comm, ... = k + n : add.comm,
dist_eq_intro H2 dist_eq_intro H2
theorem dist_sub_move_add' {k m : ℕ} (H : k ≥ m) (n : ℕ) : dist n (k - m) = dist (n + m) k := theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
(dist_sub_move_add H n ▸ !dist_comm) ▸ !dist_comm dist n (k - m) = dist (n + m) k :=
(dist_sub_eq_dist_add_left H n ▸ !dist.comm) ▸ !dist.comm
--triangle inequality formulated with dist theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
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)), have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
by simp, by simp,
H ▸ add_le_add !sub_triangle_inequality !sub_triangle_inequality H ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
theorem dist_add_le_add_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l := theorem dist_add_add_le_add_dist_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 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, !dist_add_add_left ▸ !dist_add_add_right ▸ rfl,
H ▸ !triangle_inequality H ▸ !dist.triangle_inequality
--interaction with multiplication
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := 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, have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
@ -440,9 +418,6 @@ 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, have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
by simp 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) := 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 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 : ℕ, take k l : ℕ,
@ -450,15 +425,15 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
have H2 : m * k ≥ m * l, from mul_le_mul_left H m, have H2 : m * k ≥ m * l, from mul_le_mul_left H m,
have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left, have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left,
calc calc
dist n m * dist k l = dist n m * (k - l) : {dist_ge H} dist n m * dist k l = dist n m * (k - l) : dist_eq_sub_of_ge H
... = dist (n * (k - l)) (m * (k - l)) : !dist_mul_right⁻¹ ... = dist (n * (k - l)) (m * (k - l)) : dist_mul_right
... = dist (n * k - n * l) (m * k - m * l) : by simp ... = 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_mul_left H n) _ ... = dist (n * k) (m * k - m * l + n * l) : dist_sub_eq_dist_add_left (mul_le_mul_left H n)
... = dist (n * k) (n * l + (m * k - m * l)) : {!add.comm} ... = 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) (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 _, ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _,
or.elim !le.total or.elim !le.total
(assume H : k ≤ l, !dist_comm ▸ !dist_comm ▸ aux l k H) (assume H : k ≤ l, !dist.comm ▸ !dist.comm ▸ aux l k H)
(assume H : l ≤ k, aux k l H) (assume H : l ≤ k, aux k l H)
end nat end nat