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.StoppingTree is the state-indexed initial algebra whose next state is selected by an abstract observation.
• 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

@[implicit_reducible]

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

Displayed algebra 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.

The node interface

A path through an operation node is a direction together with a path through the selected child. cons, head and tail are the public interface to that structure; statements and lemmas go through them rather than through the anonymous constructor and projections of the underlying sigma type, so nothing outside this file depends on how Displayed unfolds. The node is written in its simp normal form (FreeM.lift a).bind rest; the constructor spelling FreeM.liftBind a rest produced by pattern matching is the same tree.

def PFunctor.FreeM.Path.cons {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (b : P.B a) (path : (rest b).Path) : ((lift a).bind rest).Path

Prepend one operation-node direction to a path through the selected child.

def PFunctor.FreeM.Path.head {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift a).bind rest).Path) : P.B a

The direction selected at the root of a non-leaf path.

def PFunctor.FreeM.Path.tail {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift a).bind rest).Path) : (rest (head a rest path)).Path

The path remaining below the root direction of a non-leaf path.

@[simp]

theorem PFunctor.FreeM.Path.head_cons {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (b : P.B a) (path : (rest b).Path) : head a rest (cons a rest b path) = b

@[simp]

theorem PFunctor.FreeM.Path.tail_cons {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (b : P.B a) (path : (rest b).Path) : tail a rest (cons a rest b path) = path

@[simp]

theorem PFunctor.FreeM.Path.cons_head_tail {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift a).bind rest).Path) : cons a rest (head a rest path) (tail a rest path) = path

@[simp]

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

head on a path destructured by pattern matching. The path is not indexed: its hidden sigma type reduces when the polynomial is concrete.

@[simp]

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

tail on a path destructured by pattern matching.

theorem PFunctor.FreeM.Path.ext {P : PFunctor.{uA, uB}} {α : Type v} {a : P.A} {rest : P.B a → P.FreeM α} {path path' : ((lift a).bind rest).Path} (hhead : head a rest path = head a rest path') (htail : tail a rest path ≍ tail a rest path') : path = path'

Two paths through a node agree once their directions and tails agree.

Runtime paths along a lens

@[implicit_reducible]

def PFunctor.FreeM.PathAlong.algebra {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : Displayed.Algebra 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.

The node interface

The runtime analogue of Path.cons / Path.head / Path.tail: a runtime path through an operation node is a runtime direction together with a runtime path through the source branch it selects.

def PFunctor.FreeM.PathAlong.cons {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))) : PathAlong l ((lift a).bind rest)

Prepend one runtime direction to a runtime path through the branch it selects.

def PFunctor.FreeM.PathAlong.head {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 ((lift a).bind rest)) : Q.B (l.toFunA a)

The runtime direction selected at the root of a non-leaf runtime path.

def PFunctor.FreeM.PathAlong.tail {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 ((lift a).bind rest)) : PathAlong l (rest (l.toFunB a (head l a rest path)))

The runtime path remaining below the root direction of a non-leaf runtime path.

@[simp]

theorem PFunctor.FreeM.PathAlong.head_cons {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))) : head l a rest (cons l a rest d path) = d

@[simp]

theorem PFunctor.FreeM.PathAlong.tail_cons {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))) : tail l a rest (cons l a rest d path) = path

@[simp]

theorem PFunctor.FreeM.PathAlong.cons_head_tail {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 ((lift a).bind rest)) : cons l a rest (head l a rest path) (tail l a rest path) = path

@[simp]

theorem PFunctor.FreeM.PathAlong.head_mk {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))) : head l a rest ⟨d, path⟩ = d

head on a runtime path destructured by pattern matching.

@[simp]

theorem PFunctor.FreeM.PathAlong.tail_mk {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))) : tail l a rest ⟨d, path⟩ = path

tail on a runtime path destructured by pattern matching.

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.Path.ofHandler {P : PFunctor.{uA, uB}} {α : Type v} (choose : (a : P.A) → P.B a) (tree : P.FreeM α) : tree.Path

Follow a fixed direction selector at every operation node to obtain a complete path through a free tree. The selector is operation-dependent, but does not inspect the continuation below the selected direction.

@[simp]

theorem PFunctor.FreeM.Path.ofHandler_pure {P : PFunctor.{uA, uB}} {α : Type v} (choose : (a : P.A) → P.B a) (value : α) : ofHandler choose (pure value) = PUnit.unit

