# Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Fix

# The initial algebra of a multivariate qpf is again a qpf. #

For an (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 #

• Fix.mk - constructor
• Fix.dest - destructor
• Fix.rec - recursor: basis for defining functions by structural recursion on Fix F α
• Fix.drec - dependent recursor: generalization of Fix.rec where the result type of the function is allowed to depend on the Fix F α value
• Fix.rec_eq - defining equation for recursor
• Fix.ind - induction principle for Fix F α

## Implementation notes #

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

## Reference #

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
def MvQPF.recF {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α ::: β)β) :
MvPFunctor.W () αβ

recF is used as a basis for defining the recursor on Fix F α. recF traverses recursively the W-type generated by q.P using a function on F as a recursive step

Instances For
theorem MvQPF.recF_eq {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α ::: β)β) (a : ().A) (f' : TypeVec.Arrow () α) (f : PFunctor.B () aMvPFunctor.W () α) :
MvQPF.recF g (MvPFunctor.wMk () a f' f) = g (MvQPF.abs { fst := a, snd := TypeVec.splitFun f' ( f) })
theorem MvQPF.recF_eq' {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α ::: β)β) (x : MvPFunctor.W () α) :
= g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: ) ()))
inductive MvQPF.WEquiv {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } :
MvPFunctor.W () αMvPFunctor.W () αProp

Equivalence relation on W-types that represent the same Fix F value

Instances For
theorem MvQPF.recF_eq_of_wEquiv {n : } {F : TypeVec (n + 1)Type u} [] [q : ] (α : ) {β : Type u} (u : F (α ::: β)β) (x : MvPFunctor.W () α) (y : MvPFunctor.W () α) :
=
theorem MvQPF.wEquiv.abs' {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : MvPFunctor.W () α) (y : MvPFunctor.W () α) (h : MvQPF.abs () = MvQPF.abs ()) :
theorem MvQPF.wEquiv.refl {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : MvPFunctor.W () α) :
theorem MvQPF.wEquiv.symm {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : MvPFunctor.W () α) (y : MvPFunctor.W () α) :
def MvQPF.wrepr {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } :
MvPFunctor.W () αMvPFunctor.W () α

maps every element of the W type to a canonical representative

Instances For
theorem MvQPF.wrepr_wMk {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (a : ().A) (f' : TypeVec.Arrow () α) (f : PFunctor.B () aMvPFunctor.W () α) :
MvQPF.wrepr (MvPFunctor.wMk () a f' f) = MvPFunctor.wMk' () (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) { fst := a, snd := })))
theorem MvQPF.wrepr_equiv {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : MvPFunctor.W () α) :
theorem MvQPF.wEquiv_map {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : } (g : ) (x : MvPFunctor.W () α) (y : MvPFunctor.W () α) :
MvQPF.WEquiv () ()
def MvQPF.wSetoid {n : } {F : TypeVec (n + 1)Type u} [] [q : ] (α : ) :

Define the fixed point as the quotient of trees under the equivalence relation.

Instances For
def MvQPF.Fix {n : } (F : TypeVec (n + 1)Type u_1) [] [q : ] (α : ) :
Type u_1

Least 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

Fix F a b = F a b (Fix F a b)

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

Fix F is a functor

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

Recursor for Fix F

Instances For
def MvQPF.fixToW {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } :
MvPFunctor.W () α

Access W-type underlying Fix F

Instances For
def MvQPF.Fix.mk {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : F (α ::: )) :

Constructor for Fix F

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

Destructor for Fix F

Instances For
theorem MvQPF.Fix.rec_eq {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α ::: β)β) (x : F (α ::: )) :
= g (MvFunctor.map (TypeVec.id ::: ) x)
theorem MvQPF.Fix.ind_aux {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (a : ().A) (f' : TypeVec.Arrow () α) (f : PFunctor.B () aMvPFunctor.W () α) :
MvQPF.Fix.mk (MvQPF.abs { fst := a, snd := MvPFunctor.appendContents () f' fun x => Quotient.mk () (f x) }) = Quotient.mk () (MvPFunctor.wMk () a f' f)
theorem MvQPF.Fix.ind_rec {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g₁ : β) (g₂ : β) (h : ∀ (x : F (α ::: )), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) xg₁ () = g₂ ()) (x : ) :
g₁ x = g₂ x
theorem MvQPF.Fix.rec_unique {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α ::: β)β) (h : β) (hyp : ∀ (x : F (α ::: )), h () = g (MvFunctor.map (TypeVec.id ::: h) x)) :
theorem MvQPF.Fix.mk_dest {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : ) :
theorem MvQPF.Fix.dest_mk {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (x : F (α ::: )) :
theorem MvQPF.Fix.ind {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } (p : Prop) (h : (x : F (α ::: )) → p ()) (x : ) :
p x
instance MvQPF.mvqpfFix {n : } {F : TypeVec (n + 1)Type u} [] [q : ] :
def MvQPF.Fix.drec {n : } {F : TypeVec (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : (x : F (α ::: )) → β (MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) (x : ) :
β x

Dependent recursor for fix F

Instances For