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 (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} {β : Type u} (g : F (α ::: β)β) :
MvPFunctor.W (MvQPF.P F) αβ

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} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} {β : Type u} (g : F (α ::: β)β) (a : (MvQPF.P F).A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop (MvQPF.P F)) a) α) (f : PFunctor.B (MvPFunctor.last (MvQPF.P F)) aMvPFunctor.W (MvQPF.P F) α) :
    MvQPF.recF g (MvPFunctor.wMk (MvQPF.P F) a f' f) = g (MvQPF.abs { fst := a, snd := TypeVec.splitFun f' (MvQPF.recF g f) })
    theorem MvQPF.recF_eq' {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} {β : Type u} (g : F (α ::: β)β) (x : MvPFunctor.W (MvQPF.P F) α) :
    inductive MvQPF.WEquiv {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} :

    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} [MvFunctor F] [q : MvQPF F] (α : TypeVec n) {β : Type u} (u : F (α ::: β)β) (x : MvPFunctor.W (MvQPF.P F) α) (y : MvPFunctor.W (MvQPF.P F) α) :
      theorem MvQPF.wEquiv.abs' {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} (x : MvPFunctor.W (MvQPF.P F) α) (y : MvPFunctor.W (MvQPF.P F) α) (h : MvQPF.abs (MvPFunctor.wDest' (MvQPF.P F) x) = MvQPF.abs (MvPFunctor.wDest' (MvQPF.P F) y)) :
      theorem MvQPF.wEquiv.refl {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} (x : MvPFunctor.W (MvQPF.P F) α) :
      theorem MvQPF.wEquiv.symm {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} (x : MvPFunctor.W (MvQPF.P F) α) (y : MvPFunctor.W (MvQPF.P F) α) :
      def MvQPF.wrepr {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec n} :

      maps every element of the W type to a canonical representative

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

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

            Fix F is a functor

            Instances For
              instance MvQPF.Fix.mvfunctor {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] :
              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

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

                Access W-type underlying Fix F

                Instances For
                  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

                  Instances For
                    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

                    Instances For
                      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' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop (MvQPF.P F)) a) α) (f : PFunctor.B (MvPFunctor.last (MvQPF.P F)) aMvPFunctor.W (MvQPF.P F) α) :
                      theorem MvQPF.Fix.ind_rec {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec 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 (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 (TypeVec.PredLast α p) xp (MvQPF.Fix.mk x)) (x : MvQPF.Fix F α) :
                      p x
                      instance MvQPF.mvqpfFix {n : } {F : TypeVec (n + 1)Type u} [MvFunctor F] [q : MvQPF F] :
                      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

                      Instances For