mathlib documentation

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

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

Equations

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

Equations
inductive pfunctor.approx.agree {F : pfunctor} {n : } :

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 : ), pfunctor.approx.cofix_a F n) → Prop

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

Equations
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
theorem pfunctor.approx.P_corec {F : pfunctor} {X : Type w} (f : X → F.obj X) (i : X) (n : ) :

def pfunctor.approx.path  :
pfunctorType u

path F provides indices to access internal nodes in corec F

Equations
structure pfunctor.M_intl  :
pfunctorType 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

def pfunctor.M  :
pfunctorType u

For polynomial functor F, M F is its final coalgebra

Equations
@[instance]

Equations
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) :
F.B x.head → 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_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
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) :

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

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

def pfunctor.M.cases {F : pfunctor} {r : F.MSort w} (f : Π (x : F.obj F.M), r (pfunctor.M.mk x)) (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 = pfunctor.approx.cofix_a.intro a (λ (j : F.B a), (f j).approx i)

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

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

@[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 (pfunctor.M.mk 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 (pfunctor.M.mk 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} :
pfunctor.approx.path FF.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⟩)pfunctor.M.is_path xs (f i)

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

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

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

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

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

theorem pfunctor.M.corec_def {F : pfunctor} {X : Type u} (f : X → F.obj X) (x₀ : X) :

theorem pfunctor.M.ext_aux {F : pfunctor} [inhabited F.M] [decidable_eq F.A] {n : } (x y z : F.M) :
pfunctor.M.agree' n z xpfunctor.M.agree' n z y(∀ (ps : pfunctor.approx.path F), n = list.length pspfunctor.M.iselect ps x = pfunctor.M.iselect ps y)x.approx (n + 1) = y.approx (n + 1)

theorem pfunctor.M.ext {F : pfunctor} [inhabited F.M] (x y : F.M) :

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₂pfunctor.M.is_path ps s₁ pfunctor.M.is_path ps s₂(pfunctor.M.iselect ps s₁ = pfunctor.M.iselect ps s₂ ∃ (a : F.A) (f f' : F.B a → F.M), pfunctor.M.isubtree ps s₁ = pfunctor.M.mk a, f⟩ pfunctor.M.isubtree ps 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
theorem pfunctor.M.dest_corec {P : pfunctor} {α : Type u} (g : α → P.obj α) (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)f = pfunctor.M.corec g

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