160 lines
4.9 KiB
Text
160 lines
4.9 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 : ℕ) (h : succ n ≤ 0) : False :=
|
||
nomatch h
|
||
|
||
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
|