The final co-algebra of a multivariate qpf is again a qpf.

For a (n+1)-ary QPF F (α₀,..,αₙ), we take the least fixed point of F with regards to its last argument αₙ. The result is an n-ary functor: Fix F (α₀,..,αₙ₋₁). Making Fix F into a functor allows us to take the fixed point, compose with other functors and take a fixed point again.

Main definitions

• Cofix.mk - constructor
• Cofix.dest - destructor
• Cofix.corec - corecursor: useful for formulating infinite, productive computations
• Cofix.bisim - bisimulation: proof technique to show the equality of possibly infinite values of Cofix F α

Implementation notes

For F a QPF, we define Cofix F α in terms of the M-type of the polynomial functor P of F. We define the relation Mcongr and take its quotient as the definition of Cofix F α.

Mcongr is taken as the weakest bisimulation on M-type. See [avigad-carneiro-hudon2019] for more details.

Reference

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]

def MvQPF.corecF {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) : β → (P F).M α

corecF is used as a basis for defining the corecursor of Cofix F α. corecF uses corecursion to construct the M-type generated by q.P and uses function on F as a corecursive step

theorem MvQPF.corecF_eq {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) (x : β) : MvPFunctor.M.dest (P F) (corecF g x) = MvFunctor.map (TypeVec.id ::: corecF g) (repr (g x))

def MvQPF.IsPrecongr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : (P F).M α → (P F).M α → Prop) : Prop

Characterization of desirable equivalence relations on M-types

def MvQPF.Mcongr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : (P F).M α) : Prop

Equivalence relation on M-types representing a value of type Cofix F

def MvQPF.Cofix {n : ℕ} (F : TypeVec.{u} (n + 1) → Type u) [MvQPF F] (α : TypeVec.{u} n) : Type u

Greatest fixed point of functor F. The result is a functor with one fewer parameters than the input. For F a b c a ternary functor, fix F is a binary functor such that

Cofix F a b = F a b (Cofix F a b)

instance MvQPF.instInhabitedCofixOfAP {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} [Inhabited (P F).A] [(i : Fin2 n) → Inhabited (α i)] : Inhabited (Cofix F α)

def MvQPF.mRepr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : (P F).M α → (P F).M α

maps every element of the W type to a canonical representative

def MvQPF.Cofix.map {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α β : TypeVec.{u} n} (g : α.Arrow β) : Cofix F α → Cofix F β

the map function for the functor Cofix F

instance MvQPF.Cofix.mvfunctor {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] : MvFunctor (Cofix F)

def MvQPF.Cofix.corec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) : β → Cofix F α

Corecursor for Cofix F

def MvQPF.Cofix.dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : Cofix F α → F (α ::: Cofix F α)

Destructor for Cofix F

def MvQPF.Cofix.abs {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : (P F).M α → Cofix F α

Abstraction function for cofix F α

def MvQPF.Cofix.repr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : Cofix F α → (P F).M α

Representation function for Cofix F α

def MvQPF.Cofix.corec'₁ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (β → X) → F (α ::: X)) (x : β) : Cofix F α

Corecursor for Cofix F

def MvQPF.Cofix.corec' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: (Cofix F α ⊕ β))) (x : β) : Cofix F α

More flexible corecursor for Cofix F. Allows the return of a fully formed value instead of making a recursive call

def MvQPF.Cofix.corec₁ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β) : Cofix F α

Corecursor for Cofix F. The shape allows recursive calls to look like recursive calls.

theorem MvQPF.Cofix.dest_corec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) (x : β) : (corec g x).dest = MvFunctor.map (TypeVec.id ::: corec g) (g x)

def MvQPF.Cofix.mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : F (α ::: Cofix F α) → Cofix F α

constructor for Cofix F

Bisimulation principles for Cofix F

The following theorems are bisimulation principles. The general idea is to use a bisimulation relation to prove the equality between specific values of type Cofix F α.

A bisimulation relation R for values x y : Cofix F α:

• holds for x y: R x y
• for any values x y that satisfy R, their root has the same shape and their children can be paired in such a way that they satisfy R.

