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 (Nat.succ n)

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 (Nat.succ n) = PFunctor.Approx.CofixA.intro default fun (x : F.B default) => PFunctor.Approx.CofixA.default F n

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

Equations

• PFunctor.Approx.instInhabitedCofixA 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 (Nat.succ n) → 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 (Nat.succ n)) : 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 (Nat.succ n))

@[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 (Nat.succ n)) (y : PFunctor.Approx.CofixA F (Nat.succ n + 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 (Nat.succ n)) (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 (Nat.succ n) = 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 (Nat.succ n))

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 (PFunctor.Idx F)

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

• (_ : Subsingleton (PFunctor.Approx.CofixA F 0)) = (_ : Subsingleton (PFunctor.Approx.CofixA F 0))

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 (Nat.succ n)) = PFunctor.Approx.head' (x (Nat.succ m))

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

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

For polynomial functor F, M F is its final coalgebra

Equations

• PFunctor.M F = PFunctor.MIntl F

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 (PFunctor.M F)

Equations

• PFunctor.M.inhabited F = { default := { approx := default, consistent := (_ : ∀ (n : ℕ), PFunctor.Approx.Agree default default) } }

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

Equations

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

theorem PFunctor.M.ext' (F : PFunctor.{u}) (x : PFunctor.M F) (y : PFunctor.M F) (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) : PFunctor.M F

Corecursor for the M-type defined by F.

Equations

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

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

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

Equations

• PFunctor.M.head x = PFunctor.Approx.head' (x.approx 1)

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

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

Equations

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

def PFunctor.M.ichildren {F : PFunctor.{u}} [Inhabited (PFunctor.M F)] [DecidableEq F.A] (i : PFunctor.Idx F) (x : PFunctor.M F) : PFunctor.M F

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 = PFunctor.M.head x then PFunctor.M.children x (cast (_ : F.B i.fst = F.B (PFunctor.M.head x)) i.snd) else default

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

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

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

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

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

unfold an M-type

Equations

• PFunctor.M.dest x = let x := x; { fst := PFunctor.M.head x, snd := fun (i : F.B (PFunctor.M.head x)) => PFunctor.M.children x i }

def PFunctor.M.Approx.sMk {F : PFunctor.{u}} (x : ↑F (PFunctor.M F)) (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 | Nat.succ n => 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 (PFunctor.M F)) : PFunctor.Approx.AllAgree (PFunctor.M.Approx.sMk x)

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

constructor for M-types

Equations

• PFunctor.M.mk x = { approx := PFunctor.M.Approx.sMk x, consistent := (_ : PFunctor.Approx.AllAgree (PFunctor.M.Approx.sMk x)) }

inductive PFunctor.M.Agree' {F : PFunctor.{u}} : ℕ → PFunctor.M F → PFunctor.M F → Prop

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

• trivial: ∀ {F : PFunctor.{u}} (x y : PFunctor.M F), PFunctor.M.Agree' 0 x y
• step: ∀ {F : PFunctor.{u}} {n : ℕ} {a : F.A} (x y : F.B a → PFunctor.M F) {x' y' : PFunctor.M F}, x' = PFunctor.M.mk { fst := a, snd := x } → y' = PFunctor.M.mk { fst := a, snd := y } → (∀ (i : F.B a), PFunctor.M.Agree' n (x i) (y i)) → PFunctor.M.Agree' (Nat.succ n) x' y'

@[simp]

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

@[simp]

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

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

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

destructor for M-types

Equations

• PFunctor.M.cases f x = let_fun this := f (PFunctor.M.dest x); Eq.mpr (_ : r x = r (PFunctor.M.mk (PFunctor.M.dest x))) this

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

destructor for M-types

Equations

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

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

• PFunctor.M.casesOn' x f = PFunctor.M.casesOn x fun (x : ↑F (PFunctor.M F)) => match x with | { fst := a, snd := g } => f a g

theorem PFunctor.M.approx_mk {F : PFunctor.{u}} (a : F.A) (f : F.B a → PFunctor.M F) (i : ℕ) : (PFunctor.M.mk { fst := a, snd := f }).approx (Nat.succ i) = 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 : PFunctor.M F) : PFunctor.M.Agree' n x x

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

@[simp]

theorem PFunctor.M.casesOn_mk' {F : PFunctor.{u}} {r : PFunctor.M F → Sort u_2} {a : F.A} (x : F.B a → PFunctor.M F) (f : (a : F.A) → (f : F.B a → PFunctor.M F) → r (PFunctor.M.mk { fst := a, snd := f })) : PFunctor.M.casesOn' (PFunctor.M.mk { fst := a, snd := x }) f = f a x

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

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

• nil: ∀ {F : PFunctor.{u}} (x : PFunctor.M F), PFunctor.M.IsPath [] x
• cons: ∀ {F : PFunctor.{u}} (xs : PFunctor.Approx.Path F) {a : F.A} (x : PFunctor.M F) (f : F.B a → PFunctor.M F) (i : F.B a), x = PFunctor.M.mk { fst := a, snd := f } → PFunctor.M.IsPath xs (f i) → PFunctor.M.IsPath ({ fst := a, snd := 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 → PFunctor.M F} {i : F.B a'} : PFunctor.M.IsPath ({ fst := a', snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f }) → a = a'

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

