M-types

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

inductive PFunctor.Approx.CofixA (F : PFunctor.{uA, uB}) : ℕ → Type (max uA uB)

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

• continue {F : PFunctor.{uA, uB}} : CofixA F 0
• intro {F : PFunctor.{uA, uB}} {n : ℕ} (a : F.A) : (F.B a → CofixA F n) → CofixA F n.succ

def PFunctor.Approx.CofixA.default (F : PFunctor.{uA, uB}) [Inhabited F.A] (n : ℕ) : CofixA F n

default inhabitant of CofixA

@[implicit_reducible]

instance PFunctor.Approx.instInhabitedCofixAOfA (F : PFunctor.{uA, uB}) [Inhabited F.A] {n : ℕ} : Inhabited (CofixA F n)

theorem PFunctor.Approx.cofixA_eq_zero (F : PFunctor.{uA, uB}) (x y : CofixA F 0) : x = y

def PFunctor.Approx.head' {F : PFunctor.{uA, uB}} {n : ℕ} : CofixA F n.succ → F.A

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

def PFunctor.Approx.children' {F : PFunctor.{uA, uB}} {n : ℕ} (x : CofixA F n.succ) : F.B (head' x) → CofixA F n

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

theorem PFunctor.Approx.approx_eta {F : PFunctor.{uA, uB}} {n : ℕ} (x : CofixA F (n + 1)) : x = CofixA.intro (head' x) (children' x)

inductive PFunctor.Approx.Agree {F : PFunctor.{uA, uB}} {n : ℕ} : CofixA F n → 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

