2015-01-07 01:44:04 +00:00
|
|
|
|
/-
|
|
|
|
|
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
|
2014-08-22 23:36:47 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
The order relation on the natural numbers.
|
|
|
|
|
-/
|
2015-02-01 14:55:12 +00:00
|
|
|
|
import data.nat.basic algebra.ordered_ring
|
2014-11-22 08:15:51 +00:00
|
|
|
|
open eq.ops
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
namespace nat
|
2015-05-12 12:49:05 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- lt and le -/
|
2015-05-12 12:49:05 +00:00
|
|
|
|
|
2015-05-09 19:15:30 +00:00
|
|
|
|
theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
|
2015-01-08 02:26:51 +00:00
|
|
|
|
or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-05-09 19:15:30 +00:00
|
|
|
|
theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n :=
|
2015-01-07 01:44:04 +00:00
|
|
|
|
lt.by_cases
|
|
|
|
|
(assume H1 : m < n, or.inl H1)
|
|
|
|
|
(assume H1 : m = n, or.inr H1)
|
2015-01-08 02:26:51 +00:00
|
|
|
|
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
2015-05-09 19:15:30 +00:00
|
|
|
|
theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
|
2015-01-07 01:44:04 +00:00
|
|
|
|
or.elim (lt_or_eq_of_le H1)
|
|
|
|
|
(take H3 : m < n, H3)
|
2015-05-26 01:14:52 +00:00
|
|
|
|
(take H3 : m = n, by contradiction)
|
2014-12-26 21:25:05 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n :=
|
|
|
|
|
iff.intro
|
2015-01-08 02:26:51 +00:00
|
|
|
|
(take H, and.intro (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem le_add_right (n k : ℕ) : n ≤ n + k :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on k
|
2014-11-22 08:15:51 +00:00
|
|
|
|
(calc n ≤ n : le.refl n
|
2014-12-24 02:14:19 +00:00
|
|
|
|
... = n + zero : add_zero)
|
2014-11-22 08:15:51 +00:00
|
|
|
|
(λ k (ih : n ≤ n + k), calc
|
2015-01-07 01:44:04 +00:00
|
|
|
|
n ≤ succ (n + k) : le_succ_of_le ih
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = n + succ k : add_succ)
|
2014-11-22 08:15:51 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2014-11-22 08:15:51 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem le.elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
|
2015-06-04 23:16:28 +00:00
|
|
|
|
by induction h with m h ih;existsi 0; reflexivity;
|
|
|
|
|
cases ih with k H; existsi succ k; exact congr_arg succ H
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
|
|
|
|
|
lt.by_cases
|
2015-01-08 02:26:51 +00:00
|
|
|
|
(assume H : m < n, or.inl (le_of_lt H))
|
2015-05-26 01:14:52 +00:00
|
|
|
|
(assume H : m = n, or.inl (by subst m))
|
2015-01-08 02:26:51 +00:00
|
|
|
|
(assume H : m > n, or.inr (le_of_lt H))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- addition -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(calc
|
2015-05-26 01:14:52 +00:00
|
|
|
|
k + n + l = k + (n + l) : add.assoc
|
|
|
|
|
... = k + m : by subst m)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(calc
|
2015-05-26 01:14:52 +00:00
|
|
|
|
k + (n + l) = k + n + l : add.assoc
|
2014-08-27 01:47:36 +00:00
|
|
|
|
... = k + m : Hl))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-05-29 03:34:57 +00:00
|
|
|
|
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))
|
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k :=
|
|
|
|
|
!add_zero ▸ add_lt_add_left H n
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- multiplication -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-05-30 12:09:34 +00:00
|
|
|
|
theorem mul_le_mul_left {n m : ℕ} (k : ℕ) (H : n ≤ m) : k * n ≤ k * m :=
|
2015-01-07 01:44:04 +00:00
|
|
|
|
obtain (l : ℕ) (Hl : n + l = m), from le.elim H,
|
2015-03-28 00:26:06 +00:00
|
|
|
|
have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
|
2015-01-07 01:44:04 +00:00
|
|
|
|
le.intro H2
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-05-30 12:09:34 +00:00
|
|
|
|
theorem mul_le_mul_right {n m : ℕ} (k : ℕ) (H : n ≤ m) : n * k ≤ m * k :=
|
|
|
|
|
!mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
|
2015-05-30 12:09:34 +00:00
|
|
|
|
le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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,
|
2015-05-30 12:09:34 +00:00
|
|
|
|
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H),
|
2015-01-08 02:26:51 +00:00
|
|
|
|
lt_of_lt_of_le H2 H3
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
/- min and max -/
|
|
|
|
|
|
|
|
|
|
-- Because these are defined in init/nat.lean, we cannot use the definitions in algebra.
|
|
|
|
|
|
2015-07-20 02:47:14 +00:00
|
|
|
|
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
|
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
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₂)
|
|
|
|
|
|
2015-07-20 02:47:14 +00:00
|
|
|
|
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)
|
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
/- nat is an instance of a linearly ordered semiring and a lattice-/
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-05-12 12:49:05 +00:00
|
|
|
|
section migrate_algebra
|
2015-01-07 01:44:04 +00:00
|
|
|
|
open [classes] algebra
|
2015-05-12 04:44:31 +00:00
|
|
|
|
local attribute nat.comm_semiring [instance]
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-05-12 04:44:31 +00:00
|
|
|
|
protected definition linear_ordered_semiring [reducible] :
|
2015-01-26 17:01:19 +00:00
|
|
|
|
algebra.linear_ordered_semiring nat :=
|
2015-01-20 01:39:59 +00:00
|
|
|
|
⦃ 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,
|
2015-05-29 03:34:57 +00:00
|
|
|
|
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,
|
2015-01-20 01:39:59 +00:00
|
|
|
|
add_le_add_left := @add_le_add_left,
|
|
|
|
|
le_of_add_le_add_left := @le_of_add_le_add_left,
|
2015-07-08 00:13:56 +00:00
|
|
|
|
zero_lt_one := zero_lt_succ 0,
|
2015-05-30 12:09:34 +00:00
|
|
|
|
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),
|
2015-01-20 01:39:59 +00:00
|
|
|
|
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
|
|
|
|
|
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄
|
2015-05-12 04:44:31 +00:00
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
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 ⦄
|
|
|
|
|
|
2015-05-12 04:44:31 +00:00
|
|
|
|
local attribute nat.linear_ordered_semiring [instance]
|
2015-06-29 02:09:31 +00:00
|
|
|
|
local attribute nat.lattice [instance]
|
2015-03-15 03:32:39 +00:00
|
|
|
|
|
|
|
|
|
migrate from algebra with nat
|
2015-06-29 02:09:31 +00:00
|
|
|
|
replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max
|
2015-05-12 12:49:05 +00:00
|
|
|
|
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,
|
2015-05-25 09:10:17 +00:00
|
|
|
|
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
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-05-23 05:38:42 +00:00
|
|
|
|
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]
|
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2015-05-12 12:49:05 +00:00
|
|
|
|
end migrate_algebra
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
|
|
|
|
theorem zero_le_one : 0 ≤ 1 := dec_trivial
|
|
|
|
|
|
|
|
|
|
/- properties specific to nat -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
|
2015-01-07 01:44:04 +00:00
|
|
|
|
lt_of_succ_le (le.intro H)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem lt_elim {n m : ℕ} (H : n < m) : ∃k, succ n + k = m :=
|
|
|
|
|
le.elim (succ_le_of_lt H)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
theorem lt_add_succ (n m : ℕ) : n < n + succ m :=
|
2015-02-25 18:32:50 +00:00
|
|
|
|
lt_intro !succ_add_eq_succ_add
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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 -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-06-04 23:57:56 +00:00
|
|
|
|
theorem le_of_lt_succ {m n : nat} (H : m < succ n) : m ≤ n :=
|
|
|
|
|
le_of_succ_le_succ H
|
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
|
2015-06-04 23:57:56 +00:00
|
|
|
|
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
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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
|
2015-01-07 01:54:15 +00:00
|
|
|
|
(assume H, !pred_zero⁻¹ ▸ zero_le m)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(take n',
|
|
|
|
|
assume H : succ n' ≤ succ m,
|
|
|
|
|
have H1 : n' ≤ m, from le_of_succ_le_succ H,
|
2015-01-07 01:54:15 +00:00
|
|
|
|
!pred_succ⁻¹ ▸ H1)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
|
|
|
|
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,
|
2015-01-07 01:54:15 +00:00
|
|
|
|
!pred_succ⁻¹ ▸ H1)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
|
|
|
|
theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
|
|
|
|
|
nat.cases_on n
|
2015-01-07 01:54:15 +00:00
|
|
|
|
(assume H, pred_zero⁻¹ ▸ zero_le (pred m))
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(take n',
|
|
|
|
|
assume H : succ n' ≤ m,
|
2015-01-07 01:54:15 +00:00
|
|
|
|
!pred_succ⁻¹ ▸ succ_le_of_le_pred H)
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-06-03 05:08:25 +00:00
|
|
|
|
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
|
|
|
|
|
|
2015-01-12 21:28:42 +00:00
|
|
|
|
theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m :=
|
2015-05-25 09:48:07 +00:00
|
|
|
|
lt_of_not_ge
|
2015-01-12 21:28:42 +00:00
|
|
|
|
(take H1 : m ≤ n,
|
2015-05-25 09:48:07 +00:00
|
|
|
|
not_lt_of_ge (pred_le_pred_of_le H1) H)
|
2015-01-12 21:28:42 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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 :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.cases_on n
|
2015-01-07 01:54:15 +00:00
|
|
|
|
(pred_zero⁻¹ ▸ !le.refl)
|
|
|
|
|
(take k : ℕ, (!pred_succ)⁻¹ ▸ !self_le_succ)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-11-22 08:15:51 +00:00
|
|
|
|
theorem succ_pos (n : ℕ) : 0 < succ n :=
|
|
|
|
|
!zero_lt_succ
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-17 18:32:38 +00:00
|
|
|
|
theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n :=
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(or_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹
|
2014-12-17 18:32:38 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : exists k, m = succ k :=
|
2014-08-02 01:40:24 +00:00
|
|
|
|
discriminate
|
2014-10-05 18:36:39 +00:00
|
|
|
|
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
|
2014-12-16 03:05:03 +00:00
|
|
|
|
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-02-25 18:32:50 +00:00
|
|
|
|
theorem lt_succ_self (n : ℕ) : n < succ n :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
lt.base n
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-13 21:51:35 +00:00
|
|
|
|
lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
|
|
|
|
|
assume Plt, lt.trans Plt (self_lt_succ j)
|
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- other forms of induction -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-15 19:49:47 +00:00
|
|
|
|
protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
|
2014-08-27 01:47:36 +00:00
|
|
|
|
have H1 : ∀ {n m : nat}, m < n → P m, from
|
2014-08-02 02:29:50 +00:00
|
|
|
|
take n,
|
2015-07-15 19:49:47 +00:00
|
|
|
|
nat.rec_on n
|
2014-10-05 18:36:39 +00:00
|
|
|
|
(show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(take n',
|
2014-08-27 01:47:36 +00:00
|
|
|
|
assume IH : ∀ {m : nat}, m < n' → P m,
|
2015-05-26 01:14:52 +00:00
|
|
|
|
assert H2: P n', from H n' @IH,
|
2014-08-02 02:29:50 +00:00
|
|
|
|
show ∀m, m < succ n' → P m, from
|
2014-08-03 03:04:27 +00:00
|
|
|
|
take m,
|
|
|
|
|
assume H3 : m < succ n',
|
2015-07-15 19:49:47 +00:00
|
|
|
|
or.by_cases (lt_or_eq_of_le (le_of_lt_succ H3))
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(assume H4: m < n', IH H4)
|
2015-05-26 01:14:52 +00:00
|
|
|
|
(assume H4: m = n', by subst m; assumption)),
|
2015-02-25 18:32:50 +00:00
|
|
|
|
H1 !lt_succ_self
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-15 19:49:47 +00:00
|
|
|
|
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
|
|
|
|
|
|
2014-09-19 22:04:52 +00:00
|
|
|
|
protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
|
2015-05-19 05:35:18 +00:00
|
|
|
|
nat.strong_induction_on a
|
|
|
|
|
(take n,
|
|
|
|
|
show (∀ m, m < n → P m) → P n, from
|
|
|
|
|
nat.cases_on n
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(assume H : (∀m, m < 0 → P m), show P 0, from H0)
|
|
|
|
|
(take n,
|
2014-08-03 03:04:27 +00:00
|
|
|
|
assume H : (∀m, m < succ n → P m),
|
|
|
|
|
show P (succ n), from
|
2014-11-30 23:07:09 +00:00
|
|
|
|
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- pos -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-05-25 12:13:23 +00:00
|
|
|
|
theorem by_cases_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) :
|
|
|
|
|
P y :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.cases_on y H0 (take y, H1 !succ_pos)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-02-01 02:53:47 +00:00
|
|
|
|
theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 :=
|
2014-12-15 20:05:44 +00:00
|
|
|
|
or_of_or_of_imp_left
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(or.swap (lt_or_eq_of_le !zero_le))
|
2015-05-26 01:14:52 +00:00
|
|
|
|
(take H : 0 = n, by subst n)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
2015-05-26 01:14:52 +00:00
|
|
|
|
or.elim !eq_zero_or_pos (take H2 : n = 0, by contradiction) (take H2 : n > 0, H2)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem ne_zero_of_pos {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
|
|
|
|
ne.symm (ne_of_lt H)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem exists_eq_succ_of_pos {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
|
|
|
|
exists_eq_succ_of_lt H
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-04-06 16:24:09 +00:00
|
|
|
|
theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 :=
|
2015-02-01 02:53:47 +00:00
|
|
|
|
pos_of_ne_zero
|
|
|
|
|
(assume H3 : m = 0,
|
2015-05-26 01:14:52 +00:00
|
|
|
|
assert H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
|
|
|
|
|
ne_of_lt H2 (by subst n))
|
2015-02-01 02:53:47 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
/- multiplication -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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 :=
|
2015-05-30 12:09:34 +00:00
|
|
|
|
lt_of_le_of_lt (mul_le_mul_right m H1) (mul_lt_mul_of_pos_left H2 Hk)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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 :=
|
2015-05-30 12:09:34 +00:00
|
|
|
|
lt_of_le_of_lt (mul_le_mul_left n H2) (mul_lt_mul_of_pos_right H1 Hl)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem mul_lt_mul_of_le_of_le {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
|
2015-05-30 12:09:34 +00:00
|
|
|
|
have H3 : n * m ≤ k * m, from mul_le_mul_right m (le_of_lt H1),
|
2015-01-08 02:26:51 +00:00
|
|
|
|
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
|
2014-08-02 02:29:50 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
|
2015-07-18 18:36:05 +00:00
|
|
|
|
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
|
2015-01-07 01:44:04 +00:00
|
|
|
|
|
2015-01-13 16:56:25 +00:00
|
|
|
|
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)
|
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
theorem eq_zero_or_eq_of_mul_eq_mul_left {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k :=
|
2015-02-01 02:53:47 +00:00
|
|
|
|
or_of_or_of_imp_right !eq_zero_or_pos
|
2015-01-07 01:44:04 +00:00
|
|
|
|
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
|
2015-01-07 01:44:04 +00:00
|
|
|
|
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)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
|
2015-01-13 16:56:25 +00:00
|
|
|
|
theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
|
2015-05-26 01:14:52 +00:00
|
|
|
|
have H2 : n * m > 0, by rewrite H; apply succ_pos,
|
2015-01-07 01:44:04 +00:00
|
|
|
|
or.elim (le_or_gt n 1)
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(assume H5 : n ≤ 1,
|
2015-07-18 18:36:05 +00:00
|
|
|
|
have n > 0, from pos_of_mul_pos_right H2,
|
|
|
|
|
show n = 1, from le.antisymm H5 (succ_le_of_lt this))
|
2014-08-02 02:29:50 +00:00
|
|
|
|
(assume H5 : n > 1,
|
2015-07-18 18:36:05 +00:00
|
|
|
|
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))
|
2014-08-02 02:29:50 +00:00
|
|
|
|
|
2015-01-13 16:56:25 +00:00
|
|
|
|
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)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-04-06 16:24:09 +00:00
|
|
|
|
theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 :=
|
2015-02-03 17:29:52 +00:00
|
|
|
|
dvd.elim H
|
|
|
|
|
(take m,
|
|
|
|
|
assume H1 : 1 = n * m,
|
|
|
|
|
eq_one_of_mul_eq_one_right H1⁻¹)
|
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
/- min and max -/
|
2015-07-20 02:47:14 +00:00
|
|
|
|
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]
|
2015-06-29 02:09:31 +00:00
|
|
|
|
|
2015-07-20 03:14:49 +00:00
|
|
|
|
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])
|
|
|
|
|
|
2015-06-29 02:09:31 +00:00
|
|
|
|
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₁)
|
|
|
|
|
|
2015-06-29 04:07:41 +00:00
|
|
|
|
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
|
|
|
|
|
|
2015-07-07 23:54:21 +00:00
|
|
|
|
/- 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
|
|
|
|
|
|
2014-08-20 02:32:44 +00:00
|
|
|
|
end nat
|