# M-types #

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

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

Instances For

default inhabitant of CofixA

Equations
Instances For
Equations
• = { default := }
theorem PFunctor.Approx.cofixA_eq_zero (F : PFunctor.{u}) (x : ) (y : ) :
x = y

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

Equations
• = match x✝, x with | x, => i
Instances For
def PFunctor.Approx.children' {F : PFunctor.{u}} {n : } (x : PFunctor.Approx.CofixA F n.succ) :
F.B

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
inductive PFunctor.Approx.Agree {F : PFunctor.{u}} {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.{u}} (x : (n : ) → ) :

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

Equations
Instances For
@[simp]
theorem PFunctor.Approx.agree_trival {F : PFunctor.{u}} {x : } {y : } :
theorem PFunctor.Approx.agree_children {F : PFunctor.{u}} {n : } (x : PFunctor.Approx.CofixA F n.succ) (y : PFunctor.Approx.CofixA F (n.succ + 1)) {i : F.B } {j : F.B } (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.{u}} {n : } (x : ) (y : PFunctor.Approx.CofixA F n.succ) (h : ) :
def PFunctor.Approx.sCorec {F : PFunctor.{u}} {X : Type w} (f : XF 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.{u}} {X : Type w} (f : XF X) (i : X) (n : ) :

Path F provides indices to access internal nodes in Corec F

Equations
Instances For
Equations
• PFunctor.Approx.Path.inhabited = { default := [] }
theorem PFunctor.Approx.head_succ' {F : PFunctor.{u}} (n : ) (m : ) (x : (n : ) → ) (Hconsistent : ) :
structure PFunctor.MIntl (F : PFunctor.{u}) :

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

• approx : (n : ) →

An n-th level approximation, for each depth n

• consistent : PFunctor.Approx.AllAgree self.approx

Each approximation agrees with the next

Instances For
theorem PFunctor.MIntl.consistent {F : PFunctor.{u}} (self : F.MIntl) :

Each approximation agrees with the next

For polynomial functor F, M F is its final coalgebra

Equations
• F.M = F.MIntl
Instances For
Equations
• = { default := { approx := default, consistent := } }
Equations
• = let_fun this := inferInstance; this
theorem PFunctor.M.ext' (F : PFunctor.{u}) (x : F.M) (y : F.M) (H : ∀ (i : ), x.approx i = y.approx i) :
x = y
def PFunctor.M.corec {F : PFunctor.{u}} {X : Type u_1} (f : XF X) (i : X) :
F.M

Corecursor for the M-type defined by F.

Equations
• = { approx := , consistent := }
Instances For
def PFunctor.M.head {F : PFunctor.{u}} (x : F.M) :
F.A

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

Equations
Instances For
def PFunctor.M.children {F : PFunctor.{u}} (x : F.M) (i : F.B x.head) :
F.M

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

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

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

Equations
• = if H' : i.fst = x.head then x.children (cast i.snd) else default
Instances For
theorem PFunctor.M.head_succ {F : PFunctor.{u}} (n : ) (m : ) (x : F.M) :
theorem PFunctor.M.head_eq_head' {F : PFunctor.{u}} (x : F.M) (n : ) :
theorem PFunctor.M.head'_eq_head {F : PFunctor.{u}} (x : F.M) (n : ) :
theorem PFunctor.M.truncate_approx {F : PFunctor.{u}} (x : F.M) (n : ) :
PFunctor.Approx.truncate (x.approx (n + 1)) = x.approx n
def PFunctor.M.dest {F : PFunctor.{u}} :
F.MF F.M

unfold an M-type

Equations
• x.dest = let x := x; x.head, fun (i : F.B x.head) => x.children i
Instances For
def PFunctor.M.Approx.sMk {F : PFunctor.{u}} (x : F F.M) (n : ) :

generates the approximations needed for M.mk

Equations
• = match x with | 0 => PFunctor.Approx.CofixA.continue | n.succ => PFunctor.Approx.CofixA.intro x✝.fst fun (i : F.B x✝.fst) => (x✝.snd i).approx n
Instances For
theorem PFunctor.M.Approx.P_mk {F : PFunctor.{u}} (x : F F.M) :
def PFunctor.M.mk {F : PFunctor.{u}} (x : F F.M) :
F.M

constructor for M-types

