mathlib documentation

data.qpf.multivariate.constructions.fix

The initial 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 a 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

Implementation notes

For F a QPF, we definefix F αin terms of the W-type of the polynomial functorPofF. We define the relationWequivand take its quotient as the definition offix F α`.

inductive Wequiv {α : typevec n} : q.P.W α  q.P.W α  Prop
| ind (a : q.P.A) (f' : q.P.drop.B a  α) (f₀ f₁ : q.P.last.B a  q.P.W α) :
    ( x, Wequiv (f₀ x) (f₁ x))  Wequiv (q.P.W_mk a f' f₀) (q.P.W_mk a f' f₁)
| abs (a₀ : q.P.A) (f'₀ : q.P.drop.B a₀  α) (f₀ : q.P.last.B a₀  q.P.W α)
      (a₁ : q.P.A) (f'₁ : q.P.drop.B a₁  α) (f₁ : q.P.last.B a₁  q.P.W α) :
      abs a₀, q.P.append_contents f'₀ f₀ = abs a₁, q.P.append_contents f'₁ f₁ 
        Wequiv (q.P.W_mk a₀ f'₀ f₀) (q.P.W_mk a₁ f'₁ f₁)
| trans (u v w : q.P.W α) : Wequiv u v  Wequiv v w  Wequiv u w

See [avigad-carneiro-hudon2019] for more details.

Reference

def mvqpf.recF {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(F ::: β) → β)(mvqpf.P F).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

Equations
theorem mvqpf.recF_eq {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) → β) (a : (mvqpf.P F).A) (f' : (mvqpf.P F).drop.B a α) (f : (mvqpf.P F).last.B a(mvqpf.P F).W α) :

theorem mvqpf.recF_eq' {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) → β) (x : (mvqpf.P F).W α) :

inductive mvqpf.Wequiv {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).W α(mvqpf.P F).W α → Prop

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

theorem mvqpf.recF_eq_of_Wequiv {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] (α : typevec n) {β : Type u} (u : F ::: β) → β) (x y : (mvqpf.P F).W α) :

theorem mvqpf.Wequiv.abs' {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : (mvqpf.P F).W α) :

theorem mvqpf.Wequiv.refl {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : (mvqpf.P F).W α) :

theorem mvqpf.Wequiv.symm {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : (mvqpf.P F).W α) :

def mvqpf.Wrepr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).W α(mvqpf.P F).W α

maps every element of the W type to a canonical representative

Equations
theorem mvqpf.Wrepr_W_mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (a : (mvqpf.P F).A) (f' : (mvqpf.P F).drop.B a α) (f : (mvqpf.P F).last.B a(mvqpf.P F).W α) :

theorem mvqpf.Wrepr_equiv {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : (mvqpf.P F).W α) :

theorem mvqpf.Wequiv_map {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} (g : α β) (x y : (mvqpf.P F).W α) :
mvqpf.Wequiv x ymvqpf.Wequiv (g <$$> x) (g <$$> y)

def mvqpf.W_setoid {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] (α : typevec n) :
setoid ((mvqpf.P F).W α)

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

Equations
@[nolint]
def mvqpf.fix {n : } (F : typevec (n + 1)Type u_1) [mvfunctor F] [q : mvqpf F] :
typevec nType 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)
Equations
def mvqpf.fix.map {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} :
α βmvqpf.fix F αmvqpf.fix F β

fix F is a functor

Equations
@[instance]
def mvqpf.fix.mvfunctor {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] :

Equations
def mvqpf.fix.rec {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(F ::: β) → β)mvqpf.fix F α → β

Recursor for fix F

Equations
def mvqpf.fix_to_W {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
mvqpf.fix F α(mvqpf.P F).W α

Access W-type underlying fix F

Equations
def mvqpf.fix.mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
F ::: mvqpf.fix F α)mvqpf.fix F α

Constructor for fix F

Equations
def mvqpf.fix.dest {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
mvqpf.fix F αF ::: mvqpf.fix F α)

Destructor for fix F

Equations
theorem mvqpf.fix.rec_eq {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) → β) (x : F ::: mvqpf.fix F α)) :

theorem mvqpf.fix.ind_aux {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (a : (mvqpf.P F).A) (f' : (mvqpf.P F).drop.B a α) (f : (mvqpf.P F).last.B a(mvqpf.P F).W α) :
mvqpf.fix.mk (mvqpf.abs a, (mvqpf.P F).append_contents f' (λ (x : (mvqpf.P F).last.B a), f x)⟩) = (mvqpf.P F).W_mk a f' f

theorem mvqpf.fix.ind_rec {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g₁ g₂ : mvqpf.fix F α → β) (h : ∀ (x : F ::: mvqpf.fix F α)), (typevec.id ::: g₁) <$$> x = (typevec.id ::: g₂) <$$> xg₁ (mvqpf.fix.mk x) = g₂ (mvqpf.fix.mk x)) (x : mvqpf.fix F α) :
g₁ x = g₂ x

theorem mvqpf.fix.rec_unique {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) → β) (h : mvqpf.fix F α → β) :
(∀ (x : F ::: mvqpf.fix F α)), h (mvqpf.fix.mk x) = g ((typevec.id ::: h) <$$> x))mvqpf.fix.rec g = h

theorem mvqpf.fix.mk_dest {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : mvqpf.fix F α) :

theorem mvqpf.fix.dest_mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F ::: mvqpf.fix F α)) :

theorem mvqpf.fix.ind {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (p : mvqpf.fix F α → Prop) (h : ∀ (x : F ::: mvqpf.fix F α)), mvfunctor.liftp (α.pred_last p) xp (mvqpf.fix.mk x)) (x : mvqpf.fix F α) :
p x

@[instance]
def mvqpf.mvqpf_fix {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] :

Equations
def mvqpf.fix.drec {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : mvqpf.fix F αType u} (g : Π (x : F ::: sigma β)), β (mvqpf.fix.mk ((typevec.id ::: sigma.fst) <$$> x))) (x : mvqpf.fix F α) :
β x

Dependent recursor for fix F

Equations