Branch paths and telescopes for PFunctor.FreeM

This file contains the path-dependent structure that lives on top of the basic free monad on a polynomial functor.

For a polynomial/container P, PFunctor.FreeM P α is the inductive type of well-founded P-branching trees with leaves labelled by α. The definitions below isolate the branch-object pattern of such a tree:

• FreeM.Path s records an explicit polynomial direction at every node.
• FreeM.PathAlong l s is the canonical path through s.mapLens l, i.e. the runtime branch through a control tree executed along a polynomial lens.
• FreeM.output s path recovers the leaf payload selected by that path.
• FreeM.append s k grafts a suffix tree selected by the canonical path of s.
• FreeM.TelescopeWith is the state-indexed initial algebra obtained by iterating such rounds, where the next state is selected by an abstract observation of the round.
• FreeM.Telescope is the specialization where observations are canonical branch paths.

Terminology and references

The same object appears under several names in the literature. In polynomial functor language, the free monad on a polynomial is a type of terminating decision trees. In container and W-type language, these are well-founded trees and Path is the type of paths through such a tree. In dependent-type presentations of games, these are dependent type trees and paths. In programming language semantics, the coinductive analogue is an interaction tree.

Relevant references include:

• Hancock and Setzer, Interactive Programs in Dependent Type Theory, for dependent I/O-trees over command-response worlds.
• Altenkirch, Ghani, Hancock, McBride, and Morris, Indexed Containers, for containers, indexed containers, and interaction structures.
• Libkind and Spivak, Pattern runs on matter, for free polynomial monads as terminating decision trees.
• Escardo and Oliva, Higher-order games with dependent types, for dependent type trees and paths in history-dependent games.
• Xia, Zakowski, He, Hur, Malecha, Pierce, and Zdancewic, Interaction Trees, for the coinductive programming-language analogue.

Canonical paths

def PFunctor.FreeM.Path.shape (P : PFunctor.{uA, uB}) (α : Type v) : Displayed.Shape P α

Displayed-family shape for canonical root-to-leaf paths.

@[reducible, inline]

abbrev PFunctor.FreeM.Path {P : PFunctor.{uA, uB}} {α : Type v} : P.FreeM α → Type uB

The canonical root-to-leaf path through a FreeM tree.

Runtime paths along a lens

def PFunctor.FreeM.PathAlong.shape {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : Displayed.Shape P α

Runtime path through a P-tree executed along a lens l : Lens P Q.

This is the displayed family over the source control tree whose node directions come from the runtime polynomial Q. A runtime direction d : Q.B (l.toFunA a) selects the source branch l.toFunB a d.

@[reducible, inline]

abbrev PFunctor.FreeM.PathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : Type uB₂

Runtime path through a P-tree executed along a lens l : Lens P Q.

def PFunctor.FreeM.output {P : PFunctor.{uA, uB}} {α : Type v} (s : P.FreeM α) : s.Path → α

The leaf payload selected by a path. Although the path itself records only branch choices, the tree and path together determine the terminal pure payload.

def PFunctor.FreeM.outputAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : PathAlong l s → α

The leaf payload selected by a runtime path along a lens.

@[simp]

theorem PFunctor.FreeM.outputAlong_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) (path : PathAlong l (pure x)) : outputAlong l (pure x) path = x

@[simp]

