# mathlibdocumentation

data.pfunctor.multivariate.M

# The M construction as a multivariate polynomial functor. #

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

## Main definitions #

• M.mk - constructor
• M.dest - destructor
• M.corec - corecursor: useful for formulating infinite, productive computations
• M.bisim - bisimulation: proof technique to show the equality of infinite objects

## Implementation notes #

Dual view of M-types:

• Mp: polynomial functor
• M: greatest fixed point of a polynomial functor

Specifically, we define the polynomial functor Mp as:

• A := a possibly infinite tree-like structure without information in the nodes
• B := given the tree-like structure t, B t is a valid path from the root of t to any given node.

As a result Mp.obj α is made of a dataless tree and a function from its valid paths to values of α

The difference with the polynomial functor of an initial algebra is that A is a possibly infinite tree.

## Reference #

inductive mvpfunctor.M.path {n : } (P : mvpfunctor (n + 1)) :
P.last.Mfin2 nType u

A path from the root of a tree to one of its node

Instances for mvpfunctor.M.path
@[protected, instance]
def mvpfunctor.M.path.inhabited {n : } (P : mvpfunctor (n + 1)) (x : P.last.M) {i : fin2 n} [inhabited (P.drop.B x.head i)] :
Equations
def mvpfunctor.Mp {n : } (P : mvpfunctor (n + 1)) :

Polynomial functor of the M-type of P. A is a data-less possibly infinite tree whereas, for a given a : A, B a is a valid path in tree a so that Wp.obj α is made of a tree and a function from its valid paths to the values it contains

Equations
def mvpfunctor.M {n : } (P : mvpfunctor (n + 1)) (α : typevec n) :
Type u

n-ary M-type for P

Equations
Instances for mvpfunctor.M
@[protected, instance]
def mvpfunctor.mvfunctor_M {n : } (P : mvpfunctor (n + 1)) :
Equations
@[protected, instance]
def mvpfunctor.inhabited_M {n : } (P : mvpfunctor (n + 1)) {α : typevec n} [I : inhabited P.A] [Π (i : fin2 n), inhabited (α i)] :
inhabited (P.M α)
Equations
def mvpfunctor.M.corec_shape {n : } (P : mvpfunctor (n + 1)) {β : Type u} (g₀ : β → P.A) (g₂ : Π (b : β), P.last.B (g₀ b) → β) :
β → P.last.M

construct through corecursion the shape of an M-type without its contents

Equations
def mvpfunctor.cast_dropB {n : } (P : mvpfunctor (n + 1)) {a a' : P.A} (h : a = a') :
(P.drop.B a).arrow (P.drop.B a')

Proof of type equality as an arrow

Equations
def mvpfunctor.cast_lastB {n : } (P : mvpfunctor (n + 1)) {a a' : P.A} (h : a = a') :
P.last.B aP.last.B a'

Proof of type equality as a function

Equations
def mvpfunctor.M.corec_contents {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g₀ : β → P.A) (g₁ : Π (b : β), (P.drop.B (g₀ b)).arrow α) (g₂ : Π (b : β), P.last.B (g₀ b) → β) (x : P.last.M) (b : β) :
x = g₂ b α

Using corecursion, construct the contents of an M-type

Equations
def mvpfunctor.M.corec' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g₀ : β → P.A) (g₁ : Π (b : β), (P.drop.B (g₀ b)).arrow α) (g₂ : Π (b : β), P.last.B (g₀ b) → β) :
β → P.M α

Corecursor for M-type of P

Equations
• g₁ g₂ = λ (b : β), g₂ b, g₁ g₂ g₂ b) b _
def mvpfunctor.M.corec {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g : β → P.obj ::: β)) :
β → P.M α

Corecursor for M-type of P

