Documentation

Mathlib.Data.PFunctor.Multivariate.W

The W construction as a multivariate polynomial functor. #

W types are well-founded tree-like structures. They are defined as the least fixpoint of a polynomial functor.

Main definitions #

Implementation notes #

Three views of M-types:

Specifically, we define the polynomial functor wp as:

As a result wp.Obj α is made of a dataless tree and a function from its valid paths to values of α

Reference #

inductive MvPFunctor.WPath {n : } (P : MvPFunctor (n + 1)) :

A path from the root of a tree to one of its node

Instances For

    Specialized destructor on WPath

    Instances For

      Specialized destructor on WPath

      Instances For

        Specialized destructor on WPath

        Instances For
          def MvPFunctor.wp {n : } (P : MvPFunctor (n + 1)) :

          Polynomial functor for the W-type of P. A is a data-less well-founded tree whereas, for a given a : A, B a is a valid path in tree a so that Wp.obj α is made of a tree and a function from its valid paths to the values it contains

          Instances For
            def MvPFunctor.W {n : } (P : MvPFunctor (n + 1)) (α : TypeVec n) :

            W-type of P

            Instances For

              First, describe operations on W as a polynomial functor.

              def MvPFunctor.wpMk {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (a : P.A) (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :

              Constructor for wp

              Instances For
                def MvPFunctor.wpRec {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : Type u_1} (g : (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α(PFunctor.B (MvPFunctor.last P) aC) → C) (x : PFunctor.W (MvPFunctor.last P)) :
                Equations
                Instances For
                  theorem MvPFunctor.wpRec_eq {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : Type u_1} (g : (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α(PFunctor.B (MvPFunctor.last P) aC) → C) (a : P.A) (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) :
                  MvPFunctor.wpRec P g (WType.mk a f) f' = g a f f' fun i => MvPFunctor.wpRec P g (f i) (MvPFunctor.wPathDestRight P f' i)
                  theorem MvPFunctor.wp_ind {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : (x : PFunctor.W (MvPFunctor.last P)) → TypeVec.Arrow (MvPFunctor.WPath P x) αProp} (ih : (a : P.A) → (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) → (f' : TypeVec.Arrow (MvPFunctor.WPath P (WType.mk a f)) α) → ((i : PFunctor.B (MvPFunctor.last P) a) → C (f i) (MvPFunctor.wPathDestRight P f' i)) → C (WType.mk a f) f') (x : PFunctor.W (MvPFunctor.last P)) (f' : TypeVec.Arrow (MvPFunctor.WPath P x) α) :
                  C x f'

                  Now think of W as defined inductively by the data ⟨a, f', f⟩ where

                  def MvPFunctor.wMk {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) :

                  Constructor for W

                  Instances For
                    def MvPFunctor.wRec {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α(PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) → (PFunctor.B (MvPFunctor.last P) aC) → C) :
                    MvPFunctor.W P αC

                    Recursor for W

                    Instances For
                      theorem MvPFunctor.wRec_eq {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : Type u_1} (g : (a : P.A) → TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α(PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) → (PFunctor.B (MvPFunctor.last P) aC) → C) (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) :
                      MvPFunctor.wRec P g (MvPFunctor.wMk P a f' f) = g a f' f fun i => MvPFunctor.wRec P g (f i)

                      Defining equation for the recursor of W

                      theorem MvPFunctor.w_ind {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : MvPFunctor.W P αProp} (ih : (a : P.A) → (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) → (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) → ((i : PFunctor.B (MvPFunctor.last P) a) → C (f i)) → C (MvPFunctor.wMk P a f' f)) (x : MvPFunctor.W P α) :
                      C x

                      Induction principle for W

                      theorem MvPFunctor.w_cases {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {C : MvPFunctor.W P αProp} (ih : (a : P.A) → (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) → (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) → C (MvPFunctor.wMk P a f' f)) (x : MvPFunctor.W P α) :
                      C x
                      def MvPFunctor.wMap {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : TypeVec n} (g : TypeVec.Arrow α β) :

                      W-types are functorial

                      Instances For
                        theorem MvPFunctor.wMk_eq {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (a : P.A) (f : PFunctor.B (MvPFunctor.last P) aPFunctor.W (MvPFunctor.last P)) (g' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (g : (j : PFunctor.B (MvPFunctor.last P) a) → TypeVec.Arrow (MvPFunctor.WPath P (f j)) α) :
                        (MvPFunctor.wMk P a g' fun i => { fst := f i, snd := g i }) = { fst := WType.mk a f, snd := MvPFunctor.wPathCasesOn P g' g }
                        theorem MvPFunctor.w_map_wMk {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : TypeVec n} (g : TypeVec.Arrow α β) (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) :
                        MvFunctor.map g (MvPFunctor.wMk P a f' f) = MvPFunctor.wMk P a (TypeVec.comp g f') fun i => MvFunctor.map g (f i)
                        @[reducible]
                        def MvPFunctor.objAppend1 {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aβ) :

                        Constructor of a value of P.obj (α ::: β) from components. Useful to avoid complicated type annotation

                        Instances For
                          theorem MvPFunctor.map_objAppend1 {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {γ : TypeVec n} (g : TypeVec.Arrow α γ) (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) :

                          Yet another view of the W type: as a fixed point for a multivariate polynomial functor. These are needed to use the W-construction to construct a fixed point of a qpf, since the qpf axioms are expressed in terms of map on P.

                          def MvPFunctor.wMk' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} :

                          Constructor for the W-type of P

                          Instances For
                            def MvPFunctor.wDest' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} :

                            Destructor for the W-type of P

                            Instances For
                              theorem MvPFunctor.wDest'_wMk {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (a : P.A) (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aMvPFunctor.W P α) :
                              MvPFunctor.wDest' P (MvPFunctor.wMk P a f' f) = { fst := a, snd := TypeVec.splitFun f' f }
                              theorem MvPFunctor.wDest'_wMk' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (x : MvPFunctor.Obj P (α ::: MvPFunctor.W P α)) :