theorem PFunctor.FreeM.Path.ofHandler_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (choose : (a : P.A) → P.B a) (operation : P.A) (next : P.B operation → P.FreeM α) : ofHandler choose (liftBind operation next) = ⟨choose operation, ofHandler choose (next (choose operation))⟩

def PFunctor.FreeM.collapseUnit {α : Type v} (tree : y.FreeM α) : α

Read the leaf selected by the unique direction of every node in a free tree over the identity polynomial y.

@[simp]

theorem PFunctor.FreeM.collapseUnit_pure {α : Type v} (value : α) : (pure value).collapseUnit = value

theorem PFunctor.FreeM.collapseUnit_liftBind {α : Type v} (next : PUnit.{uB + 1} → y.FreeM α) : (liftBind PUnit.unit next).collapseUnit = (next PUnit.unit).collapseUnit

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 (FreeM.pure x)) : outputAlong l (pure x) path = x

theorem PFunctor.FreeM.outputAlong_liftBind {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 ((lift a).bind rest)) : outputAlong l (liftBind a rest) path = outputAlong l (rest (l.toFunB a (PathAlong.head l a rest path))) (PathAlong.tail l a rest path)

@[simp]

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

theorem PFunctor.FreeM.output_liftBind {P : PFunctor.{uA, uB}} {α : Type v} (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift a).bind rest).Path) : (liftBind a rest).output path = (rest (Path.head a rest path)).output (Path.tail a rest path)

def PFunctor.FreeM.projectPathAlongLocalMap {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) : Displayed.LocalMap (PathAlong.algebra l) (Path.algebra 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 (FreeM.pure x)) : projectPathAlong l (pure x) path = PUnit.unit

theorem PFunctor.FreeM.projectPathAlong_liftBind {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 ((lift a).bind rest)) : projectPathAlong l (liftBind a rest) path = Path.cons a rest (l.toFunB a (PathAlong.head l a rest path)) (projectPathAlong l (rest (l.toFunB a (PathAlong.head l a rest path))) (PathAlong.tail l a rest path))

@[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 (FreeM.pure x)) : pathAlongToMapLensPath l (pure x) path = PUnit.unit

theorem PFunctor.FreeM.pathAlongToMapLensPath_liftBind {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 ((lift a).bind rest)) : pathAlongToMapLensPath l (liftBind a rest) path = Path.cons (l.toFunA a) (fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))) (PathAlong.head l a rest path) (pathAlongToMapLensPath l (rest (l.toFunB a (PathAlong.head l a rest path))) (PathAlong.tail l a rest 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 (FreeM.pure x)).Path) : mapLensPathToPathAlong l (pure x) path = PUnit.unit

theorem PFunctor.FreeM.mapLensPathToPathAlong_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift (l.toFunA a)).bind fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))).Path) : mapLensPathToPathAlong l (liftBind a rest) path = let d := Path.head (l.toFunA a) (fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))) path; PathAlong.cons l a rest d (mapLensPathToPathAlong l (rest (l.toFunB a d)) (Path.tail (l.toFunA a) (fun (d : Q.B (l.toFunA a)) => FreeM.mapLens 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.Path.pullMapLens {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (s : P.FreeM α) : (FreeM.mapLens l s).Path → s.Path

Pull a canonical path through a lens-mapped tree back to the corresponding canonical path through the source tree.

@[simp]

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

theorem PFunctor.FreeM.Path.pullMapLens_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {Q : PFunctor.{uA₂, uB₂}} (l : P.Lens Q) (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift (l.toFunA a)).bind fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))).Path) : pullMapLens l (liftBind a rest) path = let d := head (l.toFunA a) (fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))) path; cons a rest (l.toFunB a d) (pullMapLens l (rest (l.toFunB a d)) (tail (l.toFunA a) (fun (d : Q.B (l.toFunA a)) => FreeM.mapLens l (rest (l.toFunB a d))) path))

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

Pulling a mapped path directly agrees with first viewing it as a runtime path and then projecting it to the control tree.

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

Pull a path through a leaf-relabelled tree back to the original tree. Relabelling changes no operation-node directions.

@[simp]

theorem PFunctor.FreeM.Path.pullMap_pure {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (f : α → β) (x : α) (path : (map f (FreeM.pure x)).Path) : pullMap f (pure x) path = PUnit.unit

theorem PFunctor.FreeM.Path.pullMap_liftBind {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} (f : α → β) (a : P.A) (rest : P.B a → P.FreeM α) (path : ((lift a).bind fun (b : P.B a) => map f (rest b)).Path) : pullMap f (liftBind a rest) path = cons a rest (head a (fun (b : P.B a) => map f (rest b)) path) (pullMap f (rest (head a (fun (b : P.B a) => map f (rest b)) path)) (tail a (fun (b : P.B a) => map f (rest b)) path))

@[implicit_reducible]

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₂ : (FreeM.pure x).Path → P.FreeM β) : (pure x).append s₂ = s₂ PUnit.unit

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

