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.{u}) : ℕ → Type u

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

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

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

default inhabitant of CofixA

Equations

• PFunctor.Approx.CofixA.default F 0 = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.CofixA.default F n.succ = PFunctor.Approx.CofixA.intro default fun (x : F.B default) => PFunctor.Approx.CofixA.default F n

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

Equations

• PFunctor.Approx.instInhabitedCofixAOfA F = { default := PFunctor.Approx.CofixA.default F n }

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

def PFunctor.Approx.head' {F : PFunctor.{u}} {n : ℕ} : PFunctor.Approx.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.

Equations

• PFunctor.Approx.head' x = match x✝, x with | x, PFunctor.Approx.CofixA.intro i a => i

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

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

Equations

• One or more equations did not get rendered due to their size.

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

inductive PFunctor.Approx.Agree {F : PFunctor.{u}} {n : ℕ} : PFunctor.Approx.CofixA F n → PFunctor.Approx.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.{u}} (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 1), PFunctor.Approx.Agree x y
• intro: ∀ {F : PFunctor.{u}} {n : ℕ} {a : F.A} (x : F.B a → PFunctor.Approx.CofixA F n) (x' : F.B a → PFunctor.Approx.CofixA F (n + 1)), (∀ (i : F.B a), PFunctor.Approx.Agree (x i) (x' i)) → PFunctor.Approx.Agree (PFunctor.Approx.CofixA.intro a x) (PFunctor.Approx.CofixA.intro a x')

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

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

Equations

• PFunctor.Approx.AllAgree x = ∀ (n : ℕ), PFunctor.Approx.Agree (x n) (x n.succ)

@[simp]

theorem PFunctor.Approx.agree_trival {F : PFunctor.{u}} {x : PFunctor.Approx.CofixA F 0} {y : PFunctor.Approx.CofixA F 1} : PFunctor.Approx.Agree x y

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

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

truncate a turns a into a more limited approximation

Equations

• PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro a a_1) = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.truncate (PFunctor.Approx.CofixA.intro i f) = PFunctor.Approx.CofixA.intro i (PFunctor.Approx.truncate ∘ f)

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

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

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

Equations

• PFunctor.Approx.sCorec f x 0 = PFunctor.Approx.CofixA.continue
• PFunctor.Approx.sCorec f x n.succ = PFunctor.Approx.CofixA.intro (f x).fst fun (i : F.B (f x).fst) => PFunctor.Approx.sCorec f ((f x).snd i) n

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

def PFunctor.Approx.Path (F : PFunctor.{u}) : Type u

Path F provides indices to access internal nodes in Corec F

Equations

• PFunctor.Approx.Path F = List F.Idx

instance PFunctor.Approx.Path.inhabited {F : PFunctor.{u}} : Inhabited (PFunctor.Approx.Path F)

Equations

• PFunctor.Approx.Path.inhabited = { default := [] }

instance PFunctor.Approx.CofixA.instSubsingleton {F : PFunctor.{u}} : Subsingleton (PFunctor.Approx.CofixA F 0)

Equations

• ⋯ = ⋯

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

structure PFunctor.MIntl (F : PFunctor.{u}) : 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

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

  An n-th level approximation, for each depth n

• consistent : PFunctor.Approx.AllAgree self.approx

  Each approximation agrees with the next

theorem PFunctor.MIntl.consistent {F : PFunctor.{u}} (self : F.MIntl) : PFunctor.Approx.AllAgree self.approx

Each approximation agrees with the next

def PFunctor.M (F : PFunctor.{u}) : Type u

For polynomial functor F, M F is its final coalgebra

Equations

• F.M = F.MIntl

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

instance PFunctor.M.inhabited (F : PFunctor.{u}) [Inhabited F.A] : Inhabited F.M

Equations

• PFunctor.M.inhabited F = { default := { approx := default, consistent := ⋯ } }

instance PFunctor.MIntl.inhabited (F : PFunctor.{u}) [Inhabited F.A] : Inhabited F.MIntl

Equations

