Auxiliary lemmas for PFunctor.M

Small extensions to Mathlib.Data.PFunctor.Univariate.M used by the ToMathlib.ITree port of the Coq InteractionTrees library.

The Mathlib file already supplies M.mk, M.dest, M.corec, M.dest_mk, M.mk_dest, M.dest_corec, M.corec_unique, and the bisimulation principle M.bisim. We add a few rewriting helpers that come up repeatedly when defining and reasoning about ITrees:

• M.dest_inj / M.eq_of_dest_eq — M.dest is injective on M P (since it has a left inverse M.mk).
• M.dest_corec_apply — destructured form of M.dest_corec whose RHS unpacks the Sigma so that nested pattern matches reduce by rfl.
• M.dest_corec_eq — reformulation of M.dest_corec that lets simp see the result as an explicit Sigma.
• M.corec_eq_corec — bisimulation principle for two corecs, the workhorse for bind/iter rewriting.
• M.corec_dest — M.corec dest = id. The corecursive identity.

Injectivity of dest

theorem PFunctor.M.eq_of_dest_eq {P : PFunctor.{uA, uB}} {u v : P.M} (h : u.dest = v.dest) : u = v

M.dest is injective: equal destructions imply equal M-values, since M.mk is a left inverse of M.dest (see M.mk_dest).

@[simp]

theorem PFunctor.M.dest_inj {P : PFunctor.{uA, uB}} {u v : P.M} : u.dest = v.dest ↔ u = v

Corec helpers

theorem PFunctor.M.dest_corec_apply {P : PFunctor.{uA, uB}} {α : Type v} (g : α → ↑P α) (x : α) : (M.corec g x).dest = ⟨(g x).fst, fun (b : P.B (g x).fst) => M.corec g ((g x).snd b)⟩

M.dest_corec with the result Sigma unpacked. The shape of M.dest's output is (g x).1; the children component, after applying the PFunctor.map on the RHS of M.dest_corec, is M.corec g ∘ (g x).2.

theorem PFunctor.M.dest_corec_eq {P : PFunctor.{uA, uB}} {α : Type v} {a : P.A} {h : P.B a → α} (g : α → ↑P α) (x : α) (heq : g x = ⟨a, h⟩) : (M.corec g x).dest = ⟨a, fun (b : P.B a) => M.corec g (h b)⟩

Pointwise version of dest_corec_apply written in Sigma-eta form, convenient when the right-hand side of a corec step is already known explicitly.

theorem PFunctor.M.corec_eq_corec {P : PFunctor.{uA, uB}} {α β : Type v} (g : α → ↑P α) (h : β → ↑P β) (R : α → β → Prop) (x₀ : α) (y₀ : β) (hR : R x₀ y₀) (step : ∀ (x : α) (y : β), R x y → ∃ (a : P.A) (f : P.B a → α) (f' : P.B a → β), g x = ⟨a, f⟩ ∧ h y = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) : M.corec g x₀ = M.corec h y₀

Bisimulation principle specialized to two corecs built from the same shape transformer. If at every reachable state the two seed transitions agree on shapes and yield bisimilar children, the two corecs are equal.

theorem PFunctor.M.corec_dest {P : PFunctor.{uA, uB}} (u : P.M) : M.corec dest u = u

M.corec dest = id. The corecursive identity. Together with M.corec_unique it characterises corec as the unique solution to dest ∘ f = map f ∘ g.