@[simp]

theorem PFunctor.FreeM.append_output_eq_bind {P : PFunctor.{uA, uB}} {α β : Type v} (s : P.FreeM α) (k : α → P.FreeM β) : (s.append fun (path : s.Path) => k (s.output path)) = s >>= k

Grafting a continuation selected only by the leaf payload is ordinary free-monad bind. append is more general because its continuation may inspect the entire path; this theorem identifies their exact overlap.

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₂ : (FreeM.pure x).Path → P.FreeM β) (path₂ : (s₂ PUnit.unit).Path) : append (pure x) s₂ PUnit.unit path₂ = path₂

theorem PFunctor.FreeM.Path.append_tree_assoc {P : PFunctor.{uA, uB}} {α : Type v} {β : Type t} {γ : Type z} (s₁ : P.FreeM α) (s₂ : s₁.Path → P.FreeM β) (s₃ : (s₁.append s₂).Path → P.FreeM γ) : (s₁.append s₂).append s₃ = s₁.append fun (path₁ : s₁.Path) => (s₂ path₁).append fun (path₂ : (s₂ path₁).Path) => s₃ (append s₁ s₂ path₁ path₂)

Associativity of path-indexed tree grafting. The suffix continuation on the right is reindexed by the path obtained by appending the outer and middle paths.

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₂ : (FreeM.pure x).Path → P.FreeM β) (F : (path₁ : (FreeM.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.

Well-founded stopping trees

inductive PFunctor.FreeM.StoppingTree {St : Type z} (Obs : St → Type w) (step : (s : St) → Obs s → St) : St → Type (max w z)

Indexed W-type of stopping trees for a transition system observed through an arbitrary family Obs.

At each state s, an inhabitant either stops or extends and recurses into the next state selected by each observation obs : Obs s. Because done s is available at every state, inhabitation alone does not assert termination of the underlying transition system.

• done {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} (s : St) : StoppingTree Obs step s
• extend {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} (s : St) (cont : (obs : Obs s) → StoppingTree Obs step (step s obs)) : StoppingTree Obs step s

structure PFunctor.FreeM.StoppingTree.Algebra {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} (Carrier : St → Type t) : Type (max (max t w) z)

An algebra for the indexed polynomial y ↦ (fun s => PUnit ⊕ ((obs : Obs s) → y (step s obs))).

StoppingTree is its initial algebra: fold below is the unique algebra homomorphism into any such carrier family.

• done (s : St) : Carrier s

  Interpretation of a stopping leaf.

• extend (s : St) : ((obs : Obs s) → Carrier (step s obs)) → Carrier s

  Interpretation of one transition layer.

def PFunctor.FreeM.StoppingTree.fold {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} {Carrier : St → Type t} (alg : Algebra Carrier) {s : St} : StoppingTree Obs step s → Carrier s

The catamorphism from the initial stopping-tree algebra.

@[simp]

theorem PFunctor.FreeM.StoppingTree.fold_done {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} {Carrier : St → Type t} (alg : Algebra Carrier) (s : St) : fold alg (done s) = alg.done s

@[simp]

theorem PFunctor.FreeM.StoppingTree.fold_extend {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} {Carrier : St → Type t} (alg : Algebra Carrier) (s : St) (cont : (obs : Obs s) → StoppingTree Obs step (step s obs)) : fold alg (extend s cont) = alg.extend s fun (obs : Obs s) => fold alg (cont obs)

theorem PFunctor.FreeM.StoppingTree.eq_fold {St : Type z} {Obs : St → Type w} {step : (s : St) → Obs s → St} {Carrier : St → Type t} (alg : Algebra Carrier) (f : {s : St} → StoppingTree Obs step s → Carrier s) (hDone : ∀ (s : St), f (done s) = alg.done s) (hExtend : ∀ (s : St) (cont : (obs : Obs s) → StoppingTree Obs step (step s obs)), f (extend s cont) = alg.extend s fun (obs : Obs s) => f (cont obs)) {s : St} (tree : StoppingTree Obs step s) : f tree = fold alg tree

Uniqueness half of the initial-algebra universal property. Any function respecting done and extend agrees pointwise with fold.

@[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 round-indexed specialization of StoppingTree; users with a more compact observation type should use StoppingTree 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)