lean2/library/data/nat/order.lean
2015-07-19 20:21:25 -07:00

584 lines
22 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.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
The order relation on the natural numbers.
-/
import data.nat.basic algebra.ordered_ring
open eq.ops
namespace nat
/- lt and le -/
theorem le_of_lt_or_eq {m n : } (H : m < n m = n) : m ≤ n :=
or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
theorem lt_or_eq_of_le {m n : } (H : m ≤ n) : m < n m = n :=
lt.by_cases
(assume H1 : m < n, or.inl H1)
(assume H1 : m = n, or.inr H1)
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
theorem le_iff_lt_or_eq (m n : ) : m ≤ n ↔ m < n m = n :=
iff.intro lt_or_eq_of_le le_of_lt_or_eq
theorem lt_of_le_and_ne {m n : } (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
or.elim (lt_or_eq_of_le H1)
(take H3 : m < n, H3)
(take H3 : m = n, by contradiction)
theorem lt_iff_le_and_ne (m n : ) : m < n ↔ m ≤ n ∧ m ≠ n :=
iff.intro
(take H, and.intro (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
(take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H))
theorem le_add_right (n k : ) : n ≤ n + k :=
nat.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_of_le ih
... = n + succ k : add_succ)
theorem le_add_left (n m : ): n ≤ m + n :=
!add.comm ▸ !le_add_right
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 :=
by induction h with m h ih;existsi 0; reflexivity;
cases ih with k H; existsi succ k; exact congr_arg succ H
theorem le.total {m n : } : m ≤ n n ≤ m :=
lt.by_cases
(assume H : m < n, or.inl (le_of_lt H))
(assume H : m = n, or.inl (by subst m))
(assume H : m > n, or.inr (le_of_lt H))
/- addition -/
theorem add_le_add_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 : by subst m)
theorem add_le_add_right {n m : } (H : n ≤ m) (k : ) : n + k ≤ m + k :=
!add.comm ▸ !add.comm ▸ add_le_add_left H k
theorem le_of_add_le_add_left {k n m : } (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 lt_of_add_lt_add_left {k n m : } (H : k + n < k + m) : n < m :=
let H' := le_of_lt H in
lt_of_le_and_ne (le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H))
theorem add_lt_add_left {n m : } (H : n < m) (k : ) : k + n < k + m :=
lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k)
theorem add_lt_add_right {n m : } (H : n < m) (k : ) : n + k < m + k :=
!add.comm ▸ !add.comm ▸ add_lt_add_left H k
theorem lt_add_of_pos_right {n k : } (H : k > 0) : n < n + k :=
!add_zero ▸ add_lt_add_left H n
/- multiplication -/
theorem mul_le_mul_left {n m : } (k : ) (H : n ≤ m) : k * n ≤ k * m :=
obtain (l : ) (Hl : n + l = m), from le.elim H,
have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
le.intro H2
theorem mul_le_mul_right {n m : } (k : ) (H : n ≤ m) : n * k ≤ m * k :=
!mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H
theorem mul_le_mul {n m k l : } (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2)
theorem mul_lt_mul_of_pos_left {n m k : } (H : n < m) (Hk : k > 0) : k * n < k * m :=
have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk,
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H),
lt_of_lt_of_le H2 H3
theorem mul_lt_mul_of_pos_right {n m k : } (H : n < m) (Hk : k > 0) : n * k < m * k :=
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
/- min and max -/
-- Because these are defined in init/nat.lean, we cannot use the definitions in algebra.
definition max (a b : ) : := if a < b then b else a
definition min (a b : ) : := if a < b then a else b
theorem max_self [rewrite] (a : ) : max a a = a :=
eq.rec_on !if_t_t rfl
theorem max_le {n m k : } (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k :=
decidable.by_cases
(assume H : n < m, by rewrite [↑max, if_pos H]; apply H₂)
(assume H : ¬ n < m, by rewrite [↑max, if_neg H]; apply H₁)
theorem min_le_left (n m : ) : min n m ≤ n :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H])
(assume H : ¬ n < m,
assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
by rewrite [↑min, if_neg H]; apply H')
theorem min_le_right (n m : ) : min n m ≤ m :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H]; apply le_of_lt H)
(assume H : ¬ n < m,
assert H' : m ≤ n, from or_resolve_right !lt_or_ge H,
by rewrite [↑min, if_neg H])
theorem le_min {n m k : } (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m :=
decidable.by_cases
(assume H : n < m, by rewrite [↑min, if_pos H]; apply H₁)
(assume H : ¬ n < m, by rewrite [↑min, if_neg H]; apply H₂)
theorem eq_max_right {a b : } (H : a < b) : b = max a b :=
(if_pos H)⁻¹
theorem eq_max_left {a b : } (H : ¬ a < b) : a = max a b :=
(if_neg H)⁻¹
open decidable
theorem le_max_right (a b : ) : b ≤ max a b :=
by_cases
(suppose a < b, eq.rec_on (eq_max_right this) !le.refl)
(suppose ¬ a < b, or.rec_on (eq_or_lt_of_not_lt this)
(suppose a = b, eq.rec_on this (eq.rec_on (eq.symm (max_self a)) !le.refl))
(suppose b < a,
have h : a = max a b, from eq_max_left (lt.asymm this),
eq.rec_on h (le_of_lt this)))
theorem le_max_left (a b : ) : a ≤ max a b :=
by_cases
(λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h))
(λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
/- nat is an instance of a linearly ordered semiring and a lattice-/
section migrate_algebra
open [classes] algebra
local attribute nat.comm_semiring [instance]
protected definition linear_ordered_semiring [reducible] :
algebra.linear_ordered_semiring nat :=
⦃ algebra.linear_ordered_semiring, nat.comm_semiring,
add_left_cancel := @add.cancel_left,
add_right_cancel := @add.cancel_right,
lt := lt,
le := le,
le_refl := le.refl,
le_trans := @le.trans,
le_antisymm := @le.antisymm,
le_total := @le.total,
le_iff_lt_or_eq := @le_iff_lt_or_eq,
le_of_lt := @le_of_lt,
lt_irrefl := @lt.irrefl,
lt_of_lt_of_le := @lt_of_lt_of_le,
lt_of_le_of_lt := @lt_of_le_of_lt,
lt_of_add_lt_add_left := @lt_of_add_lt_add_left,
add_lt_add_left := @add_lt_add_left,
add_le_add_left := @add_le_add_left,
le_of_add_le_add_left := @le_of_add_le_add_left,
zero_lt_one := zero_lt_succ 0,
mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1),
mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1),
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄
protected definition lattice [reducible] : algebra.lattice nat :=
⦃ algebra.lattice, nat.linear_ordered_semiring,
min := min,
max := max,
min_le_left := min_le_left,
min_le_right := min_le_right,
le_min := @le_min,
le_max_left := le_max_left,
le_max_right := le_max_right,
max_le := @max_le ⦄
local attribute nat.linear_ordered_semiring [instance]
local attribute nat.lattice [instance]
migrate from algebra with nat
replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max
hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos,
add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right,
mul_lt_mul
attribute le.trans ge.trans lt.trans gt.trans [trans]
attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans]
theorem add_pos_left : ∀{a : }, 0 < a → ∀b : , 0 < a + b :=
take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
theorem add_pos_right : ∀{a : }, 0 < a → ∀b : , 0 < b + a :=
take a H b, !add.comm ▸ add_pos_left H b
theorem add_eq_zero_iff_eq_zero_and_eq_zero : ∀{a b : },
a + b = 0 ↔ a = 0 ∧ b = 0 :=
take a b : ,
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
theorem le_add_of_le_left : ∀{a b c : }, b ≤ c → b ≤ a + c :=
take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
theorem le_add_of_le_right : ∀{a b c : }, b ≤ c → b ≤ c + a :=
take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
theorem lt_add_of_lt_left : ∀{b c : }, b < c → ∀a, b < a + c :=
take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
theorem lt_add_of_lt_right : ∀{b c : }, b < c → ∀a, b < c + a :=
take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
theorem lt_of_mul_lt_mul_left : ∀{a b c : }, c * a < c * b → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
theorem lt_of_mul_lt_mul_right : ∀{a b c : }, a * c < b * c → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
theorem pos_of_mul_pos_left : ∀{a b : }, 0 < a * b → 0 < b :=
take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
theorem pos_of_mul_pos_right : ∀{a b : }, 0 < a * b → 0 < a :=
take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le
end migrate_algebra
theorem zero_le_one : 0 ≤ 1 := dec_trivial
/- properties specific to nat -/
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_succ_add
theorem eq_zero_of_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
/- succ and pred -/
theorem le_of_lt_succ {m n : nat} (H : m < succ n) : m ≤ n :=
le_of_succ_le_succ H
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
iff.rfl
theorem lt_succ_iff_le (m n : nat) : m < succ n ↔ m ≤ n :=
iff.intro le_of_lt_succ lt_succ_of_le
theorem self_le_succ (n : ) : n ≤ succ n :=
le.intro !add_one
theorem succ_le_or_eq_of_le {n m : } (H : n ≤ m) : succ n ≤ m n = m :=
or.elim (lt_or_eq_of_le H)
(assume H1 : n < m, or.inl (succ_le_of_lt H1))
(assume H1 : n = m, or.inr H1)
theorem pred_le_of_le_succ {n m : } : n ≤ succ m → pred n ≤ m :=
nat.cases_on n
(assume H, !pred_zero⁻¹ ▸ zero_le m)
(take n',
assume H : succ n' ≤ succ m,
have H1 : n' ≤ m, from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
theorem succ_le_of_le_pred {n m : } : succ n ≤ m → n ≤ pred m :=
nat.cases_on m
(assume H, absurd H !not_succ_le_zero)
(take m',
assume H : succ n ≤ succ m',
have H1 : n ≤ m', from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
theorem pred_le_pred_of_le {n m : } : n ≤ m → pred n ≤ pred m :=
nat.cases_on n
(assume H, pred_zero⁻¹ ▸ zero_le (pred m))
(take n',
assume H : succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred H)
theorem pre_lt_of_lt : ∀ {n m : }, n < m → pred n < m
| 0 m h := h
| (succ n) m h := lt_of_succ_lt h
theorem lt_of_pred_lt_pred {n m : } (H : pred n < pred m) : n < m :=
lt_of_not_ge
(take H1 : m ≤ n,
not_lt_of_ge (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)
theorem le_pred_self (n : ) : pred n ≤ n :=
nat.cases_on n
(pred_zero⁻¹ ▸ !le.refl)
(take k : , (!pred_succ)⁻¹ ▸ !self_le_succ)
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 (ne_of_lt H)))⁻¹
theorem exists_eq_succ_of_lt {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)
theorem lt_succ_self (n : ) : n < succ n :=
lt.base n
lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
assume Plt, lt.trans Plt (self_lt_succ j)
/- other forms of induction -/
protected definition strong_rec_on {P : nat → Type} (n : ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
have H1 : ∀ {n m : nat}, m < n → P m, from
take n,
nat.rec_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,
assert H2: P n', from H n' @IH,
show ∀m, m < succ n' → P m, from
take m,
assume H3 : m < succ n',
or.by_cases (lt_or_eq_of_le (le_of_lt_succ H3))
(assume H4: m < n', IH H4)
(assume H4: m = n', by subst m; assumption)),
H1 !lt_succ_self
protected theorem strong_induction_on {P : nat → Prop} (n : ) (H : ∀n, (∀m, m < n → P m) → P n) :
P n :=
nat.strong_rec_on n H
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 :=
nat.strong_induction_on a
(take n,
show (∀ m, m < n → P m) → P n, from
nat.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))))
/- pos -/
theorem by_cases_zero_pos {P : → Prop} (y : ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) :
P y :=
nat.cases_on y H0 (take y, H1 !succ_pos)
theorem eq_zero_or_pos (n : ) : n = 0 n > 0 :=
or_of_or_of_imp_left
(or.swap (lt_or_eq_of_le !zero_le))
(take H : 0 = n, by subst n)
theorem pos_of_ne_zero {n : } (H : n ≠ 0) : n > 0 :=
or.elim !eq_zero_or_pos (take H2 : n = 0, by contradiction) (take H2 : n > 0, H2)
theorem ne_zero_of_pos {n : } (H : n > 0) : n ≠ 0 :=
ne.symm (ne_of_lt H)
theorem exists_eq_succ_of_pos {n : } (H : n > 0) : exists l, n = succ l :=
exists_eq_succ_of_lt H
theorem pos_of_dvd_of_pos {m n : } (H1 : m n) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(assume H3 : m = 0,
assert H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
ne_of_lt H2 (by subst n))
/- multiplication -/
theorem mul_lt_mul_of_le_of_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_mul_right m H1) (mul_lt_mul_of_pos_left H2 Hk)
theorem mul_lt_mul_of_lt_of_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_mul_left n H2) (mul_lt_mul_of_pos_right H1 Hl)
theorem mul_lt_mul_of_le_of_le {n m k l : } (H1 : n < k) (H2 : m < l) : n * m < k * l :=
have H3 : n * m ≤ k * m, from mul_le_mul_right m (le_of_lt H1),
have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le H1),
lt_of_le_of_lt H3 H4
theorem eq_of_mul_eq_mul_left {m k n : } (Hn : n > 0) (H : n * m = n * k) : m = k :=
have n * m ≤ n * k, by rewrite H,
have h : m ≤ k, from le_of_mul_le_mul_left this Hn,
have n * k ≤ n * m, by rewrite H,
have k ≤ m, from le_of_mul_le_mul_left this Hn,
le.antisymm h this
theorem eq_of_mul_eq_mul_right {n m k : } (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : } (H : n * m = n * k) : n = 0 m = k :=
or_of_or_of_imp_right !eq_zero_or_pos
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
theorem eq_zero_or_eq_of_mul_eq_mul_right {n m k : } (H : n * m = k * m) : m = 0 n = k :=
eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
theorem eq_one_of_mul_eq_one_right {n m : } (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, by rewrite H; apply succ_pos,
or.elim (le_or_gt n 1)
(assume H5 : n ≤ 1,
have n > 0, from pos_of_mul_pos_right H2,
show n = 1, from le.antisymm H5 (succ_le_of_lt this))
(assume H5 : n > 1,
have m > 0, from pos_of_mul_pos_left H2,
have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt this),
have 1 ≥ 2, from !mul_one ▸ H ▸ this,
absurd !lt_succ_self (not_lt_of_ge this))
theorem eq_one_of_mul_eq_one_left {n m : } (H : n * m = 1) : m = 1 :=
eq_one_of_mul_eq_one_right (!mul.comm ▸ H)
theorem eq_one_of_mul_eq_self_left {n m : } (Hpos : n > 0) (H : m * n = n) : m = 1 :=
eq_of_mul_eq_mul_right Hpos (H ⬝ !one_mul⁻¹)
theorem eq_one_of_mul_eq_self_right {n m : } (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
theorem eq_one_of_dvd_one {n : } (H : n 1) : n = 1 :=
dvd.elim H
(take m,
assume H1 : 1 = n * m,
eq_one_of_mul_eq_one_right H1⁻¹)
/- min and max -/
open decidable
theorem le_max_left_iff_true [rewrite] (a b : ) : a ≤ max a b ↔ true :=
iff_true_intro (le_max_left a b)
theorem le_max_right_iff_true [rewrite] (a b : ) : b ≤ max a b ↔ true :=
iff_true_intro (le_max_right a b)
theorem min_zero [rewrite] (a : ) : min a 0 = 0 :=
by rewrite [min_eq_right !zero_le]
theorem zero_min [rewrite] (a : ) : min 0 a = 0 :=
by rewrite [min_eq_left !zero_le]
theorem max_zero [rewrite] (a : ) : max a 0 = a :=
by rewrite [max_eq_left !zero_le]
theorem zero_max [rewrite] (a : ) : max 0 a = a :=
by rewrite [max_eq_right !zero_le]
theorem min_succ_succ [rewrite] (a b : ) : min (succ a) (succ b) = succ (min a b) :=
by_cases
(suppose a < b, by unfold min; rewrite [if_pos this, if_pos (succ_lt_succ this)])
(suppose ¬ a < b,
assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold min; rewrite [if_neg this, if_neg h])
theorem max_succ_succ [rewrite] (a b : ) : max (succ a) (succ b) = succ (max a b) :=
by_cases
(suppose a < b, by unfold max; rewrite [if_pos this, if_pos (succ_lt_succ this)])
(suppose ¬ a < b,
assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this,
by unfold max; rewrite [if_neg this, if_neg h])
theorem lt_min {a b c : } (H₁ : a < b) (H₂ : a < c) : a < min b c :=
decidable.by_cases
(assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁)
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
by rewrite (min_eq_right H'); apply H₂)
theorem max_lt {a b c : } (H₁ : a < c) (H₂ : b < c) : max a b < c :=
decidable.by_cases
(assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
(assume H : ¬ a ≤ b,
assert H' : b ≤ a, from le_of_lt (lt_of_not_ge H),
by rewrite (max_eq_left H'); apply H₁)
theorem min_add_add_left (a b c : ) : min (a + b) (a + c) = a + min b c :=
decidable.by_cases
(assume H : b ≤ c,
assert H1 : a + b ≤ a + c, from add_le_add_left H _,
by rewrite [min_eq_left H, min_eq_left H1])
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
assert H1 : a + c ≤ a + b, from add_le_add_left H' _,
by rewrite [min_eq_right H', min_eq_right H1])
theorem min_add_add_right (a b c : ) : min (a + c) (b + c) = min a b + c :=
by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply min_add_add_left
theorem max_add_add_left (a b c : ) : max (a + b) (a + c) = a + max b c :=
decidable.by_cases
(assume H : b ≤ c,
assert H1 : a + b ≤ a + c, from add_le_add_left H _,
by rewrite [max_eq_right H, max_eq_right H1])
(assume H : ¬ b ≤ c,
assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H),
assert H1 : a + c ≤ a + b, from add_le_add_left H' _,
by rewrite [max_eq_left H', max_eq_left H1])
theorem max_add_add_right (a b c : ) : max (a + c) (b + c) = max a b + c :=
by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left
theorem max_eq_right' {a b : } (H : a < b) : max a b = b :=
if_pos H
-- different versions will be defined in algebra
theorem max_eq_left' {a b : } (H : ¬ a < b) : max a b = a :=
if_neg H
/- greatest -/
section greatest
variable (P : → Prop)
variable [decP : ∀ n, decidable (P n)]
include decP
-- returns the largest i < n satisfying P, or n if there is none.
definition greatest :
| 0 := 0
| (succ n) := if P n then n else greatest n
theorem greatest_of_lt {i n : } (ltin : i < n) (Hi : P i) : P (greatest P n) :=
begin
induction n with [m, ih],
{exact absurd ltin !not_lt_zero},
{cases (decidable.em (P m)) with [Psm, Pnsm],
{rewrite [↑greatest, if_pos Psm]; exact Psm},
{rewrite [↑greatest, if_neg Pnsm],
have neim : i ≠ m, from assume H : i = m, absurd (H ▸ Hi) Pnsm,
have ltim : i < m, from lt_of_le_of_ne (le_of_lt_succ ltin) neim,
apply ih ltim}}
end
theorem le_greatest_of_lt {i n : } (ltin : i < n) (Hi : P i) : i ≤ greatest P n :=
begin
induction n with [m, ih],
{exact absurd ltin !not_lt_zero},
{cases (decidable.em (P m)) with [Psm, Pnsm],
{rewrite [↑greatest, if_pos Psm], apply le_of_lt_succ ltin},
{rewrite [↑greatest, if_neg Pnsm],
have neim : i ≠ m, from assume H : i = m, absurd (H ▸ Hi) Pnsm,
have ltim : i < m, from lt_of_le_of_ne (le_of_lt_succ ltin) neim,
apply ih ltim}}
end
end greatest
end nat