tickZero

formal source

  49@[simp] theorem tickSucc_index (t : Tick) : (tickSucc t).index = t.index + 1 := rfl
  50
  51/-- The canonical zero tick. -/
  52def tickZero : Tick := ⟨0⟩
  53
  54@[simp] theorem tickZero_index : tickZero.index = 0 := rfl
  55
  56/-! ## Tick is canonically the natural numbers -/
  57
  58/-- The canonical equivalence between `Tick` and `Nat` via the index. -/
  59def tickEquivNat : Tick ≃ Nat where
  60  toFun t := t.index
  61  invFun n := ⟨n⟩
  62  left_inv := by intro t; cases t; rfl
  63  right_inv := by intro n; rfl
  64
  65@[simp] theorem tickEquivNat_apply (t : Tick) : tickEquivNat t = t.index := rfl
  66@[simp] theorem tickEquivNat_symm_apply (n : Nat) :
  67    tickEquivNat.symm n = ⟨n⟩ := rfl
  68
  69@[simp] theorem tickEquivNat_zero : tickEquivNat tickZero = 0 := rfl
  70
  71@[simp] theorem tickEquivNat_succ (t : Tick) :
  72    tickEquivNat (tickSucc t) = (tickEquivNat t) + 1 := rfl
  73
  74/-- The canonical equivalence `Tick ≃ LogicNat` via `Nat`. -/
  75def tickEquivLogicNat : Tick ≃ LogicNat :=
  76  tickEquivNat.trans LogicNat.equivNat.symm
  77
  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