160 lines
4.8 KiB
Text
160 lines
4.8 KiB
Text
/-
|
||
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
|
||
import init.core
|
||
|
||
notation `ℕ` := Nat
|
||
|
||
namespace Nat
|
||
|
||
inductive lessThanOrEqual (a : ℕ) : ℕ → Prop
|
||
| refl : lessThanOrEqual a
|
||
| step : Π {b}, lessThanOrEqual b → lessThanOrEqual (succ b)
|
||
|
||
@[elabAsEliminator]
|
||
theorem lessThanOrEqual.ndrec {a : Nat} {C : Nat → Prop} (m₁ : C a) (m₂ : ∀ (b : Nat), lessThanOrEqual a b → C b → C (succ b)) {b : ℕ} (h : lessThanOrEqual a b) : C b :=
|
||
@lessThanOrEqual.rec a (fun b _ => C b) m₁ m₂ b h
|
||
|
||
@[elabAsEliminator]
|
||
theorem lessThanOrEqual.ndrecOn {a : Nat} {C : Nat → Prop} {b : ℕ} (h : lessThanOrEqual a b) (m₁ : C a) (m₂ : ∀ (b : Nat), lessThanOrEqual a b → C b → C (succ b)) : C b :=
|
||
@lessThanOrEqual.rec a (fun b _ => C b) m₁ m₂ b h
|
||
|
||
instance : HasLessEq ℕ :=
|
||
⟨Nat.lessThanOrEqual⟩
|
||
|
||
@[reducible] protected def le (n m : ℕ) := Nat.lessThanOrEqual n m
|
||
@[reducible] protected def lt (n m : ℕ) := Nat.lessThanOrEqual (succ n) m
|
||
|
||
set_option codegen false
|
||
|
||
|
||
instance : HasLess ℕ :=
|
||
⟨Nat.lt⟩
|
||
|
||
def pred : ℕ → ℕ
|
||
| 0 := 0
|
||
| (a+1) := a
|
||
|
||
protected def sub : ℕ → ℕ → ℕ
|
||
| a 0 := a
|
||
| a (b+1) := pred (sub a b)
|
||
|
||
protected def mul : Nat → Nat → Nat
|
||
| a 0 := 0
|
||
| a (b+1) := (mul a b) + a
|
||
|
||
instance : HasSub ℕ :=
|
||
⟨Nat.sub⟩
|
||
|
||
instance : HasMul ℕ :=
|
||
⟨Nat.mul⟩
|
||
|
||
def hasDecEq : Π a b : Nat, Decidable (a = b)
|
||
| zero zero := isTrue rfl
|
||
| (succ x) zero := isFalse (fun h => Nat.noConfusion h)
|
||
| zero (succ y) := isFalse (fun h => Nat.noConfusion h)
|
||
| (succ x) (succ y) :=
|
||
match hasDecEq x y with
|
||
| isTrue xeqy := isTrue (xeqy ▸ Eq.refl (succ x))
|
||
| isFalse xney := isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney))
|
||
|
||
instance : DecidableEq ℕ :=
|
||
{decEq := hasDecEq}
|
||
|
||
def repeat.{u} {α : Type u} (f : ℕ → α → α) : ℕ → α → α
|
||
| 0 a := a
|
||
| (succ n) a := f n (repeat n a)
|
||
|
||
theorem natZeroEqZero : Nat.zero = 0 :=
|
||
rfl
|
||
|
||
/- properties of inequality -/
|
||
|
||
protected def leRefl : ∀ a : ℕ, a ≤ a :=
|
||
lessThanOrEqual.refl
|
||
|
||
theorem leSucc (n : ℕ) : n ≤ succ n :=
|
||
lessThanOrEqual.step (Nat.leRefl n)
|
||
|
||
theorem succLeSucc {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
|
||
fun h => lessThanOrEqual.ndrec (Nat.leRefl (succ n)) (fun a b => lessThanOrEqual.step) h
|
||
|
||
theorem zeroLe : ∀ (n : ℕ), 0 ≤ n
|
||
| 0 := Nat.leRefl 0
|
||
| (n+1) := lessThanOrEqual.step (zeroLe n)
|
||
|
||
theorem zeroLtSucc (n : ℕ) : 0 < succ n :=
|
||
succLeSucc (zeroLe n)
|
||
|
||
def succPos := zeroLtSucc
|
||
|
||
theorem notSuccLeZero : ∀ (n : ℕ), succ n ≤ 0 → False
|
||
.
|
||
|
||
theorem notLtZero (a : ℕ) : ¬ a < 0 := notSuccLeZero a
|
||
|
||
theorem predLePred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
|
||
fun h => lessThanOrEqual.ndrecOn h
|
||
(Nat.leRefl (pred n))
|
||
(fun n => Nat.rec (fun a b => b) (fun a b c => lessThanOrEqual.step) n)
|
||
|
||
theorem leOfSuccLeSucc {n m : ℕ} : succ n ≤ succ m → n ≤ m :=
|
||
predLePred
|
||
|
||
instance decidableLe : ∀ a b : ℕ, Decidable (a ≤ b)
|
||
| 0 b := isTrue (zeroLe b)
|
||
| (a+1) 0 := isFalse (notSuccLeZero a)
|
||
| (a+1) (b+1) :=
|
||
match decidableLe a b with
|
||
| isTrue h := isTrue (succLeSucc h)
|
||
| isFalse h := isFalse (fun a => h (leOfSuccLeSucc a))
|
||
|
||
instance decidableLt : ∀ a b : ℕ, Decidable (a < b) :=
|
||
fun a b => Nat.decidableLe (succ a) b
|
||
|
||
protected theorem eqOrLtOfLe {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b :=
|
||
lessThanOrEqual.casesOn h (Or.inl rfl) (fun n h => Or.inr (succLeSucc h))
|
||
|
||
theorem ltSuccOfLe {a b : ℕ} : a ≤ b → a < succ b :=
|
||
succLeSucc
|
||
|
||
theorem succSubSuccEqSub (a b : ℕ) : succ a - succ b = a - b :=
|
||
Nat.recOn b
|
||
(show succ a - succ zero = a - zero from (Eq.refl (succ a - succ zero)))
|
||
(fun b => congrArg pred)
|
||
|
||
theorem notSuccLeSelf : ∀ n : ℕ, ¬succ n ≤ n :=
|
||
fun n => Nat.rec (notSuccLeZero 0) (fun a b c => b (leOfSuccLeSucc c)) n
|
||
|
||
protected theorem ltIrrefl (n : ℕ) : ¬n < n :=
|
||
notSuccLeSelf n
|
||
|
||
protected theorem leTrans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k :=
|
||
lessThanOrEqual.ndrec h1 (fun p h2 => lessThanOrEqual.step)
|
||
|
||
theorem predLe : ∀ (n : ℕ), pred n ≤ n
|
||
| 0 := lessThanOrEqual.refl 0
|
||
| (succ a) := lessThanOrEqual.step (lessThanOrEqual.refl a)
|
||
|
||
theorem predLt : ∀ {n : ℕ}, n ≠ 0 → pred n < n
|
||
| 0 h := absurd rfl h
|
||
| (succ a) h := ltSuccOfLe (lessThanOrEqual.refl _)
|
||
|
||
theorem subLe (a b : ℕ) : a - b ≤ a :=
|
||
Nat.recOn b (Nat.leRefl (a - 0)) (fun b₁ => Nat.leTrans (predLe (a - b₁)))
|
||
|
||
theorem subLt : ∀ {a b : ℕ}, 0 < a → 0 < b → a - b < a
|
||
| 0 b h1 h2 := absurd h1 (Nat.ltIrrefl 0)
|
||
| (a+1) 0 h1 h2 := absurd h2 (Nat.ltIrrefl 0)
|
||
| (a+1) (b+1) h1 h2 :=
|
||
Eq.symm (succSubSuccEqSub a b) ▸
|
||
show a - b < succ a from
|
||
ltSuccOfLe (subLe a b)
|
||
|
||
protected theorem ltOfLtOfLe {n m k : ℕ} : n < m → m ≤ k → n < k :=
|
||
Nat.leTrans
|
||
|
||
end Nat
|