corecContents — Mathlib

English

Define how to build the contents of an M-type by recursively composing g0, g1, g2 with the current path and shape.

Русский

Определение построения содержимого M‑типа через рекурсивное сочетание g0, g1, g2 с текущим путём и формой.

LaTeX

$$$\\text{corecContents} : (g_0, g_1, g_2) \\to \\text{Path} \\; P \\; x \\Rightarrow \\text{α}$ (описание рекурсивного содержимого)$$

Lean4

/-- Using corecursion, construct the contents of an M-type -/
def corecContents {α : TypeVec.{u} n} {β : Type u} (g₀ : β → P.A) (g₁ : ∀ b : β, P.drop.B (g₀ b) ⟹ α)
    (g₂ : ∀ b : β, P.last.B (g₀ b) → β) (x : _) (b : β) (h : x = M.corecShape P g₀ g₂ b) : M.Path P x ⟹ α
  | _, M.Path.root x a f h' i c =>
    have : a = g₀ b := by
      rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
      cases h'
      rfl
    g₁ b i (P.castDropB this i c)
  | _, M.Path.child x a f h' j i c =>
    have h₀ : a = g₀ b := by
      rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
      cases h'
      rfl
    have h₁ : f j = M.corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j)) :=
      by
      rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
      cases h'
      rfl
    M.corecContents g₀ g₁ g₂ (f j) (g₂ b (P.castLastB h₀ j)) h₁ i c

Похожие утверждения