lean2/library/data/nat/order.lean

527 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, Leonardo de Moura
-- data.nat.order
-- ==============
--
-- The ordering on the natural numbers
import .basic
open eq.ops
namespace nat
-- TODO: move this
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
iff.intro succ_le_of_lt lt_of_succ_le
-- Less than or equal
-- ------------------
theorem le.succ_right {n m : } (h : n ≤ m) : n ≤ succ m :=
lt.step h
theorem le.add_right (n k : ) : n ≤ n + k :=
induction_on k
(calc n ≤ n : le.refl n
... = n + zero : add_zero)
(λ k (ih : n ≤ n + k), calc
n ≤ succ (n + k) : le.succ_right ih
... = n + succ k : add_succ)
theorem le_intro {n m k : } (h : n + k = m) : n ≤ m :=
h ▸ le.add_right n k
theorem le_elim {n m : } (h : n ≤ m) : ∃k, n + k = m :=
le.rec_on h
(exists.intro 0 rfl)
(λ m (h : n < m), lt.rec_on h
(exists.intro 1 rfl)
(λ b hlt (ih : ∃ (k : ), n + k = b),
obtain (k : ) (h : n + k = b), from ih,
exists.intro (succ k) (calc
n + succ k = succ (n + k) : add_succ
... = succ b : h)))
-- ### partial order (totality is part of less than)
theorem le_refl (n : ) : n ≤ n :=
le.refl n
theorem zero_le (n : ) : 0 ≤ n :=
le_intro !zero_add
theorem le_zero {n : } (H : n ≤ 0) : n = 0 :=
obtain (k : ) (Hk : n + k = 0), from le_elim H,
eq_zero_of_add_eq_zero_right Hk
theorem not_succ_zero_le (n : ) : ¬ succ n ≤ 0 :=
(assume H : succ n ≤ 0,
have H2 : succ n = 0, from le_zero H,
absurd H2 !succ_ne_zero)
theorem le_trans {n m k : } (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
le.trans H1 H2
theorem le_antisym {n m : } (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
obtain (k : ) (Hk : n + k = m), from (le_elim H1),
obtain (l : ) (Hl : m + l = n), from (le_elim H2),
have L1 : k + l = 0, from
add.cancel_left
(calc
n + (k + l) = n + k + l : !add.assoc⁻¹
... = m + l : {Hk}
... = n : Hl
... = n + 0 : !add_zero⁻¹),
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
calc
n = n + 0 : !add_zero⁻¹
... = n + k : {L2⁻¹}
... = m : Hk
-- ### interaction with addition
theorem le_add_right (n m : ) : n ≤ n + m :=
le_intro rfl
theorem le_add_left (n m : ): n ≤ m + n :=
le_intro !add.comm
theorem add_le_left {n m : } (H : n ≤ m) (k : ) : k + n ≤ k + m :=
obtain (l : ) (Hl : n + l = m), from (le_elim H),
le_intro
(calc
k + n + l = k + (n + l) : !add.assoc
... = k + m : {Hl})
theorem add_le_right {n m : } (H : n ≤ m) (k : ) : n + k ≤ m + k :=
!add.comm ▸ !add.comm ▸ add_le_left H k
theorem add_le {n m k l : } (H1 : n ≤ k) (H2 : m ≤ l) : n + m ≤ k + l :=
le_trans (add_le_right H1 m) (add_le_left H2 k)
theorem add_le_cancel_left {n m k : } (H : k + n ≤ k + m) : n ≤ m :=
obtain (l : ) (Hl : k + n + l = k + m), from (le_elim H),
le_intro (add.cancel_left
(calc
k + (n + l) = k + n + l : !add.assoc⁻¹
... = k + m : Hl))
theorem add_le_cancel_right {n m k : } (H : n + k ≤ m + k) : n ≤ m :=
add_le_cancel_left (!add.comm ▸ !add.comm ▸ H)
theorem add_le_inv {n m k l : } (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤ l :=
obtain (a : ) (Ha : k + a = n), from le_elim H2,
have H3 : k + (a + m) ≤ k + l, from !add.assoc ▸ Ha⁻¹ ▸ H1,
have H4 : a + m ≤ l, from add_le_cancel_left H3,
show m ≤ l, from le_trans !le_add_left H4
-- add_rewrite le_add_right le_add_left
-- ### interaction with successor and predecessor
theorem succ_le {n m : } (H : n ≤ m) : succ n ≤ succ m :=
!add_one ▸ !add_one ▸ add_le_right H 1
theorem succ_le_cancel {n m : } (H : succ n ≤ succ m) : n ≤ m :=
add_le_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
theorem self_le_succ (n : ) : n ≤ succ n :=
le_intro !add_one
theorem le_imp_le_succ {n m : } (H : n ≤ m) : n ≤ succ m :=
le_trans H !self_le_succ
theorem le_imp_succ_le_or_eq {n m : } (H : n ≤ m) : succ n ≤ m n = m :=
obtain (k : ) (Hk : n + k = m), from (le_elim H),
discriminate
(assume H3 : k = 0,
have Heq : n = m,
from calc
n = n + 0 : !add_zero⁻¹
... = n + k : {H3⁻¹}
... = m : Hk,
or.inr Heq)
(take l : nat,
assume H3 : k = succ l,
have Hlt : succ n ≤ m, from
(le_intro
(calc
succ n + l = n + succ l : !succ_add_eq_add_succ
... = n + k : {H3⁻¹}
... = m : Hk)),
or.inl Hlt)
theorem le_ne_imp_succ_le {n m : } (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m :=
or_resolve_left (le_imp_succ_le_or_eq H1) H2
theorem le_succ_imp_le_or_eq {n m : } (H : n ≤ succ m) : n ≤ m n = succ m :=
or_of_or_of_imp_left (le_imp_succ_le_or_eq H)
(take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2)
theorem succ_le_imp_le_and_ne {n m : } (H : succ n ≤ m) : n ≤ m ∧ n ≠ m :=
obtain (k : ) (H2 : succ n + k = m), from (le_elim H),
and.intro
(have H3 : n + succ k = m,
from calc
n + succ k = succ n + k : !succ_add_eq_add_succ⁻¹
... = m : H2,
show n ≤ m, from le_intro H3)
(assume H3 : n = m,
have H4 : succ n ≤ n, from H3⁻¹ ▸ H,
have H5 : succ n = n, from le_antisym H4 !self_le_succ,
show false, from absurd H5 succ.ne_self)
theorem le_pred_self (n : ) : pred n ≤ n :=
cases_on n
(pred.zero⁻¹ ▸ !le_refl)
(take k : , !pred.succ⁻¹ ▸ !self_le_succ)
theorem pred_le_pre_of_le {n m : } (H : n ≤ m) : pred n ≤ pred m :=
discriminate
(take Hn : n = 0,
have H2 : pred n = 0,
from calc
pred n = pred 0 : {Hn}
... = 0 : pred.zero,
H2⁻¹ ▸ !zero_le)
(take k : ,
assume Hn : n = succ k,
obtain (l : ) (Hl : n + l = m), from le_elim H,
have H2 : pred n + l = pred m,
from calc
pred n + l = pred (succ k) + l : {Hn}
... = k + l : {!pred.succ}
... = pred (succ (k + l)) : !pred.succ⁻¹
... = pred (succ k + l) : {!add.succ_left⁻¹}
... = pred (n + l) : {Hn⁻¹}
... = pred m : {Hl},
le_intro H2)
theorem pred_le_imp_le_or_eq {n m : } (H : pred n ≤ m) : n ≤ m n = succ m :=
discriminate
(take Hn : n = 0,
or.inl (Hn⁻¹ ▸ !zero_le))
(take k : ,
assume Hn : n = succ k,
have H2 : pred n = k,
from calc
pred n = pred (succ k) : {Hn}
... = k : !pred.succ,
have H3 : k ≤ m, from H2 ▸ H,
have H4 : succ k ≤ m k = m, from le_imp_succ_le_or_eq H3,
show n ≤ m n = succ m, from
or_of_or_of_imp_of_imp H4
(take H5 : succ k ≤ m, show n ≤ m, from Hn⁻¹ ▸ H5)
(take H5 : k = m, show n = succ m, from H5 ▸ Hn))
-- ### interaction with multiplication
theorem mul_le_left {n m : } (H : n ≤ m) (k : ) : k * n ≤ k * m :=
obtain (l : ) (Hl : n + l = m), from (le_elim H),
have H2 : k * n + k * l = k * m, from
calc
k * n + k * l = k * (n + l) : mul.left_distrib
... = k * m : {Hl},
le_intro H2
theorem mul_le_right {n m : } (H : n ≤ m) (k : ) : n * k ≤ m * k :=
!mul.comm ▸ !mul.comm ▸ (mul_le_left H k)
theorem mul_le {n m k l : } (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
le_trans (mul_le_right H1 m) (mul_le_left H2 k)
-- Less than, Greater than, Greater than or equal
-- ----------------------------------------------
theorem lt_intro {n m k : } (H : succ n + k = m) : n < m :=
lt_of_succ_le (le_intro H)
theorem lt_elim {n m : } (H : n < m) : ∃ k, succ n + k = m :=
le_elim (succ_le_of_lt H)
theorem lt_add_succ (n m : ) : n < n + succ m :=
lt_intro !succ_add_eq_add_succ
-- ### basic facts
theorem lt_imp_ne {n m : } (H : n < m) : n ≠ m :=
λ heq : n = m, absurd H (heq ▸ !lt.irrefl)
theorem lt_irrefl (n : ) : ¬ n < n :=
(assume H : n < n, absurd rfl (lt_imp_ne H))
theorem lt_def (n m : ) : n < m ↔ succ n ≤ m :=
iff.intro
(λ h, succ_le_of_lt h)
(λ h, lt_of_succ_le h)
theorem succ_pos (n : ) : 0 < succ n :=
!zero_lt_succ
theorem succ_pred_of_pos {n : } (H : n > 0) : succ (pred n) = n :=
(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (lt_imp_ne H))⁻¹)
theorem lt_imp_eq_succ {n m : } (H : n < m) : exists k, m = succ k :=
discriminate
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
(take (l : ) (Hm : m = succ l), exists.intro l Hm)
-- ### interaction with le
theorem self_lt_succ (n : ) : n < succ n :=
lt.base n
theorem lt_imp_le {n m : } (H : n < m) : n ≤ m :=
le.of_lt H
theorem le_imp_lt_or_eq {n m : } (H : n ≤ m) : n < m n = m :=
or.swap (eq_or_lt_of_le H)
theorem le_ne_imp_lt {n m : } (H1 : n ≤ m) (H2 : n ≠ m) : n < m :=
or_resolve_left (le_imp_lt_or_eq H1) H2
theorem lt_succ_imp_le {n m : } (H : n < succ m) : n ≤ m :=
succ_le_cancel (succ_le_of_lt H)
theorem le_imp_not_gt {n m : } (H : n ≤ m) : ¬ n > m :=
le.rec_on H
!lt.irrefl
(λ m (h : n < m), lt.asymm h)
theorem lt_imp_not_ge {n m : } (H : n < m) : ¬ n ≥ m :=
(assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
theorem lt_antisym {n m : } (H : n < m) : ¬ m < n :=
lt.asymm H
-- le_imp_not_gt (lt_imp_le H)
-- ### interaction with addition
theorem add_lt_left {n m : } (H : n < m) (k : ) : k + n < k + m :=
lt_of_succ_le (!add_succ ▸ add_le_left (succ_le_of_lt H) k)
theorem add_lt_right {n m : } (H : n < m) (k : ) : n + k < m + k :=
!add.comm ▸ !add.comm ▸ add_lt_left H k
theorem add_le_lt {n m k l : } (H1 : n ≤ k) (H2 : m < l) : n + m < k + l :=
lt.of_le_of_lt (add_le_right H1 m) (add_lt_left H2 k)
theorem add_lt_le {n m k l : } (H1 : n < k) (H2 : m ≤ l) : n + m < k + l :=
lt.of_lt_of_le (add_lt_right H1 m) (add_le_left H2 k)
theorem add_lt {n m k l : } (H1 : n < k) (H2 : m < l) : n + m < k + l :=
add_lt_le H1 (lt_imp_le H2)
theorem add_lt_cancel_left {n m k : } (H : k + n < k + m) : n < m :=
lt_of_succ_le (add_le_cancel_left (!add_succ⁻¹ ▸ (succ_le_of_lt H)))
theorem add_lt_cancel_right {n m k : } (H : n + k < m + k) : n < m :=
add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H)
-- ### interaction with successor (see also the interaction with le)
theorem succ_lt {n m : } (H : n < m) : succ n < succ m :=
!add_one ▸ !add_one ▸ add_lt_right H 1
theorem succ_lt_cancel {n m : } (H : succ n < succ m) : n < m :=
add_lt_cancel_right (!add_one⁻¹ ▸ !add_one⁻¹ ▸ H)
theorem lt_imp_lt_succ {n m : } (H : n < m) : n < succ m :=
lt.step H
-- ### totality of lt and le
theorem le_or_gt {n m : } : n ≤ m n > m :=
or.rec_on (lt.trichotomy n m)
(λ h : n < m, or.inl (le.of_lt h))
(λ h : n = m m < n, or.rec_on h
(λ h : n = m, eq.rec_on h (or.inl !le.refl))
(λ h : m < n, or.inr h))
theorem trichotomy_alt (n m : ) : (n < m n = m) n > m :=
or.rec_on (lt.trichotomy n m)
(λ h, or.inl (or.inl h))
(λ h, or.rec_on h
(λ h, or.inl (or.inr h))
(λ h, or.inr h))
theorem trichotomy (n m : ) : n < m n = m n > m :=
lt.trichotomy n m
theorem le_total (n m : ) : n ≤ m m ≤ n :=
or_of_or_of_imp_right le_or_gt (assume H : m < n, lt_imp_le H)
theorem not_lt_imp_ge {n m : } (H : ¬ n < m) : n ≥ m :=
or_resolve_left le_or_gt H
theorem not_le_imp_gt {n m : } (H : ¬ n ≤ m) : n > m :=
or_resolve_right le_or_gt H
-- ### misc
protected theorem strong_induction_on {P : nat → Prop} (n : ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
have H1 : ∀ {n m : nat}, m < n → P m, from
take n,
induction_on n
(show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero)
(take n',
assume IH : ∀ {m : nat}, m < n' → P m,
have H2: P n', from H n' @IH,
show ∀m, m < succ n' → P m, from
take m,
assume H3 : m < succ n',
or.elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
(assume H4: m < n', IH H4)
(assume H4: m = n', H4⁻¹ ▸ H2)),
H1 !self_lt_succ
protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
strong_induction_on a (
take n,
show (∀m, m < n → P m) → P n, from
cases_on n
(assume H : (∀m, m < 0 → P m), show P 0, from H0)
(take n,
assume H : (∀m, m < succ n → P m),
show P (succ n), from
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
-- Positivity
-- ---------
--
-- Writing "t > 0" is the preferred way to assert that a natural number is positive.
-- ### basic
theorem case_zero_pos {P : → Prop} (y : ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
cases_on y H0 (take y, H1 !succ_pos)
theorem zero_or_pos {n : } : n = 0 n > 0 :=
or_of_or_of_imp_left
(or.swap (le_imp_lt_or_eq !zero_le))
(take H : 0 = n, H⁻¹)
theorem succ_imp_pos {n m : } (H : n = succ m) : n > 0 :=
H⁻¹ ▸ !succ_pos
theorem ne_zero_imp_pos {n : } (H : n ≠ 0) : n > 0 :=
or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
theorem pos_imp_ne_zero {n : } (H : n > 0) : n ≠ 0 :=
ne.symm (lt_imp_ne H)
theorem pos_imp_eq_succ {n : } (H : n > 0) : exists l, n = succ l :=
lt_imp_eq_succ H
theorem add_pos_right {n k : } (H : k > 0) : n + k > n :=
!add_zero ▸ add_lt_left H n
theorem add_pos_left {n : } {k : } (H : k > 0) : k + n > n :=
!add.comm ▸ add_pos_right H
-- ### multiplication
theorem mul_pos {n m : } (Hn : n > 0) (Hm : m > 0) : n * m > 0 :=
obtain (k : ) (Hk : n = succ k), from pos_imp_eq_succ Hn,
obtain (l : ) (Hl : m = succ l), from pos_imp_eq_succ Hm,
succ_imp_pos (calc
n * m = succ k * m : {Hk}
... = succ k * succ l : {Hl}
... = succ k * l + succ k : !mul_succ
... = succ (succ k * l + k) : !add_succ)
theorem mul_pos_imp_pos_left {n m : } (H : n * m > 0) : n > 0 :=
discriminate
(assume H2 : n = 0,
have H3 : n * m = 0,
from calc
n * m = 0 * m : {H2}
... = 0 : !zero_mul,
have H4 : 0 > 0, from H3 ▸ H,
absurd H4 !lt_irrefl)
(take l : nat,
assume Hl : n = succ l,
Hl⁻¹ ▸ !succ_pos)
theorem mul_pos_imp_pos_right {m n : } (H : n * m > 0) : m > 0 :=
mul_pos_imp_pos_left (!mul.comm ▸ H)
-- ### interaction of mul with le and lt
theorem mul_lt_left {n m k : } (Hk : k > 0) (H : n < m) : k * n < k * m :=
have H2 : k * n < k * n + k, from add_pos_right Hk,
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_left (succ_le_of_lt H) k,
lt.of_lt_of_le H2 H3
theorem mul_lt_right {n m k : } (Hk : k > 0) (H : n < m) : n * k < m * k :=
!mul.comm ▸ !mul.comm ▸ mul_lt_left Hk H
theorem mul_le_lt {n m k l : } (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l :=
lt.of_le_of_lt (mul_le_right H1 m) (mul_lt_left Hk H2)
theorem mul_lt_le {n m k l : } (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l :=
lt.of_le_of_lt (mul_le_left H2 n) (mul_lt_right Hl H1)
theorem mul_lt {n m k l : } (H1 : n < k) (H2 : m < l) : n * m < k * l :=
have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
have H4 : k * m < k * l, from mul_lt_left (lt.of_le_of_lt !zero_le H1) H2,
lt.of_le_of_lt H3 H4
theorem mul_lt_cancel_left {n m k : } (H : k * n < k * m) : n < m :=
or.elim le_or_gt
(assume H2 : m ≤ n,
have H3 : k * m ≤ k * n, from mul_le_left H2 k,
absurd H3 (lt_imp_not_ge H))
(assume H2 : n < m, H2)
theorem mul_lt_cancel_right {n m k : } (H : n * k < m * k) : n < m :=
mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H)
theorem mul_le_cancel_left {n m k : } (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m :=
have H2 : k * n < k * m + k, from lt.of_le_of_lt H (add_pos_right Hk),
have H3 : k * n < k * succ m, from !mul_succ⁻¹ ▸ H2,
have H4 : n < succ m, from mul_lt_cancel_left H3,
show n ≤ m, from lt_succ_imp_le H4
theorem mul_le_cancel_right {n k m : } (Hm : m > 0) (H : n * m ≤ k * m) : n ≤ k :=
mul_le_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H)
theorem mul_cancel_left {m k n : } (Hn : n > 0) (H : n * m = n * k) : m = k :=
have H2 : n * m ≤ n * k, from H ▸ !le_refl,
have H3 : n * k ≤ n * m, from H ▸ !le_refl,
have H4 : m ≤ k, from mul_le_cancel_left Hn H2,
have H5 : k ≤ m, from mul_le_cancel_left Hn H3,
le_antisym H4 H5
theorem mul_cancel_left_or {n m k : } (H : n * m = n * k) : n = 0 m = k :=
or_of_or_of_imp_right zero_or_pos
(assume Hn : n > 0, mul_cancel_left Hn H)
theorem mul_cancel_right {n m k : } (Hm : m > 0) (H : n * m = k * m) : n = k :=
mul_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H)
theorem mul_cancel_right_or {n m k : } (H : n * m = k * m) : m = 0 n = k :=
mul_cancel_left_or (!mul.comm ▸ !mul.comm ▸ H)
theorem mul_eq_one_left {n m : } (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
have H3 : n > 0, from mul_pos_imp_pos_left H2,
have H4 : m > 0, from mul_pos_imp_pos_right H2,
or.elim le_or_gt
(assume H5 : n ≤ 1,
show n = 1, from le_antisym H5 (succ_le_of_lt H3))
(assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le (succ_le_of_lt H5) (succ_le_of_lt H4),
have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
absurd !self_lt_succ (le_imp_not_gt H7))
theorem mul_eq_one_right {n m : } (H : n * m = 1) : m = 1 :=
mul_eq_one_left (!mul.comm ▸ H)
end nat