mathlib3 documentation

data.qpf.multivariate.constructions.fix

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Reference #

def mvqpf.recF {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : 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).arrow α) (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 α) (h : mvqpf.abs ((mvqpf.P F).W_dest' x) = mvqpf.abs ((mvqpf.P F).W_dest' y)) :
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).arrow α) (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 : α.arrow β) (x y : (mvqpf.P F).W α) :
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 n) :
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)
Equations
Instances for mvqpf.fix
def mvqpf.fix.map {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} (g : α.arrow β) :

fix F is a functor

Equations
@[protected, 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} (g : 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} (x : 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).arrow α) (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 α)), mvfunctor.map (typevec.id ::: g₁) x = mvfunctor.map (typevec.id ::: g₂) x g₁ (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 α β) (hyp : (x : F ::: mvqpf.fix F α)), h (mvqpf.fix.mk x) = g (mvfunctor.map (typevec.id ::: h) x)) :
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) x p (mvqpf.fix.mk x)) (x : mvqpf.fix F α) :
p x
@[protected, 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 (mvfunctor.map (typevec.id ::: sigma.fst) x))) (x : mvqpf.fix F α) :
β x

Dependent recursor for fix F

Equations