# Documentation

Mathlib.Data.PFunctor.Univariate.M

# M-types #

M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.

inductive PFunctor.Approx.CofixA (F : PFunctor) :
Type u
• continue: {F : PFunctor} →
• intro: {F : PFunctor} → {n : } → (a : F.A) → () →

CofixA F n is an n level approximation of an M-type

Instances For

default inhabitant of CofixA

Equations
Instances For
theorem PFunctor.Approx.cofixA_eq_zero (F : PFunctor) (x : ) (y : ) :
x = y
def PFunctor.Approx.head' {F : PFunctor} {n : } :
F.A

The label of the root of the tree for a non-trivial approximation of the cofix of a pfunctor.

Instances For
def PFunctor.Approx.children' {F : PFunctor} {n : } (x : ) :

for a non-trivial approximation, return all the subtrees of the root

Instances For
inductive PFunctor.Approx.Agree {F : PFunctor} {n : } :
PFunctor.Approx.CofixA F (n + 1)Prop

Relation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated

Instances For
def PFunctor.Approx.AllAgree {F : PFunctor} (x : (n : ) → ) :

Given an infinite series of approximations approx, AllAgree approx states that they are all consistent with each other.

Instances For
@[simp]
theorem PFunctor.Approx.agree_trival {F : PFunctor} {x : } {y : } :
theorem PFunctor.Approx.agree_children {F : PFunctor} {n : } (x : ) (y : PFunctor.Approx.CofixA F ( + 1)) {i : } {j : } (h₀ : HEq i j) (h₁ : ) :

truncate a turns a into a more limited approximation

Equations
Instances For
theorem PFunctor.Approx.truncate_eq_of_agree {F : PFunctor} {n : } (x : ) (y : ) (h : ) :
def PFunctor.Approx.sCorec {F : PFunctor} {X : Type w} (f : X) :
X(n : ) →

sCorec f i n creates an approximation of height n of the final coalgebra of f

Equations
Instances For
theorem PFunctor.Approx.P_corec {F : PFunctor} {X : Type w} (f : X) (i : X) (n : ) :

Path F provides indices to access internal nodes in Corec F

Instances For
theorem PFunctor.Approx.head_succ' {F : PFunctor} (n : ) (m : ) (x : (n : ) → ) (Hconsistent : ) :
structure PFunctor.MIntl (F : PFunctor) :
• approx : (n : ) →

An n-th level approximation, for each depth n

• consistent : PFunctor.Approx.AllAgree s.approx

Each approximation agrees with the next

Internal definition for M. It is needed to avoid name clashes between M.mk and M.cases_on and the declarations generated for the structure

Instances For
def PFunctor.M (F : PFunctor) :

For polynomial functor F, M F is its final coalgebra

Instances For
theorem PFunctor.M.ext' (F : PFunctor) (x : ) (y : ) (H : ∀ (i : ), ) :
x = y
def PFunctor.M.corec {F : PFunctor} {X : Type u_1} (f : X) (i : X) :

Corecursor for the M-type defined by F.

Instances For
def PFunctor.M.head {F : PFunctor} (x : ) :
F.A

given a tree generated by F, head gives us the first piece of data it contains

Instances For
def PFunctor.M.children {F : PFunctor} (x : ) (i : ) :

return all the subtrees of the root of a tree x : M F

Instances For
def PFunctor.M.ichildren {F : PFunctor} [] [DecidableEq F.A] (i : ) (x : ) :

select a subtree using an i : F.Idx or return an arbitrary tree if i designates no subtree of x

Instances For
theorem PFunctor.M.head_succ {F : PFunctor} (n : ) (m : ) (x : ) :
theorem PFunctor.M.head_eq_head' {F : PFunctor} (x : ) (n : ) :
theorem PFunctor.M.head'_eq_head {F : PFunctor} (x : ) (n : ) :
theorem PFunctor.M.truncate_approx {F : PFunctor} (x : ) (n : ) :
def PFunctor.M.dest {F : PFunctor} :

unfold an M-type

Instances For
def PFunctor.M.Approx.sMk {F : PFunctor} (x : ) (n : ) :