Equations
def mvpfunctor.M.path_dest_left {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : x.dest = a, f⟩) (f' : α) :
(P.drop.B a).arrow α

Implementation of destructor for M-type of P

Equations
• = λ (i : fin2 n) (c : P.drop.B a i), f' i f h i c)
def mvpfunctor.M.path_dest_right {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : x.dest = a, f⟩) (f' : α) (j : P.last.B a) :
typevec.arrow (f j)) α

Implementation of destructor for M-type of P

Equations
• = λ (j : P.last.B a) (i : fin2 n) (c : (f j) i), f' i f h j i c)
def mvpfunctor.M.dest' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : x.dest = a, f⟩) (f' : α) :
P.obj ::: P.M α)

Destructor for M-type of P

Equations
def mvpfunctor.M.dest {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (x : P.M α) :
P.obj ::: P.M α)

Destructor for M-types

Equations
def mvpfunctor.M.mk {n : } (P : mvpfunctor (n + 1)) {α : typevec n} :
P.obj ::: P.M α)P.M α

Constructor for M-types

Equations
theorem mvpfunctor.M.dest'_eq_dest' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {x : P.last.M} {a₁ : P.A} {f₁ : P.last.B a₁ → P.last.M} (h₁ : x.dest = a₁, f₁⟩) {a₂ : P.A} {f₂ : P.last.B a₂ → P.last.M} (h₂ : x.dest = a₂, f₂⟩) (f' : α) :
f' = f'
theorem mvpfunctor.M.dest_eq_dest' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : x.dest = a, f⟩) (f' : α) :
x, f'⟩ = f'
theorem mvpfunctor.M.dest_corec' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g₀ : β → P.A) (g₁ : Π (b : β), (P.drop.B (g₀ b)).arrow α) (g₂ : Π (b : β), P.last.B (g₀ b) → β) (x : β) :
g₀ g₁ g₂ x) = g₀ x, typevec.split_fun (g₁ x) g₀ g₁ g₂ g₂ x)
theorem mvpfunctor.M.dest_corec {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g : β → P.obj ::: β)) (x : β) :
x) = (g x)
theorem mvpfunctor.M.bisim_lemma {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {a₁ : P.Mp.A} {f₁ : (P.Mp.B a₁).arrow α} {a' : P.A} {f' : (P.B a').drop.arrow α} {f₁' : (P.B a').lastP.M α} (e₁ : a₁, f₁⟩ = a', f₁') :
∃ (g₁' : P.last.B a' → P.last.M) (e₁' : = a', g₁'⟩), f' = f₁ f₁' = λ (x : P.last.B a'), g₁' x, f₁ x
theorem mvpfunctor.M.bisim {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (R : P.M αP.M α → Prop) (h : ∀ (x y : P.M α), R x y(∃ (a : P.A) (f : (P.B a).drop.arrow ::: P.M α).drop) (f₁ f₂ : (P.B a).last::: P.M α).last), = a, = a, ∀ (i : (P.B a).last), R (f₁ i) (f₂ i))) (x y : P.M α) (r : R x y) :
x = y
theorem mvpfunctor.M.bisim₀ {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (R : P.M αP.M α → Prop) (h₀ : equivalence R) (h : ∀ (x y : P.M α), R x ymvfunctor.map (typevec.id ::: quot.mk R) x) = mvfunctor.map (typevec.id ::: quot.mk R) y)) (x y : P.M α) (r : R x y) :
x = y
theorem mvpfunctor.M.bisim' {n : } (P : mvpfunctor (n + 1)) {α : typevec n} (R : P.M αP.M α → Prop) (h : ∀ (x y : P.M α), R x ymvfunctor.map (typevec.id ::: quot.mk R) x) = mvfunctor.map (typevec.id ::: quot.mk R) y)) (x y : P.M α) (r : R x y) :
x = y
theorem mvpfunctor.M.dest_map {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) (x : P.M α) :
x) = mvfunctor.map (g ::: λ (x : P.M α), x) x)
theorem mvpfunctor.M.map_dest {n : } (P : mvpfunctor (n + 1)) {α β : typevec n} (g : ::: P.M α).arrow ::: P.M β)) (x : P.M α) (h : ∀ (x : P.M α), ) :
x) =