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 α is made of a dataless tree and a function from its valid paths to values of α

Reference #

inductive MvPFunctor.WPath {n : } (P : MvPFunctor.{u} (n + 1)) :
P.last.WFin2 nType u

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

  • root: {n : } → {P : MvPFunctor.{u} (n + 1)} → (a : P.A) → (f : P.last.B aP.last.W) → (i : Fin2 n) → P.drop.B a iP.WPath (WType.mk a f) i
  • child: {n : } → {P : MvPFunctor.{u} (n + 1)} → (a : P.A) → (f : P.last.B aP.last.W) → (i : Fin2 n) → (j : P.last.B a) → P.WPath (f j) iP.WPath (WType.mk a f) i
Instances For
    instance MvPFunctor.WPath.inhabited {n : } (P : MvPFunctor.{u} (n + 1)) (x : P.last.W) {i : Fin2 n} [I : Inhabited (P.drop.B x.head i)] :
    Inhabited (P.WPath x i)
    Equations
    def MvPFunctor.wPathCasesOn {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α) :
    TypeVec.Arrow (P.WPath (WType.mk a f)) α

    Specialized destructor on WPath

    Equations
    Instances For
      def MvPFunctor.wPathDestLeft {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (h : TypeVec.Arrow (P.WPath (WType.mk a f)) α) :
      (P.drop.B a).Arrow α

      Specialized destructor on WPath

      Equations
      Instances For
        def MvPFunctor.wPathDestRight {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (h : TypeVec.Arrow (P.WPath (WType.mk a f)) α) (j : P.last.B a) :
        TypeVec.Arrow (P.WPath (f j)) α

        Specialized destructor on WPath

        Equations
        Instances For
          theorem MvPFunctor.wPathDestLeft_wPathCasesOn {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α) :
          P.wPathDestLeft (P.wPathCasesOn g' g) = g'
          theorem MvPFunctor.wPathDestRight_wPathCasesOn {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α) :
          P.wPathDestRight (P.wPathCasesOn g' g) = g
          theorem MvPFunctor.wPathCasesOn_eta {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B aP.last.W} (h : TypeVec.Arrow (P.WPath (WType.mk a f)) α) :
          P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h
          theorem MvPFunctor.comp_wPathCasesOn {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (h : α.Arrow β) {a : P.A} {f : P.last.B aP.last.W} (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α) :
          TypeVec.comp h (P.wPathCasesOn g' g) = P.wPathCasesOn (TypeVec.comp h g') fun (i : P.last.B a) => TypeVec.comp h (g i)

          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

          Equations
          • P.wp = { A := P.last.W, B := P.WPath }
          Instances For
            def MvPFunctor.W {n : } (P : MvPFunctor.{u} (n + 1)) (α : TypeVec.{u} n) :

            W-type of P

            Equations
            • P.W α = P.wp α
            Instances For
              instance MvPFunctor.mvfunctorW {n : } (P : MvPFunctor.{u} (n + 1)) :
              Equations
              • P.mvfunctorW = id inferInstance

              First, describe operations on W as a polynomial functor.

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

              Constructor for wp

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

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

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

                  Constructor for W

                  Equations
                  • P.wMk a f' f = WType.mk a fun (i : P.last.B a) => (f i).fst, P.wPathCasesOn f' fun (i : P.last.B a) => (f i).snd
                  Instances For
                    def MvPFunctor.wRec {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Type u_1} (g : (a : P.A) → (P.drop.B a).Arrow α(P.last.B aP.W α)(P.last.B aC)C) :
                    P.W αC

                    Recursor for W

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem MvPFunctor.wRec_eq {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Type u_1} (g : (a : P.A) → (P.drop.B a).Arrow α(P.last.B aP.W α)(P.last.B aC)C) (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B aP.W α) :
                      P.wRec g (P.wMk a f' f) = g a f' f fun (i : P.last.B a) => P.wRec g (f i)

                      Defining equation for the recursor of W

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

                      Induction principle for W

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

                      W-types are functorial

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

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

                        Equations
                        Instances For
                          theorem MvPFunctor.map_objAppend1 {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {γ : TypeVec.{u} n} (g : α.Arrow γ) (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B aP.W α) :
                          MvFunctor.map (g ::: P.wMap g) (P.objAppend1 a f' f) = P.objAppend1 a (TypeVec.comp g f') fun (x : P.last.B a) => P.wMap g (f x)

                          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.{u} (n + 1)) {α : TypeVec.{u} n} :
                          P (α ::: P.W α)P.W α

                          Constructor for the W-type of P

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

                            Destructor for the W-type of P

                            Equations
                            • P.wDest' = P.wRec fun (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B aP.W α) (x : P.last.B aP (α ::: P.W α)) => a, TypeVec.splitFun f' f
                            Instances For
                              theorem MvPFunctor.wDest'_wMk {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B aP.W α) :
                              P.wDest' (P.wMk a f' f) = a, TypeVec.splitFun f' f
                              theorem MvPFunctor.wDest'_wMk' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : P (α ::: P.W α)) :
                              P.wDest' (P.wMk' x) = x