generates the approximations needed for M.mk

Instances For
theorem PFunctor.M.Approx.P_mk {F : PFunctor} (x : ) :
def PFunctor.M.mk {F : PFunctor} (x : ) :

constructor for M-types

Instances For
inductive PFunctor.M.Agree' {F : PFunctor} :
Prop

Agree' n relates two trees of type M F that are the same up to depth n

Instances For
@[simp]
theorem PFunctor.M.dest_mk {F : PFunctor} (x : ) :
@[simp]
theorem PFunctor.M.mk_dest {F : PFunctor} (x : ) :
theorem PFunctor.M.mk_inj {F : PFunctor} {x : } {y : } (h : ) :
x = y
def PFunctor.M.cases {F : PFunctor} {r : Sort w} (f : (x : ) → r ()) (x : ) :
r x

destructor for M-types

Instances For
def PFunctor.M.casesOn {F : PFunctor} {r : Sort w} (x : ) (f : (x : ) → r ()) :
r x

destructor for M-types

Instances For
def PFunctor.M.casesOn' {F : PFunctor} {r : Sort w} (x : ) (f : (a : F.A) → (f : ) → r (PFunctor.M.mk { fst := a, snd := f })) :
r x

destructor for M-types, similar to casesOn but also gives access directly to the root and subtrees on an M-type

Instances For
theorem PFunctor.M.approx_mk {F : PFunctor} (a : F.A) (f : ) (i : ) :
@[simp]
theorem PFunctor.M.agree'_refl {F : PFunctor} {n : } (x : ) :
@[simp]
theorem PFunctor.M.cases_mk {F : PFunctor} {r : Sort u_2} (x : ) (f : (x : ) → r ()) :
= f x
@[simp]
theorem PFunctor.M.casesOn_mk {F : PFunctor} {r : Sort u_2} (x : ) (f : (x : ) → r ()) :
= f x
@[simp]
theorem PFunctor.M.casesOn_mk' {F : PFunctor} {r : Sort u_2} {a : F.A} (x : ) (f : (a : F.A) → (f : ) → r (PFunctor.M.mk { fst := a, snd := f })) :
PFunctor.M.casesOn' (PFunctor.M.mk { fst := a, snd := x }) f = f a x
inductive PFunctor.M.IsPath {F : PFunctor} :

IsPath p x tells us if p is a valid path through x

