recursor

formal source

  48
  49/-- The LogicNat primitive recursion principle, implemented via Lean's
  50    built-in pattern matching on the inductive type. -/
  51def recursor {α : Type*} (base : α) (step : α → α) : LogicNat → α
  52  | LogicNat.identity => base
  53  | LogicNat.step n => step (recursor base step n)
  54
  55theorem recursor_zero {α : Type*} (base : α) (step : α → α) :
  56    recursor base step LogicNat.zero = base := rfl
  57
  58theorem recursor_succ {α : Type*} (base : α) (step : α → α) (n : LogicNat) :
  59    recursor base step (LogicNat.succ n) = step (recursor base step n) := rfl
  60
  61/-! ## NNO universal property statement
  62
  63In a category C with terminal object 1 and an endomorphism `s : N → N`,
  64an NNO is a triple `(N, zero : 1 → N, succ : N → N)` such that for every
  65`(A, base : 1 → A, step : A → A)` there is a unique morphism `f : N → A`
  66with `f ∘ zero = base` and `f ∘ succ = step ∘ f`.
  67
  68In `Type` (the category of types), `1 = Unit` and the universal property
  69becomes: for every `(A, base : Unit → A, step : A → A)` there is a unique
  70`f : N → A` satisfying the obvious equations. We collapse `Unit → A` to
  71just `A` (the points of A correspond bijectively to maps from `Unit`).
  72-/
  73
  74/-- The NNO universal property on `LogicNat` in `Type`: existence. -/
  75theorem nno_universal_existence {α : Type*} (base : α) (step : α → α) :
  76    ∃ (f : LogicNat → α),
  77      f LogicNat.zero = base ∧
  78      ∀ n, f (LogicNat.succ n) = step (f n) :=
  79  ⟨recursor base step, recursor_zero base step, recursor_succ base step⟩
  80
  81/-- The NNO universal property on `LogicNat` in `Type`: uniqueness. -/