M-types
M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.
- continue : Π (F : pfunctor), pfunctor.approx.cofix_a F 0
- intro : Π (F : pfunctor) {n : ℕ} (a : F.A), (F.B a → pfunctor.approx.cofix_a F n) → pfunctor.approx.cofix_a F n.succ
cofix_a F n is an n level approximation of a M-type
default inhabitant of cofix_a
Equations
theorem
pfunctor.approx.cofix_a_eq_zero
(F : pfunctor)
(x y : pfunctor.approx.cofix_a F 0) :
x = y
The label of the root of the tree for a non-trivial approximation of the cofix of a pfunctor.
Equations
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
theorem
pfunctor.approx.approx_eta
{F : pfunctor}
{n : ℕ}
(x : pfunctor.approx.cofix_a F (n + 1)) :
inductive
pfunctor.approx.agree
{F : pfunctor}
{n : ℕ} :
pfunctor.approx.cofix_a F n → pfunctor.approx.cofix_a F (n + 1) → Prop
- continue : ∀ {F : pfunctor} (x : pfunctor.approx.cofix_a F 0) (y : pfunctor.approx.cofix_a F 1), pfunctor.approx.agree x y
- intro : ∀ {F : pfunctor} {n : ℕ} {a : F.A} (x : F.B a → pfunctor.approx.cofix_a F n) (x' : F.B a → pfunctor.approx.cofix_a F (n + 1)), (∀ (i : F.B a), pfunctor.approx.agree (x i) (x' i)) → pfunctor.approx.agree (pfunctor.approx.cofix_a.intro a x) (pfunctor.approx.cofix_a.intro a x')
Relation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated
Given an infinite series of approximations approx,
all_agree approx states that they are all consistent with each other.
Equations
- pfunctor.approx.all_agree x = ∀ (n : ℕ), pfunctor.approx.agree (x n) (x n.succ)
@[simp]
theorem
pfunctor.approx.agree_trival
{F : pfunctor}
{x : pfunctor.approx.cofix_a F 0}
{y : pfunctor.approx.cofix_a F 1} :
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)} :
i == j → pfunctor.approx.agree x y → pfunctor.approx.agree (pfunctor.approx.children' x i) (pfunctor.approx.children' y j)
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
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) :
pfunctor.approx.agree x y → pfunctor.approx.truncate y = x
s_corec f i n creates an approximation of height n
of the final coalgebra of f
Equations
- pfunctor.approx.s_corec f j n.succ = pfunctor.approx.cofix_a.intro (f j).fst (λ (i : F.B (f j).fst), pfunctor.approx.s_corec f ((f j).snd i) n)
- pfunctor.approx.s_corec f _x 0 = pfunctor.approx.cofix_a.continue
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)
path F provides indices to access internal nodes in corec F
Equations
- pfunctor.approx.path F = list F.Idx
@[instance]
@[instance]
Equations
theorem
pfunctor.approx.head_succ'
{F : pfunctor}
(n m : ℕ)
(x : Π (n : ℕ), pfunctor.approx.cofix_a F n) :
pfunctor.approx.all_agree x → pfunctor.approx.head' (x n.succ) = pfunctor.approx.head' (x m.succ)
- approx : Π (n : ℕ), pfunctor.approx.cofix_a F n
- consistent : pfunctor.approx.all_agree c.approx
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
@[instance]
Equations
- pfunctor.M.inhabited F = {default := {approx := λ (n : ℕ), inhabited.default (pfunctor.approx.cofix_a F n), consistent := _}}
@[instance]
Equations
- pfunctor.M_intl.inhabited F = show inhabited F.M, from pfunctor.M.inhabited F
Corecursor for the M-type defined by F.
Equations
- pfunctor.M.corec f i = {approx := pfunctor.approx.s_corec f i, consistent := _}
given a tree generated by F, head gives us the first piece of data
it contains
Equations
- x.head = pfunctor.approx.head' (x.approx 1)
return all the subtrees of the root of a tree x : M F
Equations
- x.children i = let H : ∀ (n : ℕ), pfunctor.approx.head' (x.approx n.succ) = pfunctor.approx.head' (x.approx 1) := _ in {approx := λ (n : ℕ), pfunctor.approx.children' (x.approx n.succ) (cast _ i), consistent := _}
select a subtree using a i : F.Idx or return an arbitrary tree if
i designates no subtree of x
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)
theorem
pfunctor.M.head_eq_head'
{F : pfunctor}
(x : F.M)
(n : ℕ) :
x.head = pfunctor.approx.head' (x.approx (n + 1))
theorem
pfunctor.M.head'_eq_head
{F : pfunctor}
(x : F.M)
(n : ℕ) :
pfunctor.approx.head' (x.approx (n + 1)) = x.head
theorem
pfunctor.M.truncate_approx
{F : pfunctor}
(x : F.M)
(n : ℕ) :
pfunctor.approx.truncate (x.approx (n + 1)) = x.approx n
generates the approximations needed for M.mk
Equations
- pfunctor.M.approx.s_mk x n.succ = pfunctor.approx.cofix_a.intro x.fst (λ (i : F.B x.fst), (x.snd i).approx n)
- pfunctor.M.approx.s_mk x 0 = pfunctor.approx.cofix_a.continue
constructor for M-types
Equations
- pfunctor.M.mk x = {approx := pfunctor.M.approx.s_mk x, consistent := _}
- trivial : ∀ {F : pfunctor} (x y : F.M), pfunctor.M.agree' 0 x y
- step : ∀ {F : pfunctor} {n : ℕ} {a : F.A} (x y : F.B a → F.M) {x' y' : F.M}, x' = pfunctor.M.mk ⟨a, x⟩ → y' = pfunctor.M.mk ⟨a, y⟩ → (∀ (i : F.B a), pfunctor.M.agree' n (x i) (y i)) → pfunctor.M.agree' n.succ x' y'
agree' n relates two trees of type M F that
are the same up to dept n
@[simp]
theorem
pfunctor.M.mk_inj
{F : pfunctor}
{x y : F.obj F.M} :
pfunctor.M.mk x = pfunctor.M.mk y → x = y
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
- pfunctor.M.cases f x = (λ (this : r (pfunctor.M.mk x.dest)), _.mpr this) (f x.dest)
def
pfunctor.M.cases_on
{F : pfunctor}
{r : F.M → Sort w}
(x : F.M) :
(Π (x : F.obj F.M), r (pfunctor.M.mk x)) → r x
destructor for M-types
Equations
- x.cases_on f = pfunctor.M.cases f x
def
pfunctor.M.cases_on'
{F : pfunctor}
{r : F.M → Sort 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
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_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
@[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
@[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
- nil : ∀ {F : pfunctor} (x : F.M), pfunctor.M.is_path list.nil x
- cons : ∀ {F : pfunctor} (xs : pfunctor.approx.path F) {a : F.A} (x : F.M) (f : F.B a → F.M) (i : F.B a), x = pfunctor.M.mk ⟨a, f⟩ → pfunctor.M.is_path xs (f i) → pfunctor.M.is_path (⟨a, i⟩ :: xs) 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} :
pfunctor.M.is_path (⟨a, i⟩ :: xs) (pfunctor.M.mk ⟨a, f⟩) → pfunctor.M.is_path xs (f i)
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
- pfunctor.M.isubtree (⟨a, i⟩ :: ps) x = x.cases_on' (λ (a' : F.A) (f : F.B a' → F.M), dite (a = a') (λ (h : a = a'), pfunctor.M.isubtree ps (f (cast _ i))) (λ (h : ¬a = a'), inhabited.default F.M))
- pfunctor.M.isubtree list.nil x = x
def
pfunctor.M.iselect
{F : pfunctor}
[decidable_eq F.A]
[inhabited F.M] :
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
- pfunctor.M.iselect ps = λ (x : F.M), (pfunctor.M.isubtree ps x).head
theorem
pfunctor.M.iselect_eq_default
{F : pfunctor}
[decidable_eq F.A]
[inhabited F.M]
(ps : pfunctor.approx.path F)
(x : F.M) :
¬pfunctor.M.is_path ps x → pfunctor.M.iselect ps x = (inhabited.default F.M).head
@[simp]
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) :
pfunctor.M.ichildren i (pfunctor.M.mk x) = x.iget i
@[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)
@[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
@[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)
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₀)
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 x → pfunctor.M.agree' n z y → (∀ (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) :
(∀ (ps : pfunctor.approx.path F), pfunctor.M.iselect ps x = pfunctor.M.iselect ps y) → x = y
- head : ∀ {a a' : F.A} {f : F.B a → F.M} {f' : F.B a' → F.M}, R (pfunctor.M.mk ⟨a, f⟩) (pfunctor.M.mk ⟨a', f'⟩) → a = a'
- tail : ∀ {a : F.A} {f f' : F.B a → F.M}, R (pfunctor.M.mk ⟨a, f⟩) (pfunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)
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₂
corecursor for M F with swapped arguments
Equations
- pfunctor.M.corec_on x₀ f = pfunctor.M.corec f x₀
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
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
corecursor where the state of the computation can be sent downstream in the form of a recursive call
Equations
- pfunctor.M.corec₁ F = pfunctor.M.corec (F α id)
corecursor where it is possible to return a fully formed value at any point of the computation
Equations
- pfunctor.M.corec' F x = pfunctor.M.corec₁ (λ (X : Type u) (rec : P.M ⊕ α → X) (a : P.M ⊕ α), let y : P.M ⊕ P.obj X := a >>= F (rec ∘ sum.inr) in pfunctor.M.corec'._match_1 X rec y) (sum.inr x)
- pfunctor.M.corec'._match_1 X rec (sum.inr y) = y
- pfunctor.M.corec'._match_1 X rec (sum.inl y) = (rec ∘ sum.inl) <$> y.dest