# 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} [mvf : ] [q : ] {α : } {β : Type u} (g : β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

Equations
Instances For
theorem MvQPF.corecF_eq {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : βF (α ::: β)) (x : β) :
MvPFunctor.M.dest () () = MvFunctor.map (TypeVec.id ::: ) (MvQPF.repr (g x))
def MvQPF.IsPrecongr {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } (r : ().M α().M αProp) :

Characterization of desirable equivalence relations on M-types

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MvQPF.Mcongr {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } (x : ().M α) (y : ().M α) :

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

Equations
• = ∃ (r : ().M α().M αProp), r x y
Instances For
def MvQPF.Cofix {n : } (F : TypeVec.{u} (n + 1)Type u) [] [q : ] (α : ) :

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)

Equations
Instances For
instance MvQPF.instInhabitedCofixOfAP {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } [Inhabited ().A] [(i : Fin2 n) → Inhabited (α i)] :
Equations
• MvQPF.instInhabitedCofixOfAP = { default := Quot.mk MvQPF.Mcongr default }
def MvQPF.mRepr {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } :
().M α().M α

maps every element of the W type to a canonical representative

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

the map function for the functor Cofix F

Equations
Instances For
instance MvQPF.Cofix.mvfunctor {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] :
Equations
def MvQPF.Cofix.corec {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : βF (α ::: β)) :
β

Corecursor for Cofix F

Equations
Instances For
def MvQPF.Cofix.dest {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } :
F (α ::: )

Destructor for Cofix F

Equations
Instances For
def MvQPF.Cofix.abs {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } :
().M α

Abstraction function for cofix F α

Equations
Instances For
def MvQPF.Cofix.repr {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } :
().M α

Representation function for Cofix F α

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

Corecursor for Cofix F

Equations
Instances For
def MvQPF.Cofix.corec' {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : βF (α ::: ( β))) (x : β) :

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

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

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

Equations
Instances For
theorem MvQPF.Cofix.dest_corec {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : βF (α ::: β)) (x : β) :
().dest = MvFunctor.map (TypeVec.id ::: ) (g x)
def MvQPF.Cofix.mk {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } :
F (α ::: )

constructor for Cofix F

Equations
Instances For

## 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} [mvf : ] [q : ] {α : } (r : Prop) (h : ∀ (x y : ), r x yMvFunctor.map (TypeVec.id ::: ) x.dest = MvFunctor.map (TypeVec.id ::: ) y.dest) (x : ) (y : ) :
r x yx = 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} [mvf : ] [q : ] {α : } (r : Prop) (h : ∀ (x y : ), r x yMvFunctor.LiftR (fun {i : Fin2 (n + 1)} => α.RelLast r) x.dest y.dest) (x : ) (y : ) :
r x yx = 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} [mvf : ] [q : ] {α : } (r : Prop) (h : ∀ (x y : ), r x yMvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) (x : ) (y : ) :
r x yx = 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} [mvf : ] [q : ] {α : } {β : Type u_1} (Q : βProp) (u : β) (v : β) (h : ∀ (x : β), Q x∃ (a : ().A) (f' : (().drop.B a).Arrow α) (f₀ : ().last.B a) (f₁ : ().last.B a), (u x).dest = MvQPF.abs a, ().appendContents f' f₀ (v x).dest = MvQPF.abs a, ().appendContents f' f₁ ∀ (i : ().last.B a), ∃ (x' : β), Q x' f₀ i = u x' f₁ i = v x') (x : β) :
Q xu 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} [mvf : ] [q : ] {α : } (x : ) :
MvQPF.Cofix.mk x.dest = x
theorem MvQPF.Cofix.dest_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } (x : F (α ::: )) :
().dest = x
theorem MvQPF.Cofix.ext {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } (x : ) (y : ) (h : x.dest = y.dest) :
x = y
theorem MvQPF.Cofix.ext_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } (x : F (α ::: )) (y : F (α ::: )) (h : ) :
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 : } {α : } {β : } {F' : } [] [] (R : (β.prod β).Arrow ()) (x : F' α) (f : α.Arrow β) (g : α.Arrow β) (h : α.Arrow ()) (hh : = TypeVec.comp () TypeVec.prod.diag) :
theorem MvQPF.liftR_map_last {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [lawful : ] {α : } {ι : Type u} {ι' : 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} [mvf : ] [] {α : } {ι : 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 : ] {α : } (x : ) :
Quot.mk MvQPF.Mcongr x.repr = x

tactic for proof by bisimulation

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvQPF.corec_roll {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {X : Type u} {Y : Type u} {x₀ : X} (f : XY) (g : YF (α ::: X)) :
MvQPF.Cofix.corec (g f) x₀ = MvQPF.Cofix.corec (MvFunctor.map (TypeVec.id ::: f) g) (f x₀)
theorem MvQPF.Cofix.dest_corec' {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : βF (α ::: ( β))) (x : β) :
().dest = MvFunctor.map (TypeVec.id ::: ) (g x)
theorem MvQPF.Cofix.dest_corec₁ {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] {α : } {β : Type u} (g : {X : Type u} → (X)(βX)βF (α ::: X)) (x : β) (h : ∀ (X Y : Type u) (f : X) (f' : βX) (k : XY), g (k f) (k f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) :
().dest = g id x
instance MvQPF.mvqpfCofix {n : } {F : TypeVec.{u} (n + 1)Type u} [mvf : ] [q : ] :
Equations
• MvQPF.mvqpfCofix = { P := ().mp, abs := fun {α : } => Quot.mk MvQPF.Mcongr, repr := fun {α : } => MvQPF.Cofix.repr, abs_repr := , abs_map := }