• continu {F : PFunctor.{uA, uB}} (x : CofixA F 0) (y : CofixA F 1) : Agree x y
• intro {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} (x : F.B a → CofixA F n) (x' : F.B a → CofixA F (n + 1)) : (∀ (i : F.B a), Agree (x i) (x' i)) → Agree (CofixA.intro a x) (CofixA.intro a x')

def PFunctor.Approx.AllAgree {F : PFunctor.{uA, uB}} (x : (n : ℕ) → CofixA F n) : Prop

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

@[simp]

theorem PFunctor.Approx.agree_trivial {F : PFunctor.{uA, uB}} {x : CofixA F 0} {y : CofixA F 1} : Agree x y

theorem PFunctor.Approx.agree_children {F : PFunctor.{uA, uB}} {n : ℕ} (x : CofixA F n.succ) (y : CofixA F (n.succ + 1)) {i : F.B (head' x)} {j : F.B (head' y)} (h₀ : i ≍ j) (h₁ : Agree x y) : Agree (children' x i) (children' y j)

def PFunctor.Approx.truncate {F : PFunctor.{uA, uB}} {n : ℕ} : CofixA F (n + 1) → CofixA F n

truncate a turns a into a more limited approximation

theorem PFunctor.Approx.truncate_eq_of_agree {F : PFunctor.{uA, uB}} {n : ℕ} (x : CofixA F n) (y : CofixA F n.succ) (h : Agree x y) : truncate y = x

def PFunctor.Approx.sCorec {F : PFunctor.{uA, uB}} {X : Type w} (f : X → ↑F X) : X → (n : ℕ) → CofixA F n

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

theorem PFunctor.Approx.P_corec {F : PFunctor.{uA, uB}} {X : Type w} (f : X → ↑F X) (i : X) (n : ℕ) : Agree (sCorec f i n) (sCorec f i n.succ)

def PFunctor.Approx.Path (F : PFunctor.{uA, uB}) : Type (max uA uB)

Path F provides indices to access internal nodes in Corec F

@[implicit_reducible]

instance PFunctor.Approx.Path.inhabited {F : PFunctor.{uA, uB}} : Inhabited (Path F)

instance PFunctor.Approx.CofixA.instSubsingleton {F : PFunctor.{uA, uB}} : Subsingleton (CofixA F 0)

theorem PFunctor.Approx.head_succ' {F : PFunctor.{uA, uB}} (n m : ℕ) (x : (n : ℕ) → CofixA F n) (Hconsistent : AllAgree x) : head' (x n.succ) = head' (x m.succ)

structure PFunctor.MIntl (F : PFunctor.{uA, uB}) : Type (max uA uB)

Internal definition for M. It is needed to avoid name clashes between M.mk and M.casesOn and the declarations generated for the structure

• approx (n : ℕ) : Approx.CofixA F n

  An n-th level approximation, for each depth n

• consistent : Approx.AllAgree self.approx

  Each approximation agrees with the next

def PFunctor.M (F : PFunctor.{uA, uB}) : Type (max uA uB)

For polynomial functor F, M F is its final coalgebra

theorem PFunctor.M.default_consistent (F : PFunctor.{uA, uB}) [Inhabited F.A] (n : ℕ) : Approx.Agree default default

@[implicit_reducible]

instance PFunctor.MIntl.inhabited (F : PFunctor.{uA, uB}) [Inhabited F.A] : Inhabited F.MIntl

@[implicit_reducible]

instance PFunctor.M.inhabited (F : PFunctor.{uA, uB}) [Inhabited F.A] : Inhabited F.M

theorem PFunctor.M.ext' (F : PFunctor.{uA, uB}) (x y : F.M) (H : ∀ (i : ℕ), x.approx i = y.approx i) : x = y

def PFunctor.M.corec {F : PFunctor.{uA, uB}} {X : Type u_1} (f : X → ↑F X) (i : X) : F.M

Corecursor for the M-type defined by F.

def PFunctor.M.head {F : PFunctor.{uA, uB}} (x : F.M) : F.A

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

def PFunctor.M.children {F : PFunctor.{uA, uB}} (x : F.M) (i : F.B x.head) : F.M

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

def PFunctor.M.ichildren {F : PFunctor.{uA, uB}} [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

theorem PFunctor.M.head_succ {F : PFunctor.{uA, uB}} (n m : ℕ) (x : F.M) : Approx.head' (x.approx n.succ) = Approx.head' (x.approx m.succ)

theorem PFunctor.M.head_eq_head' {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ) : x.head = Approx.head' (x.approx (n + 1))

theorem PFunctor.M.head'_eq_head {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ) : Approx.head' (x.approx (n + 1)) = x.head

theorem PFunctor.M.truncate_approx {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ) : Approx.truncate (x.approx (n + 1)) = x.approx n

def PFunctor.M.dest {F : PFunctor.{uA, uB}} : F.M → ↑F F.M

unfold an M-type

def PFunctor.M.Approx.sMk {F : PFunctor.{uA, uB}} (x : ↑F F.M) (n : ℕ) : Approx.CofixA F n

generates the approximations needed for M.mk

theorem PFunctor.M.Approx.P_mk {F : PFunctor.{uA, uB}} (x : ↑F F.M) : Approx.AllAgree (Approx.sMk x)

def PFunctor.M.mk {F : PFunctor.{uA, uB}} (x : ↑F F.M) : F.M

constructor for M-types

inductive PFunctor.M.Agree' {F : PFunctor.{uA, uB}} : ℕ → F.M → F.M → Prop

Agree' n relates two trees of type M F that are the same up to depth n

• trivial {F : PFunctor.{uA, uB}} (x y : F.M) : Agree' 0 x y
• step {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} (x y : F.B a → F.M) {x' y' : F.M} : x' = M.mk ⟨a, x⟩ → y' = M.mk ⟨a, y⟩ → (∀ (i : F.B a), Agree' n (x i) (y i)) → Agree' n.succ x' y'

@[simp]

theorem PFunctor.M.dest_mk {F : PFunctor.{uA, uB}} (x : ↑F F.M) : (M.mk x).dest = x

@[simp]

theorem PFunctor.M.mk_dest {F : PFunctor.{uA, uB}} (x : F.M) : M.mk x.dest = x

theorem PFunctor.M.mk_inj {F : PFunctor.{uA, uB}} {x y : ↑F F.M} (h : M.mk x = M.mk y) : x = y

def PFunctor.M.cases {F : PFunctor.{uA, uB}} {r : F.M → Sort w} (f : (x : ↑F F.M) → r (M.mk x)) (x : F.M) : r x

destructor for M-types

def PFunctor.M.casesOn {F : PFunctor.{uA, uB}} {r : F.M → Sort w} (x : F.M) (f : (x : ↑F F.M) → r (M.mk x)) : r x

destructor for M-types

def PFunctor.M.casesOn' {F : PFunctor.{uA, uB}} {r : F.M → Sort w} (x : F.M) (f : (a : F.A) → (f : F.B a → F.M) → r (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

theorem PFunctor.M.approx_mk {F : PFunctor.{uA, uB}} (a : F.A) (f : F.B a → F.M) (i : ℕ) : (M.mk ⟨a, f⟩).approx i.succ = Approx.CofixA.intro a fun (j : F.B a) => (f j).approx i

@[simp]

theorem PFunctor.M.agree'_refl {F : PFunctor.{uA, uB}} {n : ℕ} (x : F.M) : Agree' n x x

theorem PFunctor.M.agree_iff_agree' {F : PFunctor.{uA, uB}} {n : ℕ} (x y : F.M) : Approx.Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

@[simp]

theorem PFunctor.M.cases_mk {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} (x : ↑F F.M) (f : (x : ↑F F.M) → r (M.mk x)) : M.cases f (M.mk x) = f x

@[simp]

theorem PFunctor.M.casesOn_mk {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} (x : ↑F F.M) (f : (x : ↑F F.M) → r (M.mk x)) : (M.mk x).casesOn f = f x

@[simp]

theorem PFunctor.M.casesOn_mk' {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} {a : F.A} (x : F.B a → F.M) (f : (a : F.A) → (f : F.B a → F.M) → r (M.mk ⟨a, f⟩)) : (M.mk ⟨a, x⟩).casesOn' f = f a x

inductive PFunctor.M.IsPath {F : PFunctor.{uA, uB}} : Approx.Path F → F.M → Prop

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

• nil {F : PFunctor.{uA, uB}} (x : F.M) : IsPath [] x
• cons {F : PFunctor.{uA, uB}} (xs : Approx.Path F) {a : F.A} (x : F.M) (f : F.B a → F.M) (i : F.B a) : x = M.mk ⟨a, f⟩ → IsPath xs (f i) → IsPath (⟨a, i⟩ :: xs) x

theorem PFunctor.M.isPath_cons {F : PFunctor.{uA, uB}} {xs : Approx.Path F} {a a' : F.A} {f : F.B a → F.M} {i : F.B a'} : IsPath (⟨a', i⟩ :: xs) (M.mk ⟨a, f⟩) → a = a'

theorem PFunctor.M.isPath_cons' {F : PFunctor.{uA, uB}} {xs : Approx.Path F} {a : F.A} {f : F.B a → F.M} {i : F.B a} : IsPath (⟨a, i⟩ :: xs) (M.mk ⟨a, f⟩) → IsPath xs (f i)

def PFunctor.M.isubtree {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] : 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

def PFunctor.M.iselect {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] (ps : 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

theorem PFunctor.M.iselect_eq_default {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] (ps : Approx.Path F) (x : F.M) (h : ¬IsPath ps x) : iselect ps x = default.head

@[simp]

theorem PFunctor.M.head_mk {F : PFunctor.{uA, uB}} (x : ↑F F.M) : (M.mk x).head = x.fst

theorem PFunctor.M.children_mk {F : PFunctor.{uA, uB}} {a : F.A} (x : F.B a → F.M) (i : F.B (M.mk ⟨a, x⟩).head) : (M.mk ⟨a, x⟩).children i = x (cast ⋯ i)

@[simp]

theorem PFunctor.M.ichildren_mk {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] (x : ↑F F.M) (i : F.Idx) : ichildren i (M.mk x) = x.iget i

@[simp]

theorem PFunctor.M.isubtree_cons {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] (ps : Approx.Path F) {a : F.A} (f : F.B a → F.M) {i : F.B a} : isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i)

@[simp]

theorem PFunctor.M.iselect_nil {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] {a : F.A} (f : F.B a → F.M) : iselect [] (M.mk ⟨a, f⟩) = a

@[simp]

theorem PFunctor.M.iselect_cons {F : PFunctor.{uA, uB}} [DecidableEq F.A] [Inhabited F.M] (ps : Approx.Path F) {a : F.A} (f : F.B a → F.M) {i : F.B a} : iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i)

theorem PFunctor.M.corec_def {F : PFunctor.{uA, uB}} {X : Type u_2} (f : X → ↑F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

theorem PFunctor.M.ext_aux {F : PFunctor.{uA, uB}} [Inhabited F.M] [DecidableEq F.A] {n : ℕ} (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y) (hrec : ∀ (ps : Approx.Path F), n = List.length ps → iselect ps x = iselect ps y) : x.approx (n + 1) = y.approx (n + 1)

theorem PFunctor.M.ext {F : PFunctor.{uA, uB}} [Inhabited F.M] [DecidableEq F.A] (x y : F.M) (H : ∀ (ps : Approx.Path F), iselect ps x = iselect ps y) : x = y

structure PFunctor.M.IsBisimulation {F : PFunctor.{uA, uB}} (R : F.M → F.M → Prop) : Prop

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

• head {a a' : F.A} {f : F.B a → F.M} {f' : F.B a' → F.M} : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩) → a = a'

  The head of the trees are equal

• tail {a : F.A} {f f' : F.B a → F.M} : R (M.mk ⟨a, f⟩) (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.{uA, uB}} (R : F.M → F.M → Prop) [Inhabited F.M] [DecidableEq F.A] (bisim : IsBisimulation R) (s₁ s₂ : F.M) (ps : Approx.Path F) : R s₁ s₂ → IsPath ps s₁ ∨ IsPath ps s₂ → iselect ps s₁ = iselect ps s₂ ∧ ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → F.M), isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

theorem PFunctor.M.eq_of_bisim {F : PFunctor.{uA, uB}} (R : F.M → F.M → Prop) [Nonempty F.M] (bisim : IsBisimulation R) (s₁ s₂ : F.M) : R s₁ s₂ → s₁ = s₂

def PFunctor.M.corecOn {F : PFunctor.{uA, uB}} {X : Type u_2} (x₀ : X) (f : X → ↑F X) : F.M

corecursor for M F with swapped arguments

theorem PFunctor.M.dest_corec {P : PFunctor.{uA, uB}} {α : Type u_2} (g : α → ↑P α) (x : α) : (M.corec g x).dest = P.map (M.corec g) (g x)

theorem PFunctor.M.bisim {P : PFunctor.{uA, uB}} (R : P.M → P.M → Prop) (h : ∀ (x y : P.M), R x y → ∃ (a : P.A) (f : P.B a → P.M) (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.{uA, uB}} {α : Type u_3} (Q : α → Prop) (u v : α → P.M) (h : ∀ (x : α), Q x → ∃ (a : P.A) (f : P.B a → P.M) (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.{uA, uB}} (R : P.M → P.M → Prop) (h : ∀ (x y : P.M), R x y → ∃ (a : P.A) (f : P.B a → P.M) (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.{uA, uB}} {α : Type u_2} (g : α → ↑P α) (f : α → P.M) (hyp : ∀ (x : α), (f x).dest = P.map f (g x)) : f = M.corec g

def PFunctor.M.corec₁ {P : PFunctor.{uA, uB}} {α : 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

def PFunctor.M.corec' {P : PFunctor.{uA, uB}} {α : Type u} (F : {X : Type (max u uA uB)} → (α → 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