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 #

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 α.

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

Reference #

def MvQPF.recF {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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
  • One or more equations did not get rendered due to their size.
Instances For
    theorem MvQPF.recF_eq {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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 α) :
    MvQPF.recF g ((MvQPF.P F).wMk a f' f) = g (MvQPF.abs a, TypeVec.splitFun f' (MvQPF.recF g f))
    theorem MvQPF.recF_eq' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β)β) (x : (MvQPF.P F).W α) :
    MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))
    inductive MvQPF.WEquiv {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
    (MvQPF.P F).W α(MvQPF.P F).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.{u} (n + 1)Type u} [q : MvQPF F] (α : TypeVec.{u} n) {β : Type u} (u : F (α ::: β)β) (x : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) :
      theorem MvQPF.wEquiv.abs' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) (h : MvQPF.abs ((MvQPF.P F).wDest' x) = MvQPF.abs ((MvQPF.P F).wDest' y)) :
      theorem MvQPF.wEquiv.refl {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α) :
      theorem MvQPF.wEquiv.symm {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) :
      def MvQPF.wrepr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
      (MvQPF.P F).W α(MvQPF.P F).W α

      maps every element of the W type to a canonical representative

      Equations
      Instances For
        theorem MvQPF.wrepr_wMk {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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.wrepr ((MvQPF.P F).wMk a f' f) = (MvQPF.P F).wMk' (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) a, (MvQPF.P F).appendContents f' f)))
        theorem MvQPF.wrepr_equiv {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α) :
        theorem MvQPF.wEquiv_map {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) (x : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) :
        def MvQPF.wSetoid {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] (α : TypeVec.{u} n) :
        Setoid ((MvQPF.P F).W α)

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

        Equations
        Instances For
          def MvQPF.Fix {n : } (F : TypeVec.{u_1} (n + 1)Type u_1) [q : MvQPF F] (α : TypeVec.{u_1} 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
            def MvQPF.Fix.map {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) :
            MvQPF.Fix F αMvQPF.Fix F β

            Fix F is a functor

            Equations
            Instances For
              instance MvQPF.Fix.mvfunctor {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] :
              Equations
              • MvQPF.Fix.mvfunctor = { map := fun {α β : TypeVec.{?u.39} n} => MvQPF.Fix.map }
              def MvQPF.Fix.rec {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β)β) :
              MvQPF.Fix F αβ

              Recursor for Fix F

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

                Access W-type underlying Fix F

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

                  Constructor for Fix F

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

                    Destructor for Fix F

                    Equations
                    Instances For
                      theorem MvQPF.Fix.rec_eq {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β)β) (x : F (α ::: MvQPF.Fix F α)) :
                      theorem MvQPF.Fix.ind_aux {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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).appendContents f' fun (x : (MvQPF.P F).last.B a) => f x) = (MvQPF.P F).wMk a f' f
                      theorem MvQPF.Fix.ind_rec {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g₁ : MvQPF.Fix F αβ) (g₂ : MvQPF.Fix F αβ) (h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (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.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Fix F α) :
                      MvQPF.Fix.mk x.dest = x
                      theorem MvQPF.Fix.dest_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Fix F α)) :
                      (MvQPF.Fix.mk x).dest = x
                      theorem MvQPF.Fix.ind {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (p : MvQPF.Fix F αProp) (h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.LiftP (α.PredLast p) xp (MvQPF.Fix.mk x)) (x : MvQPF.Fix F α) :
                      p x
                      instance MvQPF.mvqpfFix {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      def MvQPF.Fix.drec {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} 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
                      Instances For