# Documentation

Mathlib.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 #

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
inductive MvPFunctor.M.Path {n : } (P : MvPFunctor (n + 1)) :
Fin2 nType u
• root: {n : } → {P : MvPFunctor (n + 1)} → (x : ) → (a : P.A) → (f : ) → = { fst := a, snd := f }(i : Fin2 n) →
• child: {n : } → {P : MvPFunctor (n + 1)} → (x : ) → (a : P.A) → (f : ) → = { fst := a, snd := f }(j : ) → (i : Fin2 n) → MvPFunctor.M.Path P (f j) i

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

Instances For
instance MvPFunctor.M.Path.inhabited {n : } (P : MvPFunctor (n + 1)) (x : ) {i : Fin2 n} [Inhabited ()] :
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 mp.Obj α is made of a tree and a function from its valid paths to the values it contains

Instances For
def MvPFunctor.M {n : } (P : MvPFunctor (n + 1)) (α : ) :

n-ary M-type for P

Instances For
instance MvPFunctor.mvfunctorM {n : } (P : MvPFunctor (n + 1)) :
instance MvPFunctor.inhabitedM {n : } (P : MvPFunctor (n + 1)) {α : } [I : Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
def MvPFunctor.M.corecShape {n : } (P : MvPFunctor (n + 1)) {β : Type u} (g₀ : βP.A) (g₂ : (b : β) → PFunctor.B () (g₀ b)β) :
β

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

Instances For
def MvPFunctor.castDropB {n : } (P : MvPFunctor (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :

Proof of type equality as an arrow

Instances For
def MvPFunctor.castLastB {n : } (P : MvPFunctor (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :

Proof of type equality as a function

Instances For
def MvPFunctor.M.corecContents {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B () (g₀ b)) α) (g₂ : (b : β) → PFunctor.B () (g₀ b)β) (x : ) (b : β) (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) :

Using corecursion, construct the contents of an M-type

Equations
Instances For
def MvPFunctor.M.corec' {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B () (g₀ b)) α) (g₂ : (b : β) → PFunctor.B () (g₀ b)β) :
β

Corecursor for M-type of P

Instances For
def MvPFunctor.M.corec {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (g : βMvPFunctor.Obj P (α ::: β)) :
β

Corecursor for M-type of P

Instances For
def MvPFunctor.M.pathDestLeft {n : } (P : MvPFunctor (n + 1)) {α : } {x : } {a : P.A} {f : } (h : = { fst := a, snd := f }) (f' : ) :

Implementation of destructor for M-type of P

Instances For
def MvPFunctor.M.pathDestRight {n : } (P : MvPFunctor (n + 1)) {α : } {x : } {a : P.A} {f : } (h : = { fst := a, snd := f }) (f' : ) (j : ) :

Implementation of destructor for M-type of P

Instances For
def MvPFunctor.M.dest' {n : } (P : MvPFunctor (n + 1)) {α : } {x : } {a : P.A} {f : } (h : = { fst := a, snd := f }) (f' : ) :

Destructor for M-type of P

Instances For
def MvPFunctor.M.dest {n : } (P : MvPFunctor (n + 1)) {α : } (x : ) :

Destructor for M-types

Instances For
def MvPFunctor.M.mk {n : } (P : MvPFunctor (n + 1)) {α : } :
MvPFunctor.Obj P (α ::: )

Constructor for M-types

Instances For
theorem MvPFunctor.M.dest'_eq_dest' {n : } (P : MvPFunctor (n + 1)) {α : } {x : } {a₁ : P.A} {f₁ : } (h₁ : = { fst := a₁, snd := f₁ }) {a₂ : P.A} {f₂ : } (h₂ : = { fst := a₂, snd := f₂ }) (f' : ) :
theorem MvPFunctor.M.dest_eq_dest' {n : } (P : MvPFunctor (n + 1)) {α : } {x : } {a : P.A} {f : } (h : = { fst := a, snd := f }) (f' : ) :
MvPFunctor.M.dest P { fst := x, snd := f' } =
theorem MvPFunctor.M.dest_corec' {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B () (g₀ b)) α) (g₂ : (b : β) → PFunctor.B () (g₀ b)β) (x : β) :
MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) = { fst := g₀ x, snd := TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ g₂ x) }
theorem MvPFunctor.M.dest_corec {n : } (P : MvPFunctor (n + 1)) {α : } {β : Type u} (g : βMvPFunctor.Obj P (α ::: β)) (x : β) :
MvPFunctor.M.dest P () = MvFunctor.map (TypeVec.id ::: ) (g x)
theorem MvPFunctor.M.bisim_lemma {n : } (P : MvPFunctor (n + 1)) {α : } {a₁ : ().A} {f₁ : TypeVec.Arrow () α} {a' : P.A} {f' : TypeVec.Arrow (TypeVec.drop (MvPFunctor.B P a')) α} {f₁' : TypeVec.last (MvPFunctor.B P a')} (e₁ : MvPFunctor.M.dest P { fst := a₁, snd := f₁ } = { fst := a', snd := TypeVec.splitFun f' f₁' }) :
g₁' e₁', f' = f₁' = fun x => { fst := g₁' x, snd := MvPFunctor.M.pathDestRight P e₁' f₁ x }
theorem MvPFunctor.M.bisim {n : } (P : MvPFunctor (n + 1)) {α : } (R : Prop) (h : ∀ (x y : ), R x ya f f₁ f₂, = { fst := a, snd := } = { fst := a, snd := } ((i : TypeVec.last ()) → R (f₁ i) (f₂ i))) (x : ) (y : ) (r : R x y) :
x = y
theorem MvPFunctor.M.bisim₀ {n : } (P : MvPFunctor (n + 1)) {α : } (R : Prop) (h₀ : ) (h : ∀ (x y : ), R x yMvFunctor.map (TypeVec.id ::: ) () = MvFunctor.map (TypeVec.id ::: ) ()) (x : ) (y : ) (r : R x y) :
x = y
theorem MvPFunctor.M.bisim' {n : } (P : MvPFunctor (n + 1)) {α : } (R : Prop) (h : ∀ (x y : ), R x yMvFunctor.map (TypeVec.id ::: ) () = MvFunctor.map (TypeVec.id ::: ) ()) (x : ) (y : ) (r : R x y) :
x = y
theorem MvPFunctor.M.dest_map {n : } (P : MvPFunctor (n + 1)) {α : } {β : } (g : ) (x : ) :
= MvFunctor.map (g ::: fun x => ) ()
theorem MvPFunctor.M.map_dest {n : } (P : MvPFunctor (n + 1)) {α : } {β : } (g : TypeVec.Arrow (α ::: ) (β ::: )) (x : ) (h : ∀ (x : ), = ) :
=