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.

source
inductive pfunctor.approx.cofix_a (F : pfunctor) :
ℕ → Type u

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

Instances for pfunctor.approx.cofix_a
source
@[protected]
def pfunctor.approx.cofix_a.default (F : pfunctor) [inhabited F.A] (n : ℕ) :
pfunctor.approx.cofix_a F n

default inhabitant of cofix_a

Equations
source
@[protected, instance]
def pfunctor.approx.cofix_a.inhabited (F : pfunctor) [inhabited F.A] {n : ℕ} :
inhabited (pfunctor.approx.cofix_a F n)
Equations
source
theorem pfunctor.approx.cofix_a_eq_zero (F : pfunctor) (x y : pfunctor.approx.cofix_a F 0) :
x = y
source
def pfunctor.approx.head' {F : pfunctor} {n : ℕ} :
pfunctor.approx.cofix_a F n.succ → F.A

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

Equations
source
def pfunctor.approx.children' {F : pfunctor} {n : ℕ} (x : pfunctor.approx.cofix_a F n.succ) :
F.B (pfunctor.approx.head' x) → pfunctor.approx.cofix_a F n

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

Equations
source
theorem pfunctor.approx.approx_eta {F : pfunctor} {n : ℕ} (x : pfunctor.approx.cofix_a F (n + 1)) :
x = pfunctor.approx.cofix_a.intro (pfunctor.approx.head' x) (pfunctor.approx.children' x)
source
inductive pfunctor.approx.agree {F : pfunctor} {n : ℕ} :
pfunctor.approx.cofix_a F n → pfunctor.approx.cofix_a 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

source
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
source
@[simp]
theorem pfunctor.approx.agree_trival {F : pfunctor} {x : pfunctor.approx.cofix_a F 0} {y : pfunctor.approx.cofix_a F 1} :
pfunctor.approx.agree x y
source
theorem pfunctor.approx.agree_children {F : pfunctor} {n : ℕ} (x : pfunctor.approx.cofix_a F n.succ) (y : pfunctor.approx.cofix_a F (n.succ + 1)) {i : F.B (pfunctor.approx.head' x)} {j : F.B (pfunctor.approx.head' y)} (h₀ : i == j) (h₁ : pfunctor.approx.agree x y) :
pfunctor.approx.agree (pfunctor.approx.children' x i) (pfunctor.approx.children' y j)
source
def pfunctor.approx.truncate {F : pfunctor} {n : ℕ} :
pfunctor.approx.cofix_a F (n + 1) → pfunctor.approx.cofix_a F n

truncate a turns a into a more limited approximation

Equations
source
theorem pfunctor.approx.truncate_eq_of_agree {F : pfunctor} {n : ℕ} (x : pfunctor.approx.cofix_a F n) (y : pfunctor.approx.cofix_a F n.succ) (h : pfunctor.approx.agree x y) :
pfunctor.approx.truncate y = x
source
def pfunctor.approx.s_corec {F : pfunctor} {X : Type w} (f : X → F.obj X) (i : X) (n : ℕ) :
pfunctor.approx.cofix_a F n

s_corec f i n creates an approximation of height n of the final coalgebra of f

Equations
source
theorem pfunctor.approx.P_corec {F : pfunctor} {X : Type w} (f : X → F.obj X) (i : X) (n : ℕ) :
pfunctor.approx.agree (pfunctor.approx.s_corec f i n) (pfunctor.approx.s_corec f i n.succ)
source
def pfunctor.approx.path (F : pfunctor) :
Type u

path F provides indices to access internal nodes in corec F

Equations
Instances for pfunctor.approx.path
source
@[protected, instance]
def pfunctor.approx.path.inhabited {F : pfunctor} :
inhabited (pfunctor.approx.path F)
Equations
source
@[protected, instance]
def pfunctor.approx.cofix_a.subsingleton {F : pfunctor} :
subsingleton (pfunctor.approx.cofix_a F 0)
source
theorem pfunctor.approx.head_succ' {F : pfunctor} (n m : ℕ) (x : Π (n : ℕ), pfunctor.approx.cofix_a F n) (Hconsistent : pfunctor.approx.all_agree x) :
pfunctor.approx.head' (x n.succ) = pfunctor.approx.head' (x m.succ)
source
structure pfunctor.M_intl (F : pfunctor) :
Type 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

Instances for pfunctor.M_intl
source
def pfunctor.M (F : pfunctor) :
Type u

For polynomial functor F, M F is its final coalgebra

Equations
Instances for pfunctor.M
source
theorem pfunctor.M.default_consistent (F : pfunctor) [inhabited F.A] (n : ℕ) :
pfunctor.approx.agree inhabited.default inhabited.default
source
@[protected, instance]
def pfunctor.M.inhabited (F : pfunctor) [inhabited F.A] :
inhabited F.M
Equations
source
@[protected, instance]
def pfunctor.M_intl.inhabited (F : pfunctor) [inhabited F.A] :
inhabited F.M_intl
Equations
source
theorem pfunctor.M.ext' (F : pfunctor) (x y : F.M) (H : ∀ (i : ℕ), x.approx i = y.approx i) :
x = y
source
@[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
source
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
source
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
source
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
source
theorem pfunctor.M.head_succ {F : pfunctor} (n m : ℕ) (x : F.M) :
pfunctor.approx.head' (x.approx n.succ) = pfunctor.approx.head' (x.approx m.succ)
source
theorem pfunctor.M.head_eq_head' {F : pfunctor} (x : F.M) (n : ℕ) :
x.head = pfunctor.approx.head' (x.approx (n + 1))
source
theorem pfunctor.M.head'_eq_head {F : pfunctor} (x : F.M) (n : ℕ) :
pfunctor.approx.head' (x.approx (n + 1)) = x.head
source
theorem pfunctor.M.truncate_approx {F : pfunctor} (x : F.M) (n : ℕ) :
pfunctor.approx.truncate (x.approx (n + 1)) = x.approx n
source
def pfunctor.M.dest {F : pfunctor} :
F.M → F.obj F.M

unfold an M-type

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

generates the approximations needed for M.mk

Equations
source
@[protected]
theorem pfunctor.M.approx.P_mk {F : pfunctor} (x : F.obj F.M) :
pfunctor.approx.all_agree (pfunctor.M.approx.s_mk x)
source
@[protected]
def pfunctor.M.mk {F : pfunctor} (x : F.obj F.M) :
F.M

constructor for M-types

Equations
source
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

source
@[simp]
theorem pfunctor.M.dest_mk {F : pfunctor} (x : F.obj F.M) :
(pfunctor.M.mk x).dest = x
source
@[simp]
theorem pfunctor.M.mk_dest {F : pfunctor} (x : F.M) :
pfunctor.M.mk x.dest = x
source
theorem pfunctor.M.mk_inj {F : pfunctor} {x y : F.obj F.M} (h : pfunctor.M.mk x = pfunctor.M.mk y) :
x = y
source
@[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
source
@[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
source
@[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
source
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)
source
@[simp]
theorem pfunctor.M.agree'_refl {F : pfunctor} {n : ℕ} (x : F.M) :
pfunctor.M.agree' n x x
source
theorem pfunctor.M.agree_iff_agree' {F : pfunctor} {n : ℕ} (x y : F.M) :
pfunctor.approx.agree (x.approx n) (y.approx (n + 1)) ↔ pfunctor.M.agree' n x y
source
@[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)) :
pfunctor.M.cases f (pfunctor.M.mk x) = f x
source
@[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)) :
(pfunctor.M.mk x).cases_on f = f x
source
@[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
source
inductive pfunctor.M.is_path {F : pfunctor} :
pfunctor.approx.path F → F.M → Prop

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

source
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'
source
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)
source
def pfunctor.M.isubtree {F : pfunctor} [decidable_eq F.A] [inhabited F.M] :
pfunctor.approx.path F → F.M → F.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
source
def pfunctor.M.iselect {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (ps : pfunctor.approx.path F) :
F.M → F.A

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

Equations
source
theorem pfunctor.M.iselect_eq_default {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (ps : pfunctor.approx.path F) (x : F.M) (h : ¬pfunctor.M.is_path ps x) :
pfunctor.M.iselect ps x = inhabited.default.head
source
@[simp]
theorem pfunctor.M.head_mk {F : pfunctor} (x : F.obj F.M) :
(pfunctor.M.mk x).head = x.fst
source
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)
source
@[simp]
theorem pfunctor.M.ichildren_mk {F : pfunctor} [decidable_eq F.A] [inhabited F.M] (x : F.obj F.M) (i : F.Idx) :
pfunctor.M.ichildren i (pfunctor.M.mk x) = x.iget i
source
@[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} :
pfunctor.M.isubtree (⟨a, i⟩ :: ps) (pfunctor.M.mk ⟨a, f⟩) = pfunctor.M.isubtree ps (f i)
source
@[simp]
theorem pfunctor.M.iselect_nil {F : pfunctor} [decidable_eq F.A] [inhabited F.M] {a : F.A} (f : F.B a → F.M) :
pfunctor.M.iselect list.nil (pfunctor.M.mk ⟨a, f⟩) = a
source
@[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} :
pfunctor.M.iselect (⟨a, i⟩ :: ps) (pfunctor.M.mk ⟨a, f⟩) = pfunctor.M.iselect ps (f i)
source
theorem pfunctor.M.corec_def {F : pfunctor} {X : Type u} (f : X → F.obj X) (x₀ : X) :
pfunctor.M.corec f x₀ = pfunctor.M.mk (pfunctor.M.corec f <$> f x₀)
source
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)
source
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
source
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

source
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))
source
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₂
source
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
source
theorem pfunctor.M.dest_corec {P : pfunctor} {α : Type u} (g : α → P.obj α) (x : α) :
(pfunctor.M.corec g x).dest = pfunctor.M.corec g <$> g x
source
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
source
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
source
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
source
theorem pfunctor.M.corec_unique {P : pfunctor} {α : Type u} (g : α → P.obj α) (f : α → P.M) (hyp : ∀ (x : α), (f x).dest = f <$> g x) :
f = pfunctor.M.corec g
source
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
source
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