# mathlibdocumentation

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.cofix_a  :
pfunctorType u

cofix_a F n is an n level approximation of a M-type

default inhabitant of cofix_a

Equations
@[instance]

Equations
theorem pfunctor.approx.cofix_a_eq_zero (F : pfunctor) (x y : 0) :
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.

Equations
def pfunctor.approx.children' {F : pfunctor} {n : } (x : n.succ) :
F.B

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

Equations
theorem pfunctor.approx.approx_eta {F : pfunctor} {n : } (x : (n + 1)) :

inductive pfunctor.approx.agree {F : pfunctor} {n : } :
(n + 1) → Prop
• continue : ∀ {F : pfunctor} (x : (y : ,
• intro : ∀ {F : pfunctor} {n : } {a : F.A} (x : F.B a (x' : F.B a (n + 1)), (∀ (i : F.B a), (x' i))

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

def pfunctor.approx.all_agree {F : pfunctor} :
(Π (n : ), → Prop

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

Equations
@[simp]
theorem pfunctor.approx.agree_trival {F : pfunctor} {x : 0} {y : 1} :

theorem pfunctor.approx.agree_children {F : pfunctor} {n : } (x : n.succ) (y : (n.succ + 1)) {i : F.B } {j : F.B } :
i == j

def pfunctor.approx.truncate {F : pfunctor} {n : } :
(n + 1)

truncate a turns a into a more limited approximation

Equations
theorem pfunctor.approx.truncate_eq_of_agree {F : pfunctor} {n : } (x : n) (y : n.succ) :

def pfunctor.approx.s_corec {F : pfunctor} {X : Type w} (f : X → F.obj X) (i : X) (n : ) :

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

Equations
• = (λ (i : F.B (f j).fst), ((f j).snd i) n)
theorem pfunctor.approx.P_corec {F : pfunctor} {X : Type w} (f : X → F.obj X) (i : X) (n : ) :
n.succ)

def pfunctor.approx.path  :
pfunctorType u

path F provides indices to access internal nodes in corec F

Equations
@[instance]

Equations
@[instance]

theorem pfunctor.approx.head_succ' {F : pfunctor} (n m : ) (x : Π (n : ), ) :
=

structure pfunctor.M_intl  :
pfunctorType u
• approx : Π (n : ),
• consistent :

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

def pfunctor.M  :
pfunctorType u

For polynomial functor F, M F is its final coalgebra

Equations
@[instance]

Equations
@[instance]

Equations
• = show , from
theorem pfunctor.M.ext' (F : pfunctor) (x y : F.M) :
(∀ (i : ), x.approx i = y.approx i)x = y

def pfunctor.M.corec {F : pfunctor} {X : Type u_1} :
(X → F.obj X)X → F.M

Corecursor for the M-type defined by F.

Equations
def pfunctor.M.head {F : pfunctor} :
F.M → F.A

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

Equations
def pfunctor.M.children {F : pfunctor} (x : F.M) :

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

Equations
def pfunctor.M.ichildren {F : pfunctor} [inhabited F.M] [decidable_eq F.A] :
F.IdxF.M → F.M

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

Equations
theorem pfunctor.M.head_succ {F : pfunctor} (n m : ) (x : F.M) :
=

theorem pfunctor.M.head_eq_head' {F : pfunctor} (x : F.M) (n : ) :

theorem pfunctor.M.head'_eq_head {F : pfunctor} (x : F.M) (n : ) :

theorem pfunctor.M.truncate_approx {F : pfunctor} (x : F.M) (n : ) :

def pfunctor.M.dest {F : pfunctor} :
F.MF.obj F.M

unfold an M-type

Equations
def pfunctor.M.approx.s_mk {F : pfunctor} (x : F.obj F.M) (n : ) :

generates the approximations needed for M.mk

Equations
theorem pfunctor.M.approx.P_mk {F : pfunctor} (x : F.obj F.M) :

def pfunctor.M.mk {F : pfunctor} :
F.obj F.M → F.M

constructor for M-types

Equations
inductive pfunctor.M.agree' {F : pfunctor} :
F.MF.M → Prop

agree' n relates two trees of type M F that are the same up to dept n

@[simp]
theorem pfunctor.M.dest_mk {F : pfunctor} (x : F.obj F.M) :
.dest = x

@[simp]
theorem pfunctor.M.mk_dest {F : pfunctor} (x : F.M) :

theorem pfunctor.M.mk_inj {F : pfunctor} {x y : F.obj F.M} :
x = y

def pfunctor.M.cases {F : pfunctor} {r : F.MSort w} (f : Π (x : F.obj F.M), r ) (x : F.M) :
r x

destructor for M-types

Equations
def pfunctor.M.cases_on {F : pfunctor} {r : F.MSort w} (x : F.M) :
(Π (x : F.obj F.M), r (pfunctor.M.mk x))r x

destructor for M-types

Equations
def pfunctor.M.cases_on' {F : pfunctor} {r : F.MSort w} (x : F.M) :
(Π (a : F.A) (f : F.B a → F.M), r (pfunctor.M.mk a, f⟩))r x

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

Equations
• x.cases_on' f = x.cases_on (λ (_x : F.obj F.M), pfunctor.M.cases_on'._match_1 f _x)
• pfunctor.M.cases_on'._match_1 f a, g⟩ = f a g
theorem pfunctor.M.approx_mk {F : pfunctor} (a : F.A) (f : F.B a → F.M) (i : ) :
(pfunctor.M.mk a, f⟩).approx i.succ = (λ (j : F.B a), (f j).approx i)

@[simp]
theorem pfunctor.M.agree'_refl {F : pfunctor} {n : } (x : F.M) :
x

theorem pfunctor.M.agree_iff_agree' {F : pfunctor} {n : } (x y : F.M) :
(y.approx (n + 1)) y

@[simp]
theorem pfunctor.M.cases_mk {F : pfunctor} {r : F.MSort u_1} (x : F.obj F.M) (f : Π (x : F.obj F.M), r ) :
= f x

@[simp]
theorem pfunctor.M.cases_on_mk {F : pfunctor} {r : F.MSort u_1} (x : F.obj F.M) (f : Π (x : F.obj F.M), r ) :
f = f x

@[simp]
theorem pfunctor.M.cases_on_mk' {F : pfunctor} {r : F.MSort u_1} {a : F.A} (x : F.B a → F.M) (f : Π (a : F.A) (f : F.B a → F.M), r (pfunctor.M.mk a, f⟩)) :
(pfunctor.M.mk a, x⟩).cases_on' f = f a x

inductive pfunctor.M.is_path {F : pfunctor} :
F.M → Prop

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

theorem pfunctor.M.is_path_cons {F : pfunctor} {xs : pfunctor.approx.path F} {a a' : F.A} {f : F.B a → F.M} {i : F.B a'} :
pfunctor.M.is_path (a', i⟩ :: xs) (pfunctor.M.mk a, f⟩)a = a'

theorem pfunctor.M.is_path_cons' {F : pfunctor} {xs : pfunctor.approx.path F} {a : F.A} {f : F.B a → F.M} {i : F.B a} :
pfunctor.M.is_path (a, i⟩ :: xs) (pfunctor.M.mk a, f⟩) (f i)

def pfunctor.M.isubtree {F : pfunctor} [decidable_eq F.A] [inhabited F.M] :
F.M → F.M

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
def pfunctor.M.iselect {F : pfunctor} [decidable_eq F.A] [inhabited F.M] :
F.M → F.A

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

Equations
@[simp]
theorem pfunctor.M.head_mk {F : pfunctor} (x : F.obj F.M) :

theorem pfunctor.M.children_mk {F : pfunctor} {a : F.A} (x : F.B a → F.M) (i : F.B (pfunctor.M.mk a, x⟩).head) :
(pfunctor.M.mk a, x⟩).children i = x (cast _ i)

@[simp]
theorem pfunctor.M.ichildren_mk {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (x : F.obj F.M) (i : F.Idx) :
= x.iget i

@[simp]
theorem pfunctor.M.isubtree_cons {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (ps : pfunctor.approx.path F) {a : F.A} (f : F.B a → F.M) {i : F.B a} :
pfunctor.M.isubtree (a, i⟩ :: ps) (pfunctor.M.mk a, f⟩) = (f i)

@[simp]
theorem pfunctor.M.iselect_nil {F : pfunctor} [decidable_eq F.A] [inhabited F.M] {a : F.A} (f : F.B a → F.M) :
= a

@[simp]
theorem pfunctor.M.iselect_cons {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (ps : pfunctor.approx.path F) {a : F.A} (f : F.B a → F.M) {i : F.B a} :
pfunctor.M.iselect (a, i⟩ :: ps) (pfunctor.M.mk a, f⟩) = (f i)

theorem pfunctor.M.corec_def {F : pfunctor} {X : Type u} (f : X → F.obj X) (x₀ : X) :
x₀ = pfunctor.M.mk <$> f x₀) theorem pfunctor.M.ext_aux {F : pfunctor} [inhabited F.M] [decidable_eq F.A] {n : } (x y z : F.M) : x y(∀ (ps : , n = = y)x.approx (n + 1) = y.approx (n + 1) theorem pfunctor.M.ext {F : pfunctor} [inhabited F.M] (x y : F.M) : (∀ (ps : , = y)x = y structure pfunctor.M.is_bisimulation {F : pfunctor} : (F.MF.M → Prop) → Prop Bisimulation is the standard proof technique for equality between infinite tree-like structures theorem pfunctor.M.nth_of_bisim {F : pfunctor} (R : F.MF.M → Prop) [inhabited F.M] (bisim : pfunctor.M.is_bisimulation R) (s₁ s₂ : F.M) (ps : pfunctor.approx.path F) : R s₁ s₂ s₁ s₂ s₁ = s₂ ∃ (a : F.A) (f f' : F.B a → F.M), s₁ = pfunctor.M.mk a, f⟩ s₂ = pfunctor.M.mk a, f'⟩ ∀ (i : F.B a), R (f i) (f' i)) theorem pfunctor.M.eq_of_bisim {F : pfunctor} (R : F.MF.M → Prop) [nonempty F.M] (bisim : pfunctor.M.is_bisimulation R) (s₁ s₂ : F.M) : R s₁ s₂s₁ = s₂ def pfunctor.M.corec_on {F : pfunctor} {X : Type u_1} : X → (X → F.obj X) → F.M corecursor for M F with swapped arguments Equations • = x₀ theorem pfunctor.M.dest_corec {P : pfunctor} {α : Type u} (g : α → P.obj α) (x : α) : x).dest = <$> g x

theorem pfunctor.M.bisim {P : pfunctor} (R : P.MP.M → Prop) (h : ∀ (x y : P.M), R x y(∃ (a : P.A) (f f' : P.B a → P.M), x.dest = a, f⟩ y.dest = a, f'⟩ ∀ (i : P.B a), R (f i) (f' i))) (x y : P.M) :
R x yx = y

theorem pfunctor.M.bisim' {P : pfunctor} {α : Type u_1} (Q : α → Prop) (u v : α → P.M) (h : ∀ (x : α), Q x(∃ (a : P.A) (f f' : P.B a → P.M), (u x).dest = a, f⟩ (v x).dest = a, f'⟩ ∀ (i : P.B a), ∃ (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 : P.MP.M → Prop) (h : ∀ (x y : P.M), R x y(∃ (a : P.A) (f f' : P.B a → P.M), x.dest = a, f⟩ y.dest = a, f'⟩ ∀ (i : P.B a), R (f i) (f' i))) (x y : P.M) :
R x yx = y

theorem pfunctor.M.corec_unique {P : pfunctor} {α : Type u} (g : α → P.obj α) (f : α → P.M) :
(∀ (x : α), (f x).dest = f <\$> g x)

def pfunctor.M.corec₁ {P : pfunctor} {α : Type u} :
(Π (X : Type u), (α → X)α → P.obj X)α → P.M

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

Equations
def pfunctor.M.corec' {P : pfunctor} {α : Type u} :
(Π {X : Type u}, (α → X)α → P.M P.obj X)α → P.M

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

Equations