theorem PFunctor.FreeM.outputAlong_roll {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (d : Q.B (l.toFunA a)) (path : PathAlong l (rest (l.toFunB a d))) : outputAlong l (roll a rest) ⟨d, path⟩ = outputAlong l (rest (l.toFunB a d)) path

@[simp]

theorem PFunctor.FreeM.output_pure {P : PFunctor.{uA, uB}} {α : Type v} (x : α) (path : (pure x).Path) : (pure x).output path = x

@[simp]

theorem PFunctor.FreeM.output_roll {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (b : P.B a) (path : (rest b).Path) : (roll a rest).output ⟨b, path⟩ = (rest b).output path

def PFunctor.FreeM.projectPathAlongLocalHom {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : Displayed.LocalHom (PathAlong.shape l) (Path.shape P α)

Constructor-local projection from runtime paths to control paths.

def PFunctor.FreeM.projectPathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : PathAlong l s → s.Path

Project a concrete runtime path along a lens back to the abstract canonical branch path of the control tree.

@[simp]

theorem PFunctor.FreeM.projectPathAlong_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) (path : PathAlong l (pure x)) : projectPathAlong l (pure x) path = PUnit.unit

@[simp]

theorem PFunctor.FreeM.projectPathAlong_roll {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (path : PathAlong l (roll a rest)) : projectPathAlong l (roll a rest) path = ⟨l.toFunB a path.fst, projectPathAlong l (rest (l.toFunB a path.fst)) path.snd⟩

@[simp]

theorem PFunctor.FreeM.output_projectPathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) (path : PathAlong l s) : s.output (projectPathAlong l s path) = outputAlong l s path

Runtime paths and lens-mapped trees

def PFunctor.FreeM.pathAlongToMapLensPath {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : PathAlong l s → (FreeM.mapLens l s).Path

View a runtime path through s along l as the canonical path through the lens-mapped runtime tree s.mapLens l.

The two types have the same constructor shape, but PathAlong is defined over the source tree while Path (s.mapLens l) is defined over the lens-mapped tree.

@[simp]

theorem PFunctor.FreeM.pathAlongToMapLensPath_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) (path : PathAlong l (pure x)) : pathAlongToMapLensPath l (pure x) path = PUnit.unit

@[simp]

theorem PFunctor.FreeM.pathAlongToMapLensPath_roll {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (d : Q.B (l.toFunA a)) (path : PathAlong l (rest (l.toFunB a d))) : pathAlongToMapLensPath l (roll a rest) ⟨d, path⟩ = ⟨d, pathAlongToMapLensPath l (rest (l.toFunB a d)) path⟩

def PFunctor.FreeM.mapLensPathToPathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : (FreeM.mapLens l s).Path → PathAlong l s

View a canonical path through the lens-mapped runtime tree s.mapLens l as a runtime path through the original control tree s along l.

This is the inverse constructor-by-constructor view of pathAlongToMapLensPath.

@[simp]

theorem PFunctor.FreeM.mapLensPathToPathAlong_pure {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (x : α) (path : (FreeM.mapLens l (pure x)).Path) : mapLensPathToPathAlong l (pure x) path = PUnit.unit

@[simp]

theorem PFunctor.FreeM.mapLensPathToPathAlong_roll {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (d : Q.B (l.toFunA a)) (path : (FreeM.mapLens l (rest (l.toFunB a d))).Path) : mapLensPathToPathAlong l (roll a rest) ⟨d, path⟩ = ⟨d, mapLensPathToPathAlong l (rest (l.toFunB a d)) path⟩

@[simp]

theorem PFunctor.FreeM.mapLensPathToPathAlong_toMapLensPath {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) (path : PathAlong l s) : mapLensPathToPathAlong l s (pathAlongToMapLensPath l s path) = path

@[simp]

theorem PFunctor.FreeM.pathAlongToMapLensPath_toPathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) (path : (FreeM.mapLens l s).Path) : pathAlongToMapLensPath l s (mapLensPathToPathAlong l s path) = path

@[simp]

theorem PFunctor.FreeM.output_mapLens_pathAlongToMapLensPath {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) (path : PathAlong l s) : (FreeM.mapLens l s).output (pathAlongToMapLensPath l s path) = outputAlong l s path

@[simp]

theorem PFunctor.FreeM.outputAlong_mapLensPathToPathAlong {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) (path : (FreeM.mapLens l s).Path) : outputAlong l s (mapLensPathToPathAlong l s path) = (FreeM.mapLens l s).output path

def PFunctor.FreeM.append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) : (s₁.Path → P.FreeM β) → P.FreeM β

Dependent sequential composition for FreeM trees using canonical paths.

@[simp]

theorem PFunctor.FreeM.append_pure {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (x : α) (s₂ : (pure x).Path → P.FreeM β) : (pure x).append s₂ = s₂ PUnit.unit

@[simp]

theorem PFunctor.FreeM.append_roll {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (a : P.A) (rest : P.B a → P.FreeM α) (s₂ : (roll a rest).Path → P.FreeM β) : (roll a rest).append s₂ = roll a fun (b : P.B a) => (rest b).append fun (path : (rest b).Path) => s₂ ⟨b, path⟩

Canonical paths through appended trees

def PFunctor.FreeM.Path.liftAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) : ((path₁ : s₁.Path) → (s₂ path₁).Path → Type w) → (s₁.append s₂).Path → Type w

Lift a two-argument family indexed by a canonical prefix path and canonical suffix path to a family on the appended tree.

def PFunctor.FreeM.Path.append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path₁ : s₁.Path) : (s₂ path₁).Path → (s₁.append s₂).Path

Combine canonical prefix and suffix paths into a canonical path through the appended tree.

@[simp]

theorem PFunctor.FreeM.Path.append_done {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (x : α) (s₂ : (pure x).Path → P.FreeM β) (path₂ : (s₂ PUnit.unit).Path) : append (pure x) s₂ PUnit.unit path₂ = path₂

def PFunctor.FreeM.Path.split {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) : (s₁.append s₂).Path → (path₁ : s₁.Path) × (s₂ path₁).Path

Split a canonical path through an appended tree into prefix and suffix canonical paths.

@[simp]

theorem PFunctor.FreeM.Path.liftAppend_append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) : liftAppend s₁ s₂ F (append s₁ s₂ path₁ path₂) = F path₁ path₂

liftAppend on an appended canonical path reduces to the original two-argument family.

@[simp]

theorem PFunctor.FreeM.Path.split_append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) : split s₁ s₂ (append s₁ s₂ path₁ path₂) = ⟨path₁, path₂⟩

Splitting after appending recovers the original canonical prefix and suffix.

@[simp]

theorem PFunctor.FreeM.Path.append_split {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path : (s₁.append s₂).Path) : have splitPath := split s₁ s₂ path; append s₁ s₂ splitPath.fst splitPath.snd = path

Appending the components produced by split recovers the original canonical path.

def PFunctor.FreeM.Path.packAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) : F path₁ path₂ → liftAppend s₁ s₂ F (append s₁ s₂ path₁ path₂)

Transport a value of F path₁ path₂ to the liftAppend family at the combined canonical path.

@[simp]

theorem PFunctor.FreeM.Path.packAppend_done {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (x : α) (s₂ : (pure x).Path → P.FreeM β) (F : (path₁ : (pure x).Path) → (s₂ path₁).Path → Type w) (path₂ : (s₂ PUnit.unit).Path) (y : F PUnit.unit path₂) : packAppend (pure x) s₂ F PUnit.unit path₂ y = y

def PFunctor.FreeM.Path.unpackAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) : liftAppend s₁ s₂ F (append s₁ s₂ path₁ path₂) → F path₁ path₂

Transport a value from the liftAppend family at an appended canonical path back to the original two-argument family.

theorem PFunctor.FreeM.Path.liftAppend_congr {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F G : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) : (∀ (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path), F path₁ path₂ = G path₁ path₂) → ∀ (path : (s₁.append s₂).Path), liftAppend s₁ s₂ F path = liftAppend s₁ s₂ G path

liftAppend respects pointwise equality of the pair-indexed family.

@[simp]

theorem PFunctor.FreeM.Path.liftAppend_const {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (γ : Type w) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ (fun (x : s₁.Path) (x_1 : (s₂ x).Path) => γ) path = γ

A constant family is unaffected by liftAppend.

theorem PFunctor.FreeM.Path.liftAppend_split {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) : have splitPath := split s₁ s₂ path; liftAppend s₁ s₂ F path = F splitPath.fst splitPath.snd

liftAppend can be reconstructed from the path pieces returned by split.

def PFunctor.FreeM.Path.unliftAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ F path → have splitPath := split s₁ s₂ path; F splitPath.fst splitPath.snd

Reinterpret a liftAppend value against the path pair recovered by split.

@[simp]

theorem PFunctor.FreeM.Path.unpackAppend_packAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) (x : F path₁ path₂) : unpackAppend s₁ s₂ F path₁ path₂ (packAppend s₁ s₂ F path₁ path₂ x) = x

@[simp]

theorem PFunctor.FreeM.Path.packAppend_unpackAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) (x : liftAppend s₁ s₂ F (append s₁ s₂ path₁ path₂)) : packAppend s₁ s₂ F path₁ path₂ (unpackAppend s₁ s₂ F path₁ path₂ x) = x