Equations
• = { approx := , consistent := }
Instances For
inductive PFunctor.M.Agree' {F : PFunctor.{u}} :
F.MF.MProp

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.{u}} (x : F F.M) :
().dest = x
@[simp]
theorem PFunctor.M.mk_dest {F : PFunctor.{u}} (x : F.M) :
PFunctor.M.mk x.dest = x
theorem PFunctor.M.mk_inj {F : PFunctor.{u}} {x : F F.M} {y : F F.M} (h : ) :
x = y
def PFunctor.M.cases {F : PFunctor.{u}} {r : F.MSort w} (f : (x : F F.M) → r ()) (x : F.M) :
r x

destructor for M-types

Equations
• = let_fun this := f x.dest; .mpr this
Instances For
def PFunctor.M.casesOn {F : PFunctor.{u}} {r : F.MSort w} (x : F.M) (f : (x : F F.M) → r ()) :
r x

destructor for M-types

Equations
• x.casesOn f =
Instances For
def PFunctor.M.casesOn' {F : PFunctor.{u}} {r : F.MSort w} (x : F.M) (f : (a : F.A) → (f : F.B aF.M) → r (PFunctor.M.mk a, f)) :
r x

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

Equations
• x.casesOn' f = x.casesOn fun (x : F F.M) => match x with | a, g => f a g
Instances For
theorem PFunctor.M.approx_mk {F : PFunctor.{u}} (a : F.A) (f : F.B aF.M) (i : ) :
(PFunctor.M.mk a, f).approx i.succ = PFunctor.Approx.CofixA.intro a fun (j : F.B a) => (f j).approx i
@[simp]
theorem PFunctor.M.agree'_refl {F : PFunctor.{u}} {n : } (x : F.M) :
theorem PFunctor.M.agree_iff_agree' {F : PFunctor.{u}} {n : } (x : F.M) (y : F.M) :
PFunctor.Approx.Agree (x.approx n) (y.approx (n + 1))
@[simp]
theorem PFunctor.M.cases_mk {F : PFunctor.{u}} {r : F.MSort u_2} (x : F F.M) (f : (x : F F.M) → r ()) :
= f x
@[simp]
theorem PFunctor.M.casesOn_mk {F : PFunctor.{u}} {r : F.MSort u_2} (x : F F.M) (f : (x : F F.M) → r ()) :
().casesOn f = f x
@[simp]
theorem PFunctor.M.casesOn_mk' {F : PFunctor.{u}} {r : F.MSort u_2} {a : F.A} (x : F.B aF.M) (f : (a : F.A) → (f : F.B aF.M) → r (PFunctor.M.mk a, f)) :
(PFunctor.M.mk a, x).casesOn' f = f a x
inductive PFunctor.M.IsPath {F : PFunctor.{u}} :
F.MProp

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