def PFunctor.M.isubtree {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited (PFunctor.M F)] : PFunctor.Approx.Path F → PFunctor.M F → PFunctor.M F

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

• One or more equations did not get rendered due to their size.
• PFunctor.M.isubtree [] x = x

def PFunctor.M.iselect {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) : PFunctor.M F → 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.head (PFunctor.M.isubtree ps x)

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

@[simp]

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

theorem PFunctor.M.children_mk {F : PFunctor.{u}} {a : F.A} (x : F.B a → PFunctor.M F) (i : F.B (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x }))) : PFunctor.M.children (PFunctor.M.mk { fst := a, snd := x }) i = x (cast (_ : F.B (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x })) = F.B a) i)

@[simp]

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

@[simp]

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

@[simp]

theorem PFunctor.M.iselect_nil {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited (PFunctor.M F)] {a : F.A} (f : F.B a → PFunctor.M F) : PFunctor.M.iselect [] (PFunctor.M.mk { fst := a, snd := f }) = a

@[simp]

theorem PFunctor.M.iselect_cons {F : PFunctor.{u}} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) {a : F.A} (f : F.B a → PFunctor.M F) {i : F.B a} : PFunctor.M.iselect ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := 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 (PFunctor.map F (PFunctor.M.corec f) (f x₀))

theorem PFunctor.M.ext_aux {F : PFunctor.{u}} [Inhabited (PFunctor.M F)] [DecidableEq F.A] {n : ℕ} (x : PFunctor.M F) (y : PFunctor.M F) (z : PFunctor.M F) (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 (PFunctor.M F)] (x : PFunctor.M F) (y : PFunctor.M F) (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 : PFunctor.M F → PFunctor.M F → Prop) : Prop

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

• head : ∀ {a a' : F.A} {f : F.B a → PFunctor.M F} {f' : F.B a' → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a', snd := f' }) → a = a'

  The head of the trees are equal

• tail : ∀ {a : F.A} {f f' : F.B a → PFunctor.M F}, R (PFunctor.M.mk { fst := a, snd := f }) (PFunctor.M.mk { fst := a, snd := f' }) → ∀ (i : F.B a), R (f i) (f' i)

  The tails are equal

theorem PFunctor.M.nth_of_bisim {F : PFunctor.{u}} (R : PFunctor.M F → PFunctor.M F → Prop) [Inhabited (PFunctor.M F)] (bisim : PFunctor.M.IsBisimulation R) (s₁ : PFunctor.M F) (s₂ : PFunctor.M F) (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 → PFunctor.M F) (f' : F.B a → PFunctor.M F), PFunctor.M.isubtree ps s₁ = PFunctor.M.mk { fst := a, snd := f } ∧ PFunctor.M.isubtree ps s₂ = PFunctor.M.mk { fst := a, snd := f' } ∧ ∀ (i : F.B a), R (f i) (f' i)

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

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

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.dest (PFunctor.M.corec g x) = PFunctor.map P (PFunctor.M.corec g) (g x)

theorem PFunctor.M.bisim {P : PFunctor.{u}} (R : PFunctor.M P → PFunctor.M P → Prop) (h : ∀ (x y : PFunctor.M P), R x y → ∃ (a : P.A) (f : P.B a → PFunctor.M P) (f' : P.B a → PFunctor.M P), PFunctor.M.dest x = { fst := a, snd := f } ∧ PFunctor.M.dest y = { fst := a, snd := f' } ∧ ∀ (i : P.B a), R (f i) (f' i)) (x : PFunctor.M P) (y : PFunctor.M P) : R x y → x = y

theorem PFunctor.M.bisim' {P : PFunctor.{u}} {α : Type u_3} (Q : α → Prop) (u : α → PFunctor.M P) (v : α → PFunctor.M P) (h : ∀ (x : α), Q x → ∃ (a : P.A) (f : P.B a → PFunctor.M P) (f' : P.B a → PFunctor.M P), PFunctor.M.dest (u x) = { fst := a, snd := f } ∧ PFunctor.M.dest (v x) = { fst := a, snd := 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 : PFunctor.M P → PFunctor.M P → Prop) (h : ∀ (x y : PFunctor.M P), R x y → ∃ (a : P.A) (f : P.B a → PFunctor.M P) (f' : P.B a → PFunctor.M P), PFunctor.M.dest x = { fst := a, snd := f } ∧ PFunctor.M.dest y = { fst := a, snd := f' } ∧ ∀ (i : P.B a), R (f i) (f' i)) (x : PFunctor.M P) (y : PFunctor.M P) : R x y → x = y

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

def PFunctor.M.corec₁ {P : PFunctor.{u}} {α : Type u} (F : (X : Type u) → (α → X) → α → ↑P X) : α → PFunctor.M P

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) → α → PFunctor.M P ⊕ ↑P X) (x : α) : PFunctor.M P

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.