def PFunctor.FreeM.Path.collapseAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (s₁.append s₂).Path → Type w) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => F (append s₁ s₂ path₁ path₂)) path → F path

Collapse a liftAppend family indexed by append path₁ path₂ back to the fused path index.

@[simp]

theorem PFunctor.FreeM.Path.collapseAppend_append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (s₁.append s₂).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) (x : liftAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => F (append s₁ s₂ path₁ path₂)) (append s₁ s₂ path₁ path₂)) : collapseAppend s₁ s₂ F (append s₁ s₂ path₁ path₂) x = unpackAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => F (append s₁ s₂ path₁ path₂)) path₁ path₂ x

def PFunctor.FreeM.Path.liftAppendProd {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (A B : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => A path₁ path₂ × B path₁ path₂) path → liftAppend s₁ s₂ A path × liftAppend s₁ s₂ B path

Split a fused liftAppend product payload into separately lifted payloads.

def PFunctor.FreeM.Path.liftAppendProdMk {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (A B : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ A path × liftAppend s₁ s₂ B path → liftAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => A path₁ path₂ × B path₁ path₂) path

Fuse separately lifted payloads into a lifted product payload.

@[simp]

theorem PFunctor.FreeM.Path.liftAppendProdMk_liftAppendProd {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (A B : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) (x : liftAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => A path₁ path₂ × B path₁ path₂) path) : liftAppendProdMk s₁ s₂ A B path (liftAppendProd s₁ s₂ A B path x) = x

@[simp]

theorem PFunctor.FreeM.Path.liftAppendProd_liftAppendProdMk {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (A B : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path : (s₁.append s₂).Path) (x : liftAppend s₁ s₂ A path × liftAppend s₁ s₂ B path) : liftAppendProd s₁ s₂ A B path (liftAppendProdMk s₁ s₂ A B path x) = x

@[simp]

theorem PFunctor.FreeM.Path.liftAppendProd_packAppend {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (A B : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) (x : A path₁ path₂ × B path₁ path₂) : liftAppendProd s₁ s₂ A B (append s₁ s₂ path₁ path₂) (packAppend s₁ s₂ (fun (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) => A path₁ path₂ × B path₁ path₂) path₁ path₂ x) = (packAppend s₁ s₂ A path₁ path₂ x.1, packAppend s₁ s₂ B path₁ path₂ x.2)

theorem PFunctor.FreeM.Path.rel_unliftAppend_append {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F G : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (R : (path₁ : s₁.Path) → (path₂ : (s₂ path₁).Path) → F path₁ path₂ → G path₁ path₂ → Prop) (path₁ : s₁.Path) (path₂ : (s₂ path₁).Path) (x : F path₁ path₂) (y : G path₁ path₂) : let path := append s₁ s₂ path₁ path₂; R (split s₁ s₂ path).fst (split s₁ s₂ path).snd (unliftAppend s₁ s₂ F path (packAppend s₁ s₂ F path₁ path₂ x)) (unliftAppend s₁ s₂ G path (packAppend s₁ s₂ G path₁ path₂ y)) = R path₁ path₂ x y

When path = append path₁ path₂, the round-trip (packAppend then unliftAppend) recovers the original pair-indexed relation value.

def PFunctor.FreeM.Path.liftAppendRel {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F G : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (R : (path₁ : s₁.Path) → (path₂ : (s₂ path₁).Path) → F path₁ path₂ → G path₁ path₂ → Prop) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ F path → liftAppend s₁ s₂ G path → Prop

Lift a binary relation on pair-indexed families to the fused appended path.

theorem PFunctor.FreeM.Path.liftAppendRel_iff {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F G : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (R : (path₁ : s₁.Path) → (path₂ : (s₂ path₁).Path) → F path₁ path₂ → G path₁ path₂ → Prop) (path : (s₁.append s₂).Path) (x : liftAppend s₁ s₂ F path) (y : liftAppend s₁ s₂ G path) : liftAppendRel s₁ s₂ F G R path x y ↔ R (split s₁ s₂ path).fst (split s₁ s₂ path).snd (unliftAppend s₁ s₂ F path x) (unliftAppend s₁ s₂ G path y)

liftAppendRel applies R at the path pair recovered by split.

def PFunctor.FreeM.Path.liftAppendPred {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (Pred : (path₁ : s₁.Path) → (path₂ : (s₂ path₁).Path) → F path₁ path₂ → Prop) (path : (s₁.append s₂).Path) : liftAppend s₁ s₂ F path → Prop

Lift a unary predicate on a pair-indexed family to the fused appended path.

theorem PFunctor.FreeM.Path.liftAppendPred_iff {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : s₁.Path) → (s₂ path₁).Path → Type w) (Pred : (path₁ : s₁.Path) → (path₂ : (s₂ path₁).Path) → F path₁ path₂ → Prop) (path : (s₁.append s₂).Path) (x : liftAppend s₁ s₂ F path) : liftAppendPred s₁ s₂ F Pred path x ↔ Pred (split s₁ s₂ path).fst (split s₁ s₂ path).snd (unliftAppend s₁ s₂ F path x)

liftAppendPred applies the predicate at the path pair recovered by split.

Lens-executed paths through appended trees

def PFunctor.FreeM.PathAlong.liftAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) : ((path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) → PathAlong l (s₁.append s₂) → Type w

Lift a two-argument family indexed by a runtime prefix path and a runtime suffix path to a family on the appended tree.

The suffix is selected by the control projection of the runtime prefix.

def PFunctor.FreeM.PathAlong.append {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path₁ : PathAlong l s₁) : PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → PathAlong l (s₁.append s₂)

Combine a runtime prefix path and a runtime suffix path into a runtime path through the appended tree.

def PFunctor.FreeM.PathAlong.split {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) : PathAlong l (s₁.append s₂) → (path₁ : PathAlong l s₁) × PathAlong l (s₂ (projectPathAlong l s₁ path₁))

Split a runtime path through an appended tree into its prefix runtime path and suffix runtime path.

@[simp]

theorem PFunctor.FreeM.PathAlong.liftAppend_append {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) : liftAppend l s₁ s₂ F (append l s₁ s₂ path₁ path₂) = F path₁ path₂

liftAppend on an appended runtime path reduces to the original two-argument family.

@[simp]

theorem PFunctor.FreeM.PathAlong.split_append {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) : split l s₁ s₂ (append l s₁ s₂ path₁ path₂) = ⟨path₁, path₂⟩

Splitting after appending recovers the original runtime prefix and suffix.

@[simp]

theorem PFunctor.FreeM.PathAlong.append_split {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path : PathAlong l (s₁.append s₂)) : have splitPath := split l s₁ s₂ path; append l s₁ s₂ splitPath.fst splitPath.snd = path

Appending the components produced by split recovers the original runtime path.

def PFunctor.FreeM.PathAlong.packAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) : F path₁ path₂ → liftAppend l s₁ s₂ F (append l s₁ s₂ path₁ path₂)

Transport a value of F path₁ path₂ to the liftAppend family at the combined runtime path. The definition follows the same recursion as liftAppend, so it avoids explicit equality transports.

def PFunctor.FreeM.PathAlong.unpackAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) : liftAppend l s₁ s₂ F (append l s₁ s₂ path₁ path₂) → F path₁ path₂

Transport a value from the liftAppend family at an appended runtime path back to the original two-argument family.

theorem PFunctor.FreeM.PathAlong.liftAppend_split {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path : PathAlong l (s₁.append s₂)) : have splitPath := split l s₁ s₂ path; liftAppend l s₁ s₂ F path = F splitPath.fst splitPath.snd

liftAppend can be reconstructed from the runtime path pieces returned by split.

def PFunctor.FreeM.PathAlong.unliftAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path : PathAlong l (s₁.append s₂)) : liftAppend l s₁ s₂ F path → have splitPath := split l s₁ s₂ path; F splitPath.fst splitPath.snd

Reinterpret a runtime liftAppend value against the path pair recovered by split.

@[simp]

theorem PFunctor.FreeM.PathAlong.unpackAppend_packAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) (x : F path₁ path₂) : unpackAppend l s₁ s₂ F path₁ path₂ (packAppend l s₁ s₂ F path₁ path₂ x) = x

@[simp]

theorem PFunctor.FreeM.PathAlong.packAppend_unpackAppend {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (F : (path₁ : PathAlong l s₁) → PathAlong l (s₂ (projectPathAlong l s₁ path₁)) → Type w) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) (x : liftAppend l s₁ s₂ F (append l s₁ s₂ path₁ path₂)) : packAppend l s₁ s₂ F path₁ path₂ (unpackAppend l s₁ s₂ F path₁ path₂ x) = x

@[simp]

theorem PFunctor.FreeM.PathAlong.projectPathAlong_append {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} {β : Type t} (l : P.Lens Q) (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (path₁ : PathAlong l s₁) (path₂ : PathAlong l (s₂ (projectPathAlong l s₁ path₁))) : projectPathAlong l (s₁.append s₂) (append l s₁ s₂ path₁ path₂) = Path.append s₁ s₂ (projectPathAlong l s₁ path₁) (projectPathAlong l (s₂ (projectPathAlong l s₁ path₁)) path₂)

Projecting an appended runtime path gives the appended projected paths.

Telescopes

inductive PFunctor.FreeM.TelescopeWith {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} (round : (s : St) → P.FreeM (Out s)) (Obs : St → Type w) (step : (s : St) → Obs s → St) : St → Type (max w z)

Initial-algebra presentation of a state-machine telescope of FreeM rounds observed through an arbitrary observation family Obs.

At each state s, an inhabitant either terminates or extends by running round s and recursing into the next state selected by an observation obs : Obs s. The observation family is intentionally abstract: canonical FreeM branch paths use Obs s = Path (round s), while quotiented or compact views can erase uninformative singleton choices.

• done {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {Obs : St → Type w} {step : (s : St) → Obs s → St} (s : St) : TelescopeWith round Obs step s
• extend {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {Obs : St → Type w} {step : (s : St) → Obs s → St} (s : St) (cont : (obs : Obs s) → TelescopeWith round Obs step (step s obs)) : TelescopeWith round Obs step s

def PFunctor.FreeM.TelescopeWith.toFreeM {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {Obs : St → Type w} {step : (s : St) → Obs s → St} {β : Type t} (appendRound : (s : St) → (Obs s → P.FreeM β) → P.FreeM β) (finish : St → P.FreeM β) {s : St} : TelescopeWith round Obs step s → P.FreeM β

Flatten a telescope into a single FreeM tree by iterated dependent append, using appendRound to graft each observed round and finish at terminal states.

@[simp]

theorem PFunctor.FreeM.TelescopeWith.toFreeM_done {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {Obs : St → Type w} {step : (s : St) → Obs s → St} {β : Type t} (appendRound : (s : St) → (Obs s → P.FreeM β) → P.FreeM β) (finish : St → P.FreeM β) (s : St) : toFreeM appendRound finish (done s) = finish s

@[simp]

theorem PFunctor.FreeM.TelescopeWith.toFreeM_extend {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {Obs : St → Type w} {step : (s : St) → Obs s → St} {β : Type t} (appendRound : (s : St) → (Obs s → P.FreeM β) → P.FreeM β) (finish : St → P.FreeM β) (s : St) (cont : (obs : Obs s) → TelescopeWith round Obs step (step s obs)) : toFreeM appendRound finish (extend s cont) = appendRound s fun (obs : Obs s) => toFreeM appendRound finish (cont obs)

@[reducible, inline]

abbrev PFunctor.FreeM.Telescope {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} (round : (s : St) → P.FreeM (Out s)) (step : (s : St) → (round s).Path → St) : St → Type (max uB z)

State-machine telescopes whose observations are canonical FreeM branch paths. This is the default specialization of TelescopeWith; users with a more compact observation type should use TelescopeWith directly.

@[reducible, inline]

abbrev PFunctor.FreeM.Telescope.done {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {step : (s : St) → (round s).Path → St} (s : St) : Telescope round step s

Constructor wrapper for terminating a canonical-path telescope.

@[reducible, inline]

abbrev PFunctor.FreeM.Telescope.extend {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {step : (s : St) → (round s).Path → St} (s : St) (cont : (path : (round s).Path) → Telescope round step (step s path)) : Telescope round step s

Constructor wrapper for extending a canonical-path telescope.

def PFunctor.FreeM.Telescope.toFreeM {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {step : (s : St) → (round s).Path → St} {β : Type t} (finish : St → P.FreeM β) {s : St} : Telescope round step s → P.FreeM β

Flatten a canonical-path telescope into a single FreeM tree by iterated dependent append, using finish at terminal states.

@[simp]

theorem PFunctor.FreeM.Telescope.toFreeM_done {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {step : (s : St) → (round s).Path → St} {β : Type t} (finish : St → P.FreeM β) (s : St) : toFreeM finish (done s) = finish s

@[simp]

theorem PFunctor.FreeM.Telescope.toFreeM_extend {P : PFunctor.{uA, uB}} {St : Type z} {Out : St → Type v} {round : (s : St) → P.FreeM (Out s)} {step : (s : St) → (round s).Path → St} {β : Type t} (finish : St → P.FreeM β) (s : St) (cont : (path : (round s).Path) → Telescope round step (step s path)) : toFreeM finish (extend s cont) = (round s).append fun (path : (round s).Path) => toFreeM finish (cont path)