Instances For
theorem PFunctor.M.isPath_cons {F : PFunctor} {xs : } {a : F.A} {a' : F.A} {f : } {i : PFunctor.B F a'} :
PFunctor.M.IsPath ({ fst := a', snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f })a = a'
theorem PFunctor.M.isPath_cons' {F : PFunctor} {xs : } {a : F.A} {f : } {i : } :
PFunctor.M.IsPath ({ fst := a, snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f })PFunctor.M.IsPath xs (f i)
def PFunctor.M.isubtree {F : PFunctor} [DecidableEq F.A] [] :

follow a path through a value of M F and return the subtree found at the end of the path if it is a valid path for that value and return a default tree

Equations
• One or more equations did not get rendered due to their size.
• = x
Instances For
def PFunctor.M.iselect {F : PFunctor} [DecidableEq F.A] [] (ps : ) :
F.A

similar to isubtree but returns the data at the end of the path instead of the whole subtree

Instances For
theorem PFunctor.M.iselect_eq_default {F : PFunctor} [DecidableEq F.A] [] (ps : ) (x : ) (h : ¬) :
@[simp]
theorem PFunctor.M.head_mk {F : PFunctor} (x : ) :
= x.fst
theorem PFunctor.M.children_mk {F : PFunctor} {a : F.A} (x : ) (i : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x }))) :
PFunctor.M.children (PFunctor.M.mk { fst := a, snd := x }) i = x (cast (_ : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x })) = ) i)
@[simp]
theorem PFunctor.M.ichildren_mk {F : PFunctor} [DecidableEq F.A] [] (x : ) (i : ) :
@[simp]
theorem PFunctor.M.isubtree_cons {F : PFunctor} [DecidableEq F.A] [] (ps : ) {a : F.A} (f : ) {i : } :
PFunctor.M.isubtree ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.isubtree ps (f i)
@[simp]
theorem PFunctor.M.iselect_nil {F : PFunctor} [DecidableEq F.A] [] {a : F.A} (f : ) :
PFunctor.M.iselect [] (PFunctor.M.mk { fst := a, snd := f }) = a
@[simp]
theorem PFunctor.M.iselect_cons {F : PFunctor} [DecidableEq F.A] [] (ps : ) {a : F.A} (f : ) {i : } :
PFunctor.M.iselect ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.iselect ps (f i)
theorem PFunctor.M.corec_def {F : PFunctor} {X : Type u} (f : X) (x₀ : X) :
= PFunctor.M.mk ( <$> f x₀) theorem PFunctor.M.ext_aux {F : PFunctor} [] [DecidableEq F.A] {n : } (x : ) (y : ) (z : ) (hx : ) (hy : ) (hrec : ∀ (ps : ), n = = ) : theorem PFunctor.M.ext {F : PFunctor} [] (x : ) (y : ) (H : ∀ (ps : ), = ) : x = y structure PFunctor.M.IsBisimulation {F : PFunctor} (R : Prop) : • head : ∀ {a a' : F.A} {f : } {f' : PFunctor.B F a'}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a', snd := f' })a = a' The head of the trees are equal • tail : ∀ {a : F.A} {f f' : }, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a, snd := f' })∀ (i : ), R (f i) (f' i) The tails are equal Bisimulation is the standard proof technique for equality between infinite tree-like structures Instances For theorem PFunctor.M.nth_of_bisim {F : PFunctor} (R : Prop) [] (bisim : ) (s₁ : ) (s₂ : ) (ps : ) : R s₁ s₂ = a f f', = PFunctor.M.mk { fst := a, snd := f } = PFunctor.M.mk { fst := a, snd := f' } ((i : ) → R (f i) (f' i)) theorem PFunctor.M.eq_of_bisim {F : PFunctor} (R : Prop) [] (bisim : ) (s₁ : ) (s₂ : ) : R s₁ s₂s₁ = s₂ def PFunctor.M.corecOn {F : PFunctor} {X : Type u_2} (x₀ : X) (f : X) : corecursor for M F with swapped arguments Instances For theorem PFunctor.M.dest_corec {P : PFunctor} {α : Type u} (g : α) (x : α) : = <$> g x
theorem PFunctor.M.bisim {P : PFunctor} (R : Prop) (h : ∀ (x y : ), R x ya f f', = { fst := a, snd := f } = { fst := a, snd := f' } ((i : ) → R (f i) (f' i))) (x : ) (y : ) :
R x yx = y
theorem PFunctor.M.bisim' {P : PFunctor} {α : Type u_2} (Q : αProp) (u : α) (v : α) (h : ∀ (x : α), Q xa f f', PFunctor.M.dest (u x) = { fst := a, snd := f } PFunctor.M.dest (v x) = { fst := a, snd := f' } ∀ (i : ), x', Q x' f i = u x' f' i = v x') (x : α) :
Q xu x = v x
theorem PFunctor.M.bisim_equiv {P : PFunctor} (R : Prop) (h : ∀ (x y : ), R x ya f f', = { fst := a, snd := f } = { fst := a, snd := f' } ((i : ) → R (f i) (f' i))) (x : ) (y : ) :
R x yx = y
theorem PFunctor.M.corec_unique {P : PFunctor} {α : Type u} (g : α) (f : α) (hyp : ∀ (x : α), PFunctor.M.dest (f x) = f <\$> g x) :
def PFunctor.M.corec₁ {P : PFunctor} {α : Type u} (F : (X : Type u) → (αX) → α) :
α

corecursor where the state of the computation can be sent downstream in the form of a recursive call

Instances For
def PFunctor.M.corec' {P : PFunctor} {α : Type u} (F : {X : Type u} → (αX) → α ) (x : α) :

corecursor where it is possible to return a fully formed value at any point of the computation

Instances For