• PFunctor.MIntl.inhabited F = let_fun this := inferInstance; this

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

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

Corecursor for the M-type defined by F.

Equations

• PFunctor.M.corec f i = { approx := PFunctor.Approx.sCorec f i, consistent := ⋯ }

def PFunctor.M.head {F : PFunctor.{u}} (x : F.M) : F.A

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)

def PFunctor.M.children {F : PFunctor.{u}} (x : F.M) (i : F.B x.head) : F.M

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

Equations

• x.children i = let H := ⋯; { approx := fun (n : ℕ) => PFunctor.Approx.children' (x.approx n.succ) (cast ⋯ i), consistent := ⋯ }

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

Equations

• PFunctor.M.ichildren i x = if H' : i.fst = x.head then x.children (cast ⋯ i.snd) else default

theorem PFunctor.M.head_succ {F : PFunctor.{u}} (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.{u}} (x : F.M) (n : ℕ) : x.head = PFunctor.Approx.head' (x.approx (n + 1))

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

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

def PFunctor.M.dest {F : PFunctor.{u}} : F.M → ↑F F.M

unfold an M-type

Equations

• x.dest = let x := x; ⟨x.head, fun (i : F.B x.head) => x.children i⟩

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

generates the approximations needed for M.mk

Equations

• PFunctor.M.Approx.sMk x✝ x = match x with | 0 => PFunctor.Approx.CofixA.continue | n.succ => PFunctor.Approx.CofixA.intro x✝.fst fun (i : F.B x✝.fst) => (x✝.snd i).approx n

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

def PFunctor.M.mk {F : PFunctor.{u}} (x : ↑F F.M) : F.M

constructor for M-types

Equations

• PFunctor.M.mk x = { approx := PFunctor.M.Approx.sMk x, consistent := ⋯ }

inductive PFunctor.M.Agree' {F : PFunctor.{u}} : ℕ → 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.{u}} (x y : F.M), PFunctor.M.Agree' 0 x y
• step: ∀ {F : PFunctor.{u}} {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'

@[simp]

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

@[simp]

theorem PFunctor.M.mk_dest {F : PFunctor.{u}} (x : F.M) : PFunctor.M.mk x.dest = x

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

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

destructor for M-types

Equations

• PFunctor.M.cases f x = let_fun this := f x.dest; ⋯.mpr this

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

destructor for M-types

Equations

• x.casesOn f = PFunctor.M.cases f x

def PFunctor.M.casesOn' {F : PFunctor.{u}} {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 casesOn but also gives access directly to the root and subtrees on an M-type

Equations

• x.casesOn' f = x.casesOn fun (x : ↑F F.M) => match x with | ⟨a, g⟩ => f a g

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

@[simp]

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

theorem PFunctor.M.agree_iff_agree' {F : PFunctor.{u}} {n : ℕ} (x : F.M) (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.{u}} {r : F.M → Sort u_2} (x : ↑F F.M) (f : (x : ↑F F.M) → r (PFunctor.M.mk x)) : PFunctor.M.cases f (PFunctor.M.mk x) = f x

@[simp]

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

@[simp]

theorem PFunctor.M.casesOn_mk' {F : PFunctor.{u}} {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 (PFunctor.M.mk ⟨a, f⟩)) : (PFunctor.M.mk ⟨a, x⟩).casesOn' f = f a x

inductive PFunctor.M.IsPath {F : PFunctor.{u}} : PFunctor.Approx.Path F → F.M → Prop

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

• nil: ∀ {F : PFunctor.{u}} (x : F.M), PFunctor.M.IsPath [] x
• cons: ∀ {F : PFunctor.{u}} (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.IsPath xs (f i) → PFunctor.M.IsPath (⟨a, i⟩ :: xs) x

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

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

def PFunctor.M.isubtree {F : PFunctor.{u}} [DecidableEq 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 [] x = x
• PFunctor.M.isubtree (⟨a, i⟩ :: ps) x = x.casesOn' fun (a' : F.A) (f : F.B a' → F.M) => if h : a = a' then PFunctor.M.isubtree ps (f (cast ⋯ i)) else default

def PFunctor.M.iselect {F : PFunctor.{u}} [DecidableEq 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

• PFunctor.M.iselect ps x = (PFunctor.M.isubtree ps x).head

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

@[simp]

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

theorem PFunctor.M.children_mk {F : PFunctor.{u}} {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.{u}} [DecidableEq F.A] [Inhabited F.M] (x : ↑F F.M) (i : F.Idx) : PFunctor.M.ichildren i (PFunctor.M.mk x) = x.iget i

@[simp]

theorem PFunctor.M.isubtree_cons {F : PFunctor.{u}} [DecidableEq 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.{u}} [DecidableEq F.A] [Inhabited F.M] {a : F.A} (f : F.B a → F.M) : PFunctor.M.iselect [] (PFunctor.M.mk ⟨a, f⟩) = a

@[simp]

theorem PFunctor.M.iselect_cons {F : PFunctor.{u}} [DecidableEq 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.{u}} {X : Type u_2} (f : X → ↑F X) (x₀ : X) : PFunctor.M.corec f x₀ = PFunctor.M.mk (F.map (PFunctor.M.corec f) (f x₀))

theorem PFunctor.M.ext_aux {F : PFunctor.{u}} [Inhabited F.M] [DecidableEq F.A] {n : ℕ} (x : F.M) (y : F.M) (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.{u}} [Inhabited F.M] (x : F.M) (y : F.M) (H : ∀ (ps : PFunctor.Approx.Path F), PFunctor.M.iselect ps x = PFunctor.M.iselect ps y) : x = y

structure PFunctor.M.IsBisimulation {F : PFunctor.{u}} (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 (PFunctor.M.mk ⟨a, f⟩) (PFunctor.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 (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)

  The tails are equal

theorem PFunctor.M.IsBisimulation.head {F : PFunctor.{u}} {R : F.M → F.M → Prop} (self : PFunctor.M.IsBisimulation R) {a : F.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'

The head of the trees are equal

theorem PFunctor.M.IsBisimulation.tail {F : PFunctor.{u}} {R : F.M → F.M → Prop} (self : PFunctor.M.IsBisimulation R) {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'⟩) → ∀ (i : F.B a), R (f i) (f' i)

The tails are equal

theorem PFunctor.M.nth_of_bisim {F : PFunctor.{u}} (R : F.M → F.M → Prop) [Inhabited F.M] (bisim : PFunctor.M.IsBisimulation R) (s₁ : F.M) (s₂ : F.M) (ps : PFunctor.Approx.Path F) : R s₁ s₂ → PFunctor.M.IsPath ps s₁ ∨ PFunctor.M.IsPath ps s₂ → PFunctor.M.iselect ps s₁ = PFunctor.M.iselect ps s₂ ∧ ∃ (a : F.A) (f : F.B a → F.M) (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.{u}} (R : F.M → F.M → Prop) [Nonempty F.M] (bisim : PFunctor.M.IsBisimulation R) (s₁ : F.M) (s₂ : F.M) : R s₁ s₂ → s₁ = s₂

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

corecursor for M F with swapped arguments

Equations

• PFunctor.M.corecOn x₀ f = PFunctor.M.corec f x₀

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

theorem PFunctor.M.bisim {P : PFunctor.{u}} (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 : P.M) (y : P.M) : R x y → x = y

theorem PFunctor.M.bisim' {P : PFunctor.{u}} {α : Type u_3} (Q : α → Prop) (u : α → P.M) (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.{u}} (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 : P.M) (y : P.M) : R x y → x = y

theorem PFunctor.M.corec_unique {P : PFunctor.{u}} {α : Type u_2} (g : α → ↑P α) (f : α → P.M) (hyp : ∀ (x : α), (f x).dest = P.map f (g x)) : f = PFunctor.M.corec g

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

Equations

• PFunctor.M.corec₁ F = PFunctor.M.corec (F α id)

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

Equations

• One or more equations did not get rendered due to their size.