Instances For
theorem PFunctor.M.isPath_cons {F : PFunctor.{u}} {xs : } {a : F.A} {a' : F.A} {f : F.B aF.M} {i : F.B a'} :
PFunctor.M.IsPath (a', i :: xs) (PFunctor.M.mk a, f)a = a'
theorem PFunctor.M.isPath_cons' {F : PFunctor.{u}} {xs : } {a : F.A} {f : F.B aF.M} {i : F.B a} :
PFunctor.M.IsPath (a, i :: xs) (PFunctor.M.mk a, f)PFunctor.M.IsPath xs (f i)
def PFunctor.M.isubtree {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] :
F.MF.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
Instances For
def PFunctor.M.iselect {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] (ps : ) :
F.MF.A

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

Equations
Instances For
theorem PFunctor.M.iselect_eq_default {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] (ps : ) (x : F.M) (h : ¬) :
@[simp]
theorem PFunctor.M.head_mk {F : PFunctor.{u}} (x : F F.M) :
theorem PFunctor.M.children_mk {F : PFunctor.{u}} {a : F.A} (x : F.B aF.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.{u}} [DecidableEq F.A] [Inhabited F.M] (x : F F.M) (i : F.Idx) :
= x.iget i
@[simp]
theorem PFunctor.M.isubtree_cons {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] (ps : ) {a : F.A} (f : F.B aF.M) {i : F.B a} :
PFunctor.M.isubtree (a, i :: ps) (PFunctor.M.mk a, f) = PFunctor.M.isubtree ps (f i)
@[simp]
theorem PFunctor.M.iselect_nil {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] {a : F.A} (f : F.B aF.M) :
@[simp]
theorem PFunctor.M.iselect_cons {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited F.M] (ps : ) {a : F.A} (f : F.B aF.M) {i : F.B a} :
PFunctor.M.iselect (a, i :: ps) (PFunctor.M.mk a, f) = PFunctor.M.iselect ps (f i)
theorem PFunctor.M.corec_def {F : PFunctor.{u}} {X : Type u_2} (f : XF X) (x₀ : X) :
= PFunctor.M.mk (F.map () (f x₀))
theorem PFunctor.M.ext_aux {F : PFunctor.{u}} [Inhabited F.M] [DecidableEq F.A] {n : } (x : F.M) (y : F.M) (z : F.M) (hx : ) (hy : ) (hrec : ∀ (ps : ), n = = ) :
x.approx (n + 1) = y.approx (n + 1)
theorem PFunctor.M.ext {F : PFunctor.{u}} [Inhabited F.M] (x : F.M) (y : F.M) (H : ∀ (ps : ), = ) :
x = y
structure PFunctor.M.IsBisimulation {F : PFunctor.{u}} (R : F.MF.MProp) :

Bisimulation is the standard proof technique for equality between infinite tree-like structures

• head : ∀ {a a' : F.A} {f : F.B aF.M} {f' : F.B a'F.M}, R (PFunctor.M.mk a, f) (PFunctor.M.mk a', f')a = a'

The head of the trees are equal

• tail : ∀ {a : F.A} {f f' : F.B aF.M}, R (PFunctor.M.mk a, f) (PFunctor.M.mk a, f')∀ (i : F.B a), R (f i) (f' i)

The tails are equal

Instances For
theorem PFunctor.M.IsBisimulation.head {F : PFunctor.{u}} {R : F.MF.MProp} (self : ) {a : F.A} {a' : F.A} {f : F.B aF.M} {f' : F.B a'F.M} :
R (PFunctor.M.mk a, f) (PFunctor.M.mk a', f')a = a'

The head of the trees are equal

theorem PFunctor.M.IsBisimulation.tail {F : PFunctor.{u}} {R : F.MF.MProp} (self : ) {a : F.A} {f : F.B aF.M} {f' : F.B aF.M} :
R (PFunctor.M.mk a, f) (PFunctor.M.mk a, f')∀ (i : F.B a), R (f i) (f' i)

The tails are equal

theorem PFunctor.M.nth_of_bisim {F : PFunctor.{u}} (R : F.MF.MProp) [Inhabited F.M] (bisim : ) (s₁ : F.M) (s₂ : F.M) (ps : ) :
R s₁ s₂ = ∃ (a : F.A) (f : F.B aF.M) (f' : F.B aF.M), = PFunctor.M.mk a, f = PFunctor.M.mk a, f' ∀ (i : F.B a), R (f i) (f' i)
theorem PFunctor.M.eq_of_bisim {F : PFunctor.{u}} (R : F.MF.MProp) [Nonempty F.M] (bisim : ) (s₁ : F.M) (s₂ : F.M) :
R s₁ s₂s₁ = s₂
def PFunctor.M.corecOn {F : PFunctor.{u}} {X : Type u_2} (x₀ : X) (f : XF X) :
F.M

corecursor for M F with swapped arguments

Equations
Instances For
theorem PFunctor.M.dest_corec {P : PFunctor.{u}} {α : Type u_2} (g : αP α) (x : α) :
().dest = P.map () (g x)
theorem PFunctor.M.bisim {P : PFunctor.{u}} (R : P.MP.MProp) (h : ∀ (x y : P.M), R x y∃ (a : P.A) (f : P.B aP.M) (f' : P.B aP.M), x.dest = a, f y.dest = a, f' ∀ (i : P.B a), R (f i) (f' i)) (x : P.M) (y : P.M) :
R x yx = y
theorem PFunctor.M.bisim' {P : PFunctor.{u}} {α : Type u_3} (Q : αProp) (u : αP.M) (v : αP.M) (h : ∀ (x : α), Q x∃ (a : P.A) (f : P.B aP.M) (f' : P.B aP.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.{u}} (R : P.MP.MProp) (h : ∀ (x y : P.M), R x y∃ (a : P.A) (f : P.B aP.M) (f' : P.B aP.M), x.dest = a, f y.dest = a, f' ∀ (i : P.B a), R (f i) (f' i)) (x : P.M) (y : P.M) :
R x yx = y
theorem PFunctor.M.corec_unique {P : PFunctor.{u}} {α : Type u_2} (g : αP α) (f : αP.M) (hyp : ∀ (x : α), (f x).dest = P.map f (g x)) :
def PFunctor.M.corec₁ {P : PFunctor.{u}} {α : Type u} (F : (X : Type u) → (αX)αP X) :
αP.M

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For