tickRecursor

formal source

  78/-! ## Tick is a natural-number object -/
  79
  80/-- Recursor on `Tick`: iterate `f` from `x` exactly `t.index` times. -/
  81def tickRecursor {X : Type u} (x : X) (f : X → X) (t : Tick) : X :=
  82  Nat.rec x (fun _ acc => f acc) t.index
  83
  84@[simp] theorem tickRecursor_zero {X : Type u} (x : X) (f : X → X) :
  85    tickRecursor x f tickZero = x := rfl
  86
  87@[simp] theorem tickRecursor_succ {X : Type u} (x : X) (f : X → X) (t : Tick) :
  88    tickRecursor x f (tickSucc t) = f (tickRecursor x f t) := rfl
  89
  90/-- **Tick is a Lawvere natural-number object.** Together with `tickZero`
  91and `tickSucc`, the `Tick` type satisfies the universal property of the
  92natural-number object: primitive recursion exists and is unique. -/
  93def tick_isNNO :
  94    IsNaturalNumberObject (N := Tick) tickZero tickSucc where
  95  recursor := fun {X} x f => tickRecursor x f
  96  recursor_zero := fun {X} x f => tickRecursor_zero x f
  97  recursor_step := fun {X} x f t => tickRecursor_succ x f t
  98  recursor_unique := by
  99    intro X x f h hz hs t
 100    -- Reduce to induction on t.index.
 101    suffices hgen : ∀ n : Nat, h ⟨n⟩ = tickRecursor x f ⟨n⟩ by
 102      have := hgen t.index
 103      cases t
 104      exact this
 105    intro n
 106    induction n with
 107    | zero => exact hz
 108    | succ n ih =>
 109        have hstep : h ⟨n + 1⟩ = h (tickSucc ⟨n⟩) := rfl
 110        rw [hstep, hs ⟨n⟩, ih]
 111        rfl