mk_dest — Mathlib

English

The constructor and destructor are coherently related: mk (dest x) = x for any Cofix value x.

Русский

Конструктор и деструктор согласованы: mk (dest x) = x для любого x ∈ Cofix.

LaTeX

$$$\\forall x:\\mathrm{Cofix}\\,F\\,\\alpha,\\; \\mathrm{Cofix.mk}(\\mathrm{Cofix.dest}\\,x) = x$$$

Lean4

theorem mk_dest {α : TypeVec n} (x : Cofix F α) : Cofix.mk (Cofix.dest x) = x :=
  by
  apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl
  dsimp
  intro x y h
  rw [h]
  conv =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]
  rw [← comp_map, ← appendFun_comp, id_comp]
  rw [← comp_map, ← appendFun_comp, id_comp, ← Cofix.mk]
  congr 1
  apply congrArg
  funext x
  apply Quot.sound
  rfl

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