From 0dcf06000b1325bb10082c12bdc52434c9bb85da Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 12 Jan 2015 16:28:42 -0500 Subject: [PATCH] refactor(library/data/int/sub): rename theorems, add theorems, clean up --- library/algebra/group.lean | 6 - library/data/int/basic.lean | 29 +-- library/data/nat/div.lean | 22 +- library/data/nat/order.lean | 5 + library/data/nat/sub.lean | 389 +++++++++++++++++------------------- 5 files changed, 213 insertions(+), 238 deletions(-) diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 33936caba..bf1e19637 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -45,7 +45,6 @@ prefix `-` := has_neg.neg notation 1 := !has_one.one notation 0 := !has_zero.zero - /- semigroup -/ 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 := !right_cancel_semigroup.mul_right_cancel - /- additive semigroup -/ 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 - /- additive monoid -/ 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 - /- group -/ 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 - /- additive group -/ structure add_group [class] (A : Type) extends add_monoid A, has_neg A := @@ -489,7 +484,6 @@ include s end add_comm_group - /- bundled structures -/ structure Semigroup := diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 0a92a2e8f..a567336e3 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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 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 sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl ... = of_nat (m - n) : rfl @@ -131,7 +131,7 @@ context reducible sub_nat_nat theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) : 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 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 @@ -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, H1⁻¹ ▸ (calc - m - n + n = m : add_sub_ge_left H + m - n + n = m : sub_add_cancel H ... = 0 + m : zero_add)) (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, H1⁻¹ ▸ (calc 0 + n = n : zero_add - ... = n - m + m : add_sub_ge_left (le_of_lt H) - ... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_gt H))⁻¹)) + ... = n - m + m : sub_add_cancel (le_of_lt H) + ... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_lt H))⁻¹)) theorem repr_abstr (p : ℕ × ℕ) : repr (abstr p) ≡ p := !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 H5 : pr1 p = pr1 q - pr2 q + pr2 p, from 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) : add_sub_assoc H4 ... = pr1 q - pr2 q + pr2 p : add.comm, have H6 : pr1 p - pr2 p = pr1 q - pr2 q, from calc 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)⁻¹) (assume H2, have H3 : pr1 p < pr2 p, from and.elim_left H2, have H4 : pr1 q < pr2 q, from and.elim_right H2, have H5 : pr2 p = pr2 q - pr1 q + pr1 p, from 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) : add_sub_assoc (le_of_lt H4) ... = pr2 q - pr1 q + pr1 p : add.comm, have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from calc 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)⁻¹) 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, calc 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, calc nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H ... = succ (pred (n - m)) : rfl - ... = n - m : succ_pred_of_pos (sub_pos_of_gt H) - ... = dist m n : dist_le (le_of_lt H)) + ... = n - m : succ_pred_of_pos (sub_pos_of_lt H) + ... = dist m n : dist_eq_sub_of_le (le_of_lt H)) end 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 (abstr (pneg (repr a))) : repr_neg ... = 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 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, 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 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 context diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index dfc78e0a9..31e0da9ae 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -1,4 +1,4 @@ -/- + /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. 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₂) theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := -calc (x + z) div z - = if 0 < z ∧ z ≤ x + z then divide (x + z - z) z + 1 else 0 : !divide_def -... = divide (x + z - z) z + 1 : if_pos (and.intro H (le_add_left z x)) -... = succ (x div z) : sub_add_left +calc + (x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def + ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x)) + ... = 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 := 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 = 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 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 := 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 + (succ x - y) mod y + y : add.right_comm ... = 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 := 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, have H2 : (z - x div y) * y = x mod y, from 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 : sub_add_left, + ... = x mod y : add_sub_cancel, show x mod y = 0, from by_cases (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) := by_cases (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) (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 _) -- Gcd and lcm diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 9bb8b0c77..30a8f64fc 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -308,6 +308,11 @@ nat.cases_on n assume H : succ n' ≤ m, !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 := 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) diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index acd079666..4ceaedcfa 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -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. ---- Author: Floris van Doorn +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. --- data.nat.sub --- ============ --- --- Subtraction on the natural numbers, as well as min, max, and distance. +Authors: Floris van Doorn, Jeremy Avigad +Module: data.nat.sub + +Subtraction on the natural numbers, as well as min, max, and distance. +-/ import .order import tools.fake_simplifier @@ -15,33 +16,30 @@ open fake_simplifier namespace nat --- subtraction --- ----------- +/- subtraction -/ -theorem sub_zero_right (n : ℕ) : n - 0 = n := +theorem sub_zero (n : ℕ) : n - 0 = n := 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 -irreducible sub - -theorem sub_zero_left (n : ℕ) : 0 - n = 0 := -induction_on n !sub_zero_right +theorem zero_sub (n : ℕ) : 0 - n = 0 := +induction_on n !sub_zero (take k : nat, assume IH : 0 - k = 0, calc - 0 - succ k = pred (0 - k) : !sub_succ_right - ... = pred 0 : {IH} + 0 - succ k = pred (0 - k) : sub_succ + ... = pred 0 : IH ... = 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 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 (calc (n + 0) - (m + 0) = n - (m + 0) : {!add_zero} @@ -51,183 +49,165 @@ induction_on k calc (n + succ l) - (m + succ l) = succ (n + l) - (m + succ 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) -theorem sub_add_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := -!add.comm ▸ !add.comm ▸ !sub_add_add_right +theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := +!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 - (!add_zero⁻¹ ▸ !sub_zero_right) + (!add_zero⁻¹ ▸ !sub_zero) (take k : ℕ, assume IH : n + k - k = n, calc - n + succ k - succ k = succ (n + k) - succ k : {!add_succ} - ... = n + k - k : !sub_succ_succ + n + succ k - succ k = succ (n + k) - succ k : add_succ + ... = n + k - k : succ_sub_succ ... = n : IH) --- TODO: add_sub_inv' -theorem sub_add_left2 (n m : ℕ) : n + m - n = m := -!add.comm ▸ !sub_add_left +theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m := +!add.comm ▸ !add_sub_cancel 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⁻¹}) + n - m - 0 = n - m : sub_zero + ... = n - (m + 0) : add_zero) (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 = pred (n - m - l) : !sub_succ + ... = pred (n - (m + l)) : IH + ... = n - succ (m + l) : sub_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 - succ n - m - succ k = succ n - (m + succ k) : !sub_sub - ... = succ n - succ (m + k) : {!add_succ} - ... = n - (m + k) : !sub_succ_succ - ... = n - m - k : !sub_sub⁻¹ + succ n - m - succ k = succ n - (m + succ k) : sub_sub + ... = succ n - succ (m + k) : add_succ + ... = n - (m + k) : succ_sub_succ + ... = 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 - n - (n + m) = n - n - m : !sub_sub⁻¹ - ... = 0 - m : {!sub_self} - ... = 0 : !sub_zero_left + n - (n + m) = n - n - m : sub_sub + ... = 0 - m : sub_self + ... = 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 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} +rfl 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 := induction_on n (calc - pred 0 * m = 0 * m : {pred_zero} - ... = 0 : !zero_mul - ... = 0 - m : !sub_zero_left⁻¹ - ... = 0 * m - m : {!zero_mul⁻¹}) + pred 0 * m = 0 * m : pred_zero + ... = 0 : zero_mul + ... = 0 - m : zero_sub + ... = 0 * m - m : zero_mul) (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 : {!succ_mul⁻¹}) + pred (succ k) * m = k * m : pred_succ + ... = k * m + m - m : add_sub_cancel + ... = succ k * m - m : succ_mul) 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} +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 := +theorem mul_sub_right_distrib (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 : {!zero_mul⁻¹}) + (n - 0) * k = n * k : sub_zero + ... = n * k - 0 : sub_zero + ... = n * k - 0 * k : zero_mul) (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) : {!succ_mul⁻¹}) + (n - succ l) * k = pred (n - l) * k : sub_succ + ... = (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) : succ_mul) 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 + ... = m * n - k * n : !mul_sub_right_distrib ... = n * m - k * n : {!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) := 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, + (take k, assume H : 0 ≤ k, rfl) + (take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (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 (succ l) - succ k = succ l - k : succ_sub_succ ... = 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 := -obtain (k : ℕ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_add_right_eq_zero +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_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 (take k, assume H : 0 ≤ k, calc - 0 + (k - 0) = k - 0 : !zero_add - ... = k : !sub_zero_right) + 0 + (k - 0) = k - 0 : zero_add + ... = k : sub_zero) (take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (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 (le_of_succ_le_succ H)}) + succ k + (succ l - succ k) = succ k + (l - k) : succ_sub_succ + ... = succ (k + (l - k)) : add.succ_left + ... = succ l : IH (le_of_succ_le_succ 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 := +theorem add_sub_of_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 + n + (m - n) = n + 0 : sub_eq_zero_of_le H + ... = n : add_zero -theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := -!add.comm ▸ add_sub_ge +theorem sub_add_cancel {n m : ℕ} : n ≥ m → n - m + m = n := +!add.comm ▸ !add_sub_of_le -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 sub_add_of_le {n m : ℕ} : n ≤ m → n - m + m = m := +!add.comm ▸ add_sub_of_ge -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) +theorem sub.cases {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)) + (assume H3 : n ≤ m, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 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, exists.intro k (calc - m - k = n + k - k : {Hk⁻¹} - ... = n : !sub_add_left) + m - k = n + k - k : Hk⁻¹ + ... = n : add_sub_cancel) 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 @@ -235,21 +215,21 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from (take m : ℕ, assume H : 0 ≤ m, calc - n + m - 0 = n + m : !sub_zero_right - ... = n + (m - 0) : {!sub_zero_right⁻¹}) + n + m - 0 = n + m : sub_zero + ... = n + (m - 0) : sub_zero) (take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero) (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} - ... = n + m - k : !sub_succ_succ + n + succ m - succ k = succ (n + m) - succ k : add_succ + ... = n + m - k : succ_sub_succ ... = 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 -theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m := -sub_split +theorem le_of_sub_eq_zero {n m : ℕ} : n - m = 0 → n ≤ m := +sub.cases (assume H1 : n ≤ m, assume H2 : 0 = 0, H1) (take k : ℕ, assume H1 : m + k = n, @@ -257,38 +237,38 @@ sub_split have H3 : n = m, from !add_zero ▸ H2 ▸ H1⁻¹, 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) := or.elim !le.total (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, - 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 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⁻¹ ... = m + n : !add.comm, 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, 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, have H3 : n - k + l = m - k, from calc n - k + l = l + (n - k) : add.comm - ... = l + n - k : (add_sub_assoc H2 l)⁻¹ - ... = n + l - k : {!add.comm} - ... = m - k : {Hl}, + ... = 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 := +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, -sub_split +sub.cases (assume H2 : k ≤ m, !zero_le) (take m' : ℕ, assume Hm : m + m' = k, @@ -298,33 +278,43 @@ sub_split m' + l + n = n + (m' + l) : add.comm ... = n + (l + m') : add.comm ... = n + l + m' : add.assoc - ... = m + m' : {Hl} + ... = m + m' : Hl ... = k : Hm - ... = k - n + n : (add_sub_ge_left H3)⁻¹, + ... = k - n + n : sub_add_cancel H3, le.intro (add.cancel_right H4)) -theorem sub_pos_of_gt {m n : ℕ} (H : n > m) : n - m > 0 := -have H1 : n = n - m + m, from (add_sub_ge_left (le_of_lt H))⁻¹, +theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 := +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, !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) := -sub_split - (assume H : n ≤ m, !zero_add⁻¹ ▸ sub_le_right H k) +theorem lt_of_sub_lt_sub_left {n m k : ℕ} (H : n - m < n - k) : k < m := +lt_of_not_le + (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 : ℕ, assume Hmn : m + mn = n, - sub_split + sub.cases (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, + have H2 : n - k ≤ n - m, from sub_le_sub_left H n, + have H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2, show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3) (take km : ℕ, assume Hkm : k + km = m, @@ -334,23 +324,14 @@ sub_split ... = k + km + mn : add.assoc ... = m + mn : Hkm ... = 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)) - --- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right - - --- absolute difference --- -------------------------------------------- - --- ### absolute difference - --- This section is still incomplete +/- distance -/ 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 theorem dist_self (n : ℕ) : dist n n = 0 := @@ -359,78 +340,75 @@ calc ... = 0 + 0 : sub_self ... = 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 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 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 -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 - dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H} - ... = m - n : !zero_add + dist n m = 0 + (m - n) : {sub_eq_zero_of_le H} + ... = m - n : zero_add -theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m := -!dist_comm ▸ dist_le H +theorem dist_eq_sub_of_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m := +!dist.comm ▸ dist_eq_sub_of_le H 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 := -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 - dist k n = k - n : dist_ge (le.intro H) - ... = m : sub_intro H + dist k n = k - n : dist_eq_sub_of_ge (le.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 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} + ... = (n - m) + ((m + k) - (n + k)) : add_sub_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 := -!add.comm ▸ !add.comm ▸ !dist_add_right +theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m := +!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_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n := +theorem dist_add_eq_of_ge {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 + dist n m + m = n - m + m : {dist_eq_sub_of_ge 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 := calc - dist n k = dist (n + m) (k + m) : !dist_add_right⁻¹ - ... = dist (k + l) (k + m) : {H} - ... = dist l m : !dist_add_left + dist n k = dist (n + m) (k + m) : dist_add_add_right + ... = dist (k + l) (k + m) : H + ... = 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 calc n - m + (k + m) = n - m + (m + k) : add.comm ... = n - m + m + k : add.assoc - ... = n + k : {add_sub_ge_left H} + ... = n + k : sub_add_cancel H ... = k + n : add.comm, 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 +theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) : + 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 triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k := +theorem dist.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_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 - !dist_add_left ▸ !dist_add_right ▸ rfl, -H ▸ !triangle_inequality - ---interaction with multiplication + !dist_add_add_left ▸ !dist_add_add_right ▸ rfl, +H ▸ !dist.triangle_inequality 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, @@ -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, 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 : ℕ, @@ -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 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 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 - 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) (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 _, + ... = 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_sub_assoc H2 (n * l) + ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _, 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) end nat