mathlib3 documentation

data.pfunctor.univariate.M

M-types #

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.

cofix_a F n is an n level approximation of a M-type

Instances for pfunctor.approx.cofix_a

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

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} (x : Π (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

path F provides indices to access internal nodes in corec F

Equations
Instances for pfunctor.approx.path
structure pfunctor.M_intl (F : pfunctor) :

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

Instances for pfunctor.M_intl
def pfunctor.M (F : pfunctor) :

For polynomial functor F, M F is its final coalgebra

Equations
Instances for pfunctor.M
@[protected, instance]
Equations
theorem pfunctor.M.ext' (F : pfunctor) (x y : F.M) (H : (i : ), x.approx i = y.approx i) :
x = y
@[protected]
def pfunctor.M.corec {F : pfunctor} {X : Type u_1} (f : X F.obj X) (i : X) :
F.M

Corecursor for the M-type defined by F.

Equations
def pfunctor.M.head {F : pfunctor} (x : 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) (i : 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] (i : F.Idx) (x : F.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.M F.obj F.M

unfold an M-type

Equations
@[protected]
def pfunctor.M.approx.s_mk {F : pfunctor} (x : F.obj F.M) (n : ) :

generates the approximations needed for M.mk

Equations
@[protected]
def pfunctor.M.mk {F : pfunctor} (x : F.obj F.M) :
F.M

constructor for M-types

Equations
inductive pfunctor.M.agree' {F : pfunctor} :
F.M F.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} (h : pfunctor.M.mk x = pfunctor.M.mk y) :
x = y
@[protected]
def pfunctor.M.cases {F : pfunctor} {r : F.M Sort w} (f : Π (x : F.obj F.M), r (pfunctor.M.mk x)) (x : F.M) :
r x

destructor for M-types

Equations
@[protected]
def pfunctor.M.cases_on {F : pfunctor} {r : F.M Sort w} (x : F.M) (f : Π (x : F.obj F.M), r (pfunctor.M.mk x)) :
r x

destructor for M-types

Equations
@[protected]
def pfunctor.M.cases_on' {F : pfunctor} {r : F.M Sort w} (x : F.M) (f : Π (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.M Sort 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.M Sort 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.M Sort 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

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

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) (hx : pfunctor.M.agree' n z x) (hy : pfunctor.M.agree' n z y) (hrec : (ps : pfunctor.approx.path F), n = list.length ps pfunctor.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) (H : (ps : pfunctor.approx.path F), pfunctor.M.iselect ps x = pfunctor.M.iselect ps y) :
x = y
structure pfunctor.M.is_bisimulation {F : pfunctor} (R : F.M F.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.M F.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.M F.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 : 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.M P.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 y x = 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 x u x = v x
theorem pfunctor.M.bisim_equiv {P : pfunctor} (R : P.M P.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 y x = y
theorem pfunctor.M.corec_unique {P : pfunctor} {α : Type u} (g : α P.obj α) (f : α P.M) (hyp : (x : α), (f x).dest = f <$> g x) :
def pfunctor.M.corec₁ {P : pfunctor} {α : Type u} (F : Π (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} (F : Π {X : Type u}, X) α P.M P.obj X) (x : α) :
P.M

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

Equations