theorem MvQPF.Cofix.bisim_rel {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : Cofix F α → Cofix F α → Prop) (h : ∀ (x y : Cofix F α), r x y → MvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) (x y : Cofix F α) : r x y → x = y

Bisimulation principle using map and Quot.mk to match and relate children of two trees.

theorem MvQPF.Cofix.bisim {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : Cofix F α → Cofix F α → Prop) (h : ∀ (x y : Cofix F α), r x y → MvFunctor.LiftR (α.RelLast r) x.dest y.dest) (x y : Cofix F α) : r x y → x = y

Bisimulation principle using LiftR to match and relate children of two trees.

theorem MvQPF.Cofix.bisim₂ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : Cofix F α → Cofix F α → Prop) (h : ∀ (x y : Cofix F α), r x y → MvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) (x y : Cofix F α) : r x y → x = y

Bisimulation principle using LiftR' to match and relate children of two trees.

theorem MvQPF.Cofix.bisim' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u_1} (Q : β → Prop) (u v : β → Cofix F α) (h : ∀ (x : β), Q x → ∃ (a : (P F).A) (f' : ((P F).drop.B a).Arrow α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α), (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧ ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x') (x : β) : Q x → u x = v x

Bisimulation principle the values ⟨a,f⟩ of the polynomial functor representing Cofix F α as well as an invariant Q : β → Prop and a state β generating the left-hand side and right-hand side of the equality through functions u v : β → Cofix F α

theorem MvQPF.Cofix.mk_dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : Cofix F α) : mk x.dest = x

theorem MvQPF.Cofix.dest_mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: Cofix F α)) : (mk x).dest = x

theorem MvQPF.Cofix.ext {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : Cofix F α) (h : x.dest = y.dest) : x = y

theorem MvQPF.Cofix.ext_mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : F (α ::: Cofix F α)) (h : mk x = mk y) : x = y

liftR_map, liftR_map_last and liftR_map_last' are useful for reasoning about the induction step in bisimulation proofs.

theorem MvQPF.liftR_map {n : ℕ} {α β : TypeVec.{u_1} n} {F' : TypeVec.{u_1} n → Type u} [MvFunctor F'] [LawfulMvFunctor F'] (R : (β.prod β).Arrow (TypeVec.repeat n Prop)) (x : F' α) (f g : α.Arrow β) (h : α.Arrow (TypeVec.Subtype_ R)) (hh : TypeVec.comp (TypeVec.subtypeVal R) h = TypeVec.comp (TypeVec.prod.map f g) TypeVec.prod.diag) : MvFunctor.LiftR' R (MvFunctor.map f x) (MvFunctor.map g x)

theorem MvQPF.liftR_map_last {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [lawful : LawfulMvFunctor F] {α : TypeVec.{u} n} {ι ι' : Type u} (R : ι' → ι' → Prop) (x : F (α ::: ι)) (f g : ι → ι') (hh : ∀ (x : ι), R (f x) (g x)) : MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) (MvFunctor.map (TypeVec.id ::: g) x)

theorem MvQPF.liftR_map_last' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {ι : Type u} (R : ι → ι → Prop) (x : F (α ::: ι)) (f : ι → ι) (hh : ∀ (x : ι), R (f x) x) : MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) x

theorem MvQPF.Cofix.abs_repr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : Cofix F α) : Quot.mk Mcongr x.repr = x

def Mathlib.Tactic.MvBisim.tacticMv_bisim___With___ : Lean.ParserDescr

tactic for proof by bisimulation

theorem MvQPF.corec_roll {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {X Y : Type u} {x₀ : X} (f : X → Y) (g : Y → F (α ::: X)) : Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)

theorem MvQPF.Cofix.dest_corec' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: (Cofix F α ⊕ β))) (x : β) : (corec' g x).dest = MvFunctor.map (TypeVec.id ::: Sum.elim id (corec' g)) (g x)

theorem MvQPF.Cofix.dest_corec₁ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β) (h : ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) : (corec₁ g x).dest = g id (corec₁ g) x

instance MvQPF.mvqpfCofix {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] : MvQPF (Cofix F)