Documentation

Mathlib.Data.PFunctor.Multivariate.M

The M construction as a multivariate polynomial functor. #

M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.

Main definitions #

Implementation notes #

Dual view of M-types:

Specifically, we define the polynomial functor mp as:

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

The difference with the polynomial functor of an initial algebra is that A is a possibly infinite tree.

Reference #

inductive MvPFunctor.M.Path {n : } (P : MvPFunctor.{u} (n + 1)) :
P.last.MFin2 nType u

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

Instances For
    instance MvPFunctor.M.Path.inhabited {n : } (P : MvPFunctor.{u} (n + 1)) (x : P.last.M) {i : Fin2 n} [Inhabited (P.drop.B x.head i)] :
    Equations

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

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

      n-ary M-type for P

      Equations
      • P.M α = P.mp α
      Instances For
        instance MvPFunctor.mvfunctorM {n : } (P : MvPFunctor.{u} (n + 1)) :
        Equations
        • P.mvfunctorM = id inferInstance
        instance MvPFunctor.inhabitedM {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} [I : Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
        Inhabited (P.M α)
        Equations
        def MvPFunctor.M.corecShape {n : } (P : MvPFunctor.{u} (n + 1)) {β : Type u} (g₀ : βP.A) (g₂ : (b : β) → P.last.B (g₀ b)β) :
        βP.last.M

        construct through corecursion the shape of an M-type without its contents

        Equations
        Instances For
          def MvPFunctor.castDropB {n : } (P : MvPFunctor.{u} (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :
          (P.drop.B a).Arrow (P.drop.B a')

          Proof of type equality as an arrow

          Equations
          Instances For
            def MvPFunctor.castLastB {n : } (P : MvPFunctor.{u} (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :
            P.last.B aP.last.B a'

            Proof of type equality as a function

            Equations
            Instances For
              def MvPFunctor.M.corecContents {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → (P.drop.B (g₀ b)).Arrow α) (g₂ : (b : β) → P.last.B (g₀ b)β) (x : P.last.M) (b : β) (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) :

              Using corecursion, construct the contents of an M-type

              Equations
              Instances For
                def MvPFunctor.M.corec' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → (P.drop.B (g₀ b)).Arrow α) (g₂ : (b : β) → P.last.B (g₀ b)β) :
                βP.M α

                Corecursor for M-type of P

                Equations
                Instances For
                  def MvPFunctor.M.corec {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : βP (α ::: β)) :
                  βP.M α

                  Corecursor for M-type of P

                  Equations
                  Instances For
                    def MvPFunctor.M.pathDestLeft {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {x : P.last.M} {a : P.A} {f : P.last.B aP.last.M} (h : x.dest = a, f) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                    (P.drop.B a).Arrow α

                    Implementation of destructor for M-type of P

                    Equations
                    Instances For
                      def MvPFunctor.M.pathDestRight {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {x : P.last.M} {a : P.A} {f : P.last.B aP.last.M} (h : x.dest = a, f) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) (j : P.last.B a) :

                      Implementation of destructor for M-type of P

                      Equations
                      Instances For
                        def MvPFunctor.M.dest' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a : P.A} {f : P.last.B aP.last.M} (h : x.dest = a, f) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                        P (α ::: P.M α)

                        Destructor for M-type of P

                        Equations
                        Instances For
                          def MvPFunctor.M.dest {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : P.M α) :
                          P (α ::: P.M α)

                          Destructor for M-types

                          Equations
                          Instances For
                            def MvPFunctor.M.mk {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} :
                            P (α ::: P.M α)P.M α

                            Constructor for M-types

                            Equations
                            Instances For
                              theorem MvPFunctor.M.dest'_eq_dest' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a₁ : P.A} {f₁ : P.last.B a₁P.last.M} (h₁ : x.dest = a₁, f₁) {a₂ : P.A} {f₂ : P.last.B a₂P.last.M} (h₂ : x.dest = a₂, f₂) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                              theorem MvPFunctor.M.dest_eq_dest' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a : P.A} {f : P.last.B aP.last.M} (h : x.dest = a, f) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                              theorem MvPFunctor.M.dest_corec' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → (P.drop.B (g₀ b)).Arrow α) (g₂ : (b : β) → P.last.B (g₀ b)β) (x : β) :
                              MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) = g₀ x, TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ g₂ x)
                              theorem MvPFunctor.M.dest_corec {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : βP (α ::: β)) (x : β) :
                              theorem MvPFunctor.M.bisim_lemma {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {a₁ : P.mp.A} {f₁ : (P.mp.B a₁).Arrow α} {a' : P.A} {f' : (P.B a').drop.Arrow α} {f₁' : (P.B a').lastP.M α} (e₁ : MvPFunctor.M.dest P a₁, f₁ = a', TypeVec.splitFun f' f₁') :
                              ∃ (g₁' : P.last.B a'P.last.M) (e₁' : PFunctor.M.dest a₁ = a', g₁'), f' = MvPFunctor.M.pathDestLeft P e₁' f₁ f₁' = fun (x : P.last.B a') => g₁' x, MvPFunctor.M.pathDestRight P e₁' f₁ x
                              theorem MvPFunctor.M.bisim {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M αP.M αProp) (h : ∀ (x y : P.M α), R x y∃ (a : P.A) (f : (P.B a).drop.Arrow (α ::: P.M α).drop) (f₁ : (P.B a).last(α ::: P.M α).last) (f₂ : (P.B a).last(α ::: P.M α).last), MvPFunctor.M.dest P x = a, TypeVec.splitFun f f₁ MvPFunctor.M.dest P y = a, TypeVec.splitFun f f₂ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)) (x : P.M α) (y : P.M α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.bisim₀ {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M αP.M αProp) (h₀ : Equivalence R) (h : ∀ (x y : P.M α), R x yMvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : P.M α) (y : P.M α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.bisim' {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M αP.M αProp) (h : ∀ (x y : P.M α), R x yMvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : P.M α) (y : P.M α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.dest_map {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) (x : P.M α) :
                              theorem MvPFunctor.M.map_dest {n : } (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : (α ::: P.M α).Arrow (β ::: P.M β)) (x : P.M α) (h : ∀ (x : P.M α), TypeVec.lastFun g x = MvFunctor.map (TypeVec.dropFun g) x) :