lean2/library/init/nat.lean

292 lines
9.8 KiB
Text
Raw Normal View History

2014-12-01 04:34:12 +00:00
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura
-/
prelude
2015-03-03 21:37:38 +00:00
import init.wf init.tactic init.num
open eq.ops decidable or
namespace nat
notation `` := nat
/- basic definitions on natural numbers -/
inductive le (a : ) : → Prop :=
| refl : le a a
| step : Π {b}, le a b → le a (succ b)
infix `≤` := le
attribute le.refl [refl]
definition lt [reducible] (n m : ) := succ n ≤ m
definition ge [reducible] (n m : ) := m ≤ n
definition gt [reducible] (n m : ) := succ m ≤ n
infix `<` := lt
infix `≥` := ge
infix `>` := gt
definition pred [unfold 1] (a : nat) : nat :=
nat.cases_on a zero (λ a₁, a₁)
-- add is defined in init.num
definition sub (a b : nat) : nat :=
nat.rec_on b a (λ b₁ r, pred r)
definition mul (a b : nat) : nat :=
nat.rec_on b zero (λ b₁ r, r + a)
notation a - b := sub a b
notation a * b := mul a b
/- properties of -/
protected definition is_inhabited [instance] : inhabited nat :=
inhabited.mk zero
protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
| has_decidable_eq zero zero := inl rfl
| has_decidable_eq (succ x) zero := inr (by contradiction)
| has_decidable_eq zero (succ y) := inr (by contradiction)
| has_decidable_eq (succ x) (succ y) :=
match has_decidable_eq x y with
| inl xeqy := inl (by rewrite xeqy)
| inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney)
end
/- properties of inequality -/
theorem le_of_eq {n m : } (p : n = m) : n ≤ m := p ▸ le.refl n
theorem le_succ (n : ) : n ≤ succ n := by repeat constructor
theorem pred_le (n : ) : pred n ≤ n := by cases n;all_goals (repeat constructor)
theorem le_succ_iff_true [rewrite] (n : ) : n ≤ succ n ↔ true :=
iff_true_intro (le_succ n)
theorem pred_le_iff_true [rewrite] (n : ) : pred n ≤ n ↔ true :=
iff_true_intro (pred_le n)
theorem le.trans [trans] {n m k : } (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
by induction H2 with n H2 IH;exact H1;exact le.step IH
theorem le_succ_of_le {n m : } (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ
theorem le_of_succ_le {n m : } (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H
theorem le_of_lt {n m : } (H : n < m) : n ≤ m := le_of_succ_le H
theorem succ_le_succ {n m : } (H : n ≤ m) : succ n ≤ succ m :=
by induction H;reflexivity;exact le.step v_0
theorem pred_le_pred {n m : } (H : n ≤ m) : pred n ≤ pred m :=
by induction H;reflexivity;cases b;exact v_0;exact le.step v_0
theorem le_of_succ_le_succ {n m : } (H : succ n ≤ succ m) : n ≤ m :=
pred_le_pred H
theorem le_succ_of_pred_le {n m : } (H : pred n ≤ m) : n ≤ succ m :=
by cases n;exact le.step H;exact succ_le_succ H
theorem not_succ_le_self {n : } : ¬succ n ≤ n :=
by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a
theorem succ_le_self_iff_false [rewrite] (n : ) : succ n ≤ n ↔ false :=
iff_false_intro not_succ_le_self
theorem zero_le (n : ) : 0 ≤ n :=
by induction n with n IH;apply le.refl;exact le.step IH
theorem zero_le_iff_true [rewrite] (n : ) : 0 ≤ n ↔ true :=
iff_true_intro (zero_le n)
theorem lt.step {n m : } (H : n < m) : n < succ m :=
le.step H
theorem zero_lt_succ (n : ) : 0 < succ n :=
by induction n with n IH;apply le.refl;exact le.step IH
theorem zero_lt_succ_iff_true [rewrite] (n : ) : 0 < succ n ↔ true :=
iff_true_intro (zero_lt_succ n)
theorem lt.trans [trans] {n m k : } (H1 : n < m) (H2 : m < k) : n < k :=
le.trans (le.step H1) H2
theorem lt_of_le_of_lt [trans] {n m k : } (H1 : n ≤ m) (H2 : m < k) : n < k :=
le.trans (succ_le_succ H1) H2
theorem lt_of_lt_of_le [trans] {n m k : } (H1 : n < m) (H2 : m ≤ k) : n < k :=
le.trans H1 H2
theorem le.antisymm {n m : } (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
begin
cases H1 with m' H1',
{ reflexivity},
{ cases H2 with n' H2',
{ reflexivity},
{ exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}},
end
theorem not_succ_le_zero (n : ) : ¬succ n ≤ zero :=
by intro H; cases H
theorem succ_le_zero_iff_false (n : ) : succ n ≤ zero ↔ false :=
iff_false_intro (not_succ_le_zero n)
theorem lt.irrefl (n : ) : ¬n < n := not_succ_le_self
theorem lt_self_iff_false [rewrite] (n : ) : n < n ↔ false :=
iff_false_intro (lt.irrefl n)
theorem self_lt_succ (n : ) : n < succ n := !le.refl
theorem self_lt_succ_iff_true [rewrite] (n : ) : n < succ n ↔ true :=
iff_true_intro (self_lt_succ n)
theorem lt.base (n : ) : n < succ n := !le.refl
theorem le_lt_antisymm {n m : } (H1 : n ≤ m) (H2 : m < n) : false :=
!lt.irrefl (lt_of_le_of_lt H1 H2)
theorem lt_le_antisymm {n m : } (H1 : n < m) (H2 : m ≤ n) : false :=
le_lt_antisymm H2 H1
theorem lt.asymm {n m : } (H1 : n < m) (H2 : m < n) : false :=
le_lt_antisymm (le_of_lt H1) H2
definition lt.by_cases {a b : } {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
begin
revert b H1 H2 H3, induction a with a IH,
{ intros, cases b,
exact H2 rfl,
exact H1 !zero_lt_succ},
{ intros, cases b with b,
exact H3 !zero_lt_succ,
{ apply IH,
intro H, exact H1 (succ_le_succ H),
intro H, exact H2 (congr rfl H),
intro H, exact H3 (succ_le_succ H)}}
end
theorem lt.trichotomy (a b : ) : a < b a = b b < a :=
lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H))
theorem lt_ge_by_cases {a b : } {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
lt.by_cases H1 (λH, H2 (le_of_eq H⁻¹)) (λH, H2 (le_of_lt H))
theorem lt_or_ge (a b : ) : (a < b) (a ≥ b) :=
lt_ge_by_cases inl inr
theorem not_lt_zero (a : ) : ¬ a < zero :=
by intro H; cases H
theorem lt_zero_iff_false [rewrite] (a : ) : a < zero ↔ false :=
iff_false_intro (not_lt_zero a)
-- less-than is well-founded
definition lt.wf [instance] : well_founded lt :=
begin
constructor, intro n, induction n with n IH,
{ constructor, intros n H, exfalso, exact !not_lt_zero H},
{ constructor, intros m H,
assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m,
{ intros n₁ hlt, induction hlt,
{ intro p, injection p with q, exact q ▸ IH},
{ intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}},
apply aux H rfl},
end
definition measure {A : Type} (f : A → ) : A → A → Prop :=
inv_image lt f
definition measure.wf {A : Type} (f : A → ) : well_founded (measure f) :=
inv_image.wf f lt.wf
theorem succ_lt_succ {a b : } (H : a < b) : succ a < succ b :=
succ_le_succ H
theorem lt_of_succ_lt {a b : } (H : succ a < b) : a < b :=
le_of_succ_le H
theorem lt_of_succ_lt_succ {a b : } (H : succ a < succ b) : a < b :=
le_of_succ_le_succ H
definition decidable_le [instance] : decidable_rel le :=
begin
intros n, induction n with n IH,
{ intro m, left, apply zero_le},
{ intro m, cases m with m,
{ right, apply not_succ_le_zero},
{ let H := IH m, clear IH,
cases H with H H,
left, exact succ_le_succ H,
right, intro H2, exact H (le_of_succ_le_succ H2)}}
end
definition decidable_lt [instance] : decidable_rel lt := _
definition decidable_gt [instance] : decidable_rel gt := _
definition decidable_ge [instance] : decidable_rel ge := _
theorem eq_or_lt_of_le {a b : } (H : a ≤ b) : a = b a < b :=
by cases H with b' H; exact inl rfl; exact inr (succ_le_succ H)
theorem le_of_eq_or_lt {a b : } (H : a = b a < b) : a ≤ b :=
by cases H with H H; exact le_of_eq H; exact le_of_lt H
theorem eq_or_lt_of_not_lt {a b : } (hnlt : ¬ a < b) : a = b b < a :=
or.rec_on (lt.trichotomy a b)
(λ hlt, absurd hlt hnlt)
(λ h, h)
theorem lt_succ_of_le {a b : } (h : a ≤ b) : a < succ b :=
succ_le_succ h
theorem lt_of_succ_le {a b : } (h : succ a ≤ b) : a < b := h
theorem succ_le_of_lt {a b : } (h : a < b) : succ a ≤ b := h
theorem succ_sub_succ_eq_sub [rewrite] (a b : ) : succ a - succ b = a - b :=
by induction b with b IH;reflexivity; apply congr (eq.refl pred) IH
theorem sub_eq_succ_sub_succ (a b : ) : a - b = succ a - succ b :=
eq.rec_on (succ_sub_succ_eq_sub a b) rfl
theorem zero_sub_eq_zero [rewrite] (a : ) : zero - a = zero :=
nat.rec_on a
rfl
(λ a₁ (ih : zero - a₁ = zero), congr (eq.refl pred) ih)
theorem zero_eq_zero_sub (a : ) : zero = zero - a :=
eq.rec_on (zero_sub_eq_zero a) rfl
theorem sub_lt {a b : } : zero < a → zero < b → a - b < a :=
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
λa h₁, le.rec_on h₁
(λb h₂, le.cases_on h₂
(lt.base zero)
(λ b₁ bpos,
eq.rec_on (sub_eq_succ_sub_succ zero b₁)
(eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
(λa₁ apos ih b h₂, le.cases_on h₂
(lt.base a₁)
(λ b₁ bpos,
eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
(lt.trans (@ih b₁ bpos) (lt.base a₁)))),
λ h₁ h₂, aux h₁ h₂
theorem sub_le (a b : ) : a - b ≤ a :=
nat.rec_on b
(le.refl a)
(λ b₁ ih, le.trans !pred_le ih)
theorem sub_le_iff_true [rewrite] (a b : ) : a - b ≤ a ↔ true :=
iff_true_intro (sub_le a b)
theorem sub_lt_succ (a b : ) : a - b < succ a :=
lt_succ_of_le (sub_le a b)
theorem sub_lt_succ_iff_true [rewrite] (a b : ) : a - b < succ a ↔ true :=
iff_true_intro (sub_lt_succ a b)
end nat