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 [ACH19] for more details.

Reference

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. Data Types as Quotients of Polynomial Functors

def MvQPF.corecF {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) : β → (MvQPF.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

Equations

• MvQPF.corecF g = MvPFunctor.M.corec (MvQPF.P F) fun (x : β) => MvQPF.repr (g x)

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 (MvQPF.P F) (MvQPF.corecF g x) = MvFunctor.map (TypeVec.id ::: MvQPF.corecF g) (MvQPF.repr (g x))

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

Characterization of desirable equivalence relations on M-types

Equations

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

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

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

Equations

• MvQPF.Mcongr x y = ∃ (r : (MvQPF.P F).M α → (MvQPF.P F).M α → Prop), MvQPF.IsPrecongr r ∧ r x y

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)

Equations

• MvQPF.Cofix F α = Quot MvQPF.Mcongr

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

Equations

• MvQPF.instInhabitedCofixOfAP = { default := Quot.mk MvQPF.Mcongr default }

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

maps every element of the W type to a canonical representative

Equations

• MvQPF.mRepr = MvQPF.corecF (MvQPF.abs ∘ MvPFunctor.M.dest (MvQPF.P F))

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

the map function for the functor Cofix F

Equations

• MvQPF.Cofix.map g = Quot.lift (fun (x : (MvQPF.P F).M α) => Quot.mk MvQPF.Mcongr (MvFunctor.map g x)) ⋯

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

Equations

• MvQPF.Cofix.mvfunctor = { map := @MvQPF.Cofix.map n F q }

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

Corecursor for Cofix F

Equations

• MvQPF.Cofix.corec g x = Quot.mk MvQPF.Mcongr (MvQPF.corecF g x)

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

Destructor for Cofix F

Equations

• MvQPF.Cofix.dest = Quot.lift (fun (x : (MvQPF.P F).M α) => MvFunctor.map (TypeVec.id ::: Quot.mk MvQPF.Mcongr) (MvQPF.abs (MvPFunctor.M.dest (MvQPF.P F) x))) ⋯

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

Abstraction function for cofix F α

Equations

• MvQPF.Cofix.abs = Quot.mk MvQPF.Mcongr

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

Representation function for Cofix F α

Equations

• MvQPF.Cofix.repr = MvPFunctor.M.corec (MvQPF.P F) (MvQPF.repr ∘ MvQPF.Cofix.dest)

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 : β) : MvQPF.Cofix F α

Corecursor for Cofix F

Equations

• MvQPF.Cofix.corec'₁ g x = MvQPF.Cofix.corec (fun (x : β) => g id) x

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

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

Equations

• MvQPF.Cofix.corec' g x = MvQPF.Cofix.corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ MvQPF.Cofix.dest) g) (Sum.inr x)

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

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

Equations

• MvQPF.Cofix.corec₁ g x = MvQPF.Cofix.corec' (fun (x : β) => g Sum.inl Sum.inr x) x

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

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

constructor for Cofix F

Equations

• MvQPF.Cofix.mk = MvQPF.Cofix.corec fun (x : F (α ::: MvQPF.Cofix F α)) => MvFunctor.map (TypeVec.id ::: fun (i : MvQPF.Cofix F α) => i.dest) x

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 : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop) (h : ∀ (x y : MvQPF.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 : MvQPF.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 : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop) (h : ∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR (fun {i : Fin2 (n + 1)} => α.RelLast r) x.dest y.dest) (x y : MvQPF.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 : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop) (h : ∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) (x y : MvQPF.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 : β → MvQPF.Cofix F α) (h : ∀ (x : β), Q x → ∃ (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f₀ : (MvQPF.P F).last.B a → MvQPF.Cofix F α) (f₁ : (MvQPF.P F).last.B a → MvQPF.Cofix F α), (u x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₁⟩ ∧ ∀ (i : (MvQPF.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 : MvQPF.Cofix F α) : MvQPF.Cofix.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 (α ::: MvQPF.Cofix F α)) : (MvQPF.Cofix.mk x).dest = x

theorem MvQPF.Cofix.ext {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : MvQPF.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 (α ::: MvQPF.Cofix F α)) (h : MvQPF.Cofix.mk x = MvQPF.Cofix.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 : MvQPF.Cofix F α) : Quot.mk MvQPF.Mcongr x.repr = x

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

tactic for proof by bisimulation

Equations

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

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)) : 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} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))) (x : β) : (MvQPF.Cofix.corec' g x).dest = MvFunctor.map (TypeVec.id ::: Sum.elim id (MvQPF.Cofix.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} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β) (h : ∀ (X Y : Type u) (f : MvQPF.Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) : (MvQPF.Cofix.corec₁ g x).dest = g id (MvQPF.Cofix.corec₁ g) x

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

Equations

• MvQPF.mvqpfCofix = MvQPF.mk (MvQPF.P F).mp (fun {α : TypeVec.{?u.40} n} => Quot.mk MvQPF.Mcongr) (fun {α : TypeVec.{?u.40} n} => MvQPF.Cofix.repr) ⋯ ⋯