The M construction as a multivariate polynomial functor. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

inductive mvpfunctor.M.path {n : ℕ} (P : mvpfunctor (n + 1)) :

P.last.M → fin2 n → Type u

root : Π {n : ℕ} {P : mvpfunctor (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M), x.dest = ⟨a, f⟩ → Π (i : fin2 n), P.drop.B a i → mvpfunctor.M.path P x i
child : Π {n : ℕ} {P : mvpfunctor (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M), x.dest = ⟨a, f⟩ → Π (j : P.last.B a) (i : fin2 n), mvpfunctor.M.path P (f j) i → mvpfunctor.M.path P x i

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

Instances for mvpfunctor.M.path

mvpfunctor.M.path.has_sizeof_inst
mvpfunctor.M.path.inhabited

source

@[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)] :

inhabited (mvpfunctor.M.path P x i)

Equations

mvpfunctor.M.path.inhabited P x = {default := mvpfunctor.M.path.root x x.head x.children _ i inhabited.default}

source

def mvpfunctor.Mp {n : ℕ} (P : mvpfunctor (n + 1)) :

mvpfunctor n

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

P.Mp = {A := P.last.M, B := mvpfunctor.M.path P}

source

def mvpfunctor.M {n : ℕ} (P : mvpfunctor (n + 1)) (α : typevec n) :

Type u

n-ary M-type for P

Equations

P.M α = P.Mp.obj α

Instances for mvpfunctor.M

source

@[protected, instance]

def mvpfunctor.mvfunctor_M {n : ℕ} (P : mvpfunctor (n + 1)) :

mvfunctor P.M

Equations

P.mvfunctor_M = id (mvpfunctor.obj.mvfunctor P.Mp)

source

@[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

P.inhabited_M = mvpfunctor.obj.inhabited P.Mp

source

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

mvpfunctor.M.corec_shape P g₀ g₂ = pfunctor.M.corec (λ (b : β), ⟨g₀ b, g₂ b⟩)

source

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

P.cast_dropB h = λ (i : fin2 n) (b : P.drop.B a i), h.rec_on b

source

def mvpfunctor.cast_lastB {n : ℕ} (P : mvpfunctor (n + 1)) {a a' : P.A} (h : a = a') :

P.last.B a → P.last.B a'

Proof of type equality as a function

Equations

P.cast_lastB h = λ (b : P.last.B a), h.rec_on b

source

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 = mvpfunctor.M.corec_shape P g₀ g₂ b → typevec.arrow (mvpfunctor.M.path P x) α

Using corecursion, construct the contents of an M-type

Equations

mvpfunctor.M.corec_contents P g₀ g₁ g₂ x b h i (mvpfunctor.M.path.child x a f h' j i c) = have h₀ : a = g₀ b, from _, have h₁ : f j = mvpfunctor.M.corec_shape P g₀ g₂ (g₂ b (P.cast_lastB h₀ j)), from _, mvpfunctor.M.corec_contents P g₀ g₁ g₂ (f j) (g₂ b (P.cast_lastB h₀ j)) h₁ i c
mvpfunctor.M.corec_contents P g₀ g₁ g₂ x b h i (mvpfunctor.M.path.root x a f h' i c) = have this : a = g₀ b, from _, g₁ b i (P.cast_dropB this i c)

source

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

mvpfunctor.M.corec' P g₀ g₁ g₂ = λ (b : β), ⟨mvpfunctor.M.corec_shape P g₀ g₂ b, mvpfunctor.M.corec_contents P g₀ g₁ g₂ (mvpfunctor.M.corec_shape P g₀ g₂ b) b _⟩

source

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

mvpfunctor.M.corec P g = mvpfunctor.M.corec' P (λ (b : β), (g b).fst) (λ (b : β), typevec.drop_fun (g b).snd) (λ (b : β), typevec.last_fun (g b).snd)

source

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' : typevec.arrow (mvpfunctor.M.path P x) α) :

(P.drop.B a).arrow α

Implementation of destructor for M-type of P

Equations

mvpfunctor.M.path_dest_left P h f' = λ (i : fin2 n) (c : P.drop.B a i), f' i (mvpfunctor.M.path.root x a f h i c)

source

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' : typevec.arrow (mvpfunctor.M.path P x) α) (j : P.last.B a) :

typevec.arrow (mvpfunctor.M.path P (f j)) α

Implementation of destructor for M-type of P

Equations

mvpfunctor.M.path_dest_right P h f' = λ (j : P.last.B a) (i : fin2 n) (c : mvpfunctor.M.path P (f j) i), f' i (mvpfunctor.M.path.child x a f h j i c)

source

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' : typevec.arrow (mvpfunctor.M.path P x) α) :

P.obj (α ::: P.M α)

Destructor for M-type of P

Equations

mvpfunctor.M.dest' P h f' = ⟨a, typevec.split_fun (mvpfunctor.M.path_dest_left P h f') (λ (x_1 : (P.B a).last), ⟨f x_1, mvpfunctor.M.path_dest_right P h f' x_1⟩)⟩

source

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

P.obj (α ::: P.M α)

Destructor for M-types

Equations

mvpfunctor.M.dest P x = mvpfunctor.M.dest' P _ x.snd

source

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

P.obj (α ::: P.M α) → P.M α

Constructor for M-types

Equations

mvpfunctor.M.mk P = mvpfunctor.M.corec P (λ (i : P.obj (α ::: P.M α)), mvfunctor.map (typevec.id ::: mvpfunctor.M.dest P) i)

source

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' : typevec.arrow (mvpfunctor.M.path P x) α) :

mvpfunctor.M.dest' P h₁ f' = mvpfunctor.M.dest' P h₂ f'

source

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' : typevec.arrow (mvpfunctor.M.path P x) α) :

mvpfunctor.M.dest P ⟨x, f'⟩ = mvpfunctor.M.dest' P h f'

source

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 : β) :

mvpfunctor.M.dest P (mvpfunctor.M.corec' P g₀ g₁ g₂ x) = ⟨g₀ x, typevec.split_fun (g₁ x) (mvpfunctor.M.corec' P g₀ g₁ g₂ ∘ g₂ x)⟩

source

theorem mvpfunctor.M.dest_corec {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (g : β → P.obj (α ::: β)) (x : β) :

mvpfunctor.M.dest P (mvpfunctor.M.corec P g x) = mvfunctor.map (typevec.id ::: mvpfunctor.M.corec P g) (g x)

source

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').last → P.M α} (e₁ : mvpfunctor.M.dest P ⟨a₁, f₁⟩ = ⟨a', typevec.split_fun f' f₁'⟩) :

∃ (g₁' : P.last.B a' → P.last.M) (e₁' : pfunctor.M.dest a₁ = ⟨a', g₁'⟩), f' = mvpfunctor.M.path_dest_left P e₁' f₁ ∧ f₁' = λ (x : P.last.B a'), ⟨g₁' x, mvpfunctor.M.path_dest_right P e₁' f₁ x⟩

source

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), mvpfunctor.M.dest P x = ⟨a, typevec.split_fun f f₁⟩ ∧ mvpfunctor.M.dest P y = ⟨a, typevec.split_fun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i))) (x y : P.M α) (r : R x y) :

x = y

source

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 y → mvfunctor.map (typevec.id ::: quot.mk R) (mvpfunctor.M.dest P x) = mvfunctor.map (typevec.id ::: quot.mk R) (mvpfunctor.M.dest P y)) (x y : P.M α) (r : R x y) :

x = y

source

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 → mvfunctor.map (typevec.id ::: quot.mk R) (mvpfunctor.M.dest P x) = mvfunctor.map (typevec.id ::: quot.mk R) (mvpfunctor.M.dest P y)) (x y : P.M α) (r : R x y) :

x = y

source

theorem mvpfunctor.M.dest_map {n : ℕ} (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) (x : P.M α) :

mvpfunctor.M.dest P (mvfunctor.map g x) = mvfunctor.map (g ::: λ (x : P.M α), mvfunctor.map g x) (mvpfunctor.M.dest P x)

source

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 α), typevec.last_fun g x = mvfunctor.map (typevec.drop_fun g) x) :

mvfunctor.map g (mvpfunctor.M.dest P x) = mvpfunctor.M.dest P (mvfunctor.map (typevec.drop_fun g) x)