Documentation

Mathlib.Data.QPF.Multivariate.Basic

Multivariate quotients of polynomial functors. #

Basic definition of multivariate QPF. QPFs form a compositional framework for defining inductive and coinductive types, their quotients and nesting.

The idea is based on building ever larger functors. For instance, we can define a list using a shape functor:

inductive ListShape (a b : Type)
  | nil : ListShape
  | cons : a -> b -> ListShape

This shape can itself be decomposed as a sum of product which are themselves QPFs. It follows that the shape is a QPF and we can take its fixed point and create the list itself:

def List (a : Type) := fix ListShape a -- not the actual notation

We can continue and define the quotient on permutation of lists and create the multiset type:

def Multiset (a : Type) := QPF.quot List.perm List a -- not the actual notion

And Multiset is also a QPF. We can then create a novel data type (for Lean):

inductive Tree (a : Type)
  | node : a -> Multiset Tree -> Tree

An unordered tree. This is currently not supported by Lean because it nests an inductive type inside of a quotient. We can go further and define unordered, possibly infinite trees:

coinductive Tree' (a : Type)
| node : a -> Multiset Tree' -> Tree'

by using the cofix construct. Those options can all be mixed and matched because they preserve the properties of QPF. The latter example, Tree', combines fixed point, co-fixed point and quotients.

each proves that some operations on functors preserves the QPF structure

Reference #

! * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]

class MvQPF {n : } (F : TypeVec.{u} nType u_1) [MvFunctor F] :
Type (max (u + 1) u_1)

Multivariate quotients of polynomial functors.

Instances

    Show that every MvQPF is a lawful MvFunctor. #

    theorem MvQPF.id_map {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) :
    MvFunctor.map TypeVec.id x = x
    @[simp]
    theorem MvQPF.comp_map {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} {γ : TypeVec.{u} n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow β γ) (x : F α) :
    instance MvQPF.lawfulMvFunctor {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :
    Equations
    theorem MvQPF.liftP_iff {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (p : i : Fin2 n⦄ → α iProp) (x : F α) :
    MvFunctor.LiftP p x ∃ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), x = MvQPF.abs { fst := a, snd := f } ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), p (f i j)
    theorem MvQPF.liftR_iff {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (r : {i : Fin2 n} → α iα iProp) (x : F α) (y : F α) :
    MvFunctor.LiftR (fun {i : Fin2 n} => r) x y ∃ (a : (MvQPF.P F).A) (f₀ : TypeVec.Arrow ((MvQPF.P F).B a) α) (f₁ : TypeVec.Arrow ((MvQPF.P F).B a) α), x = MvQPF.abs { fst := a, snd := f₀ } y = MvQPF.abs { fst := a, snd := f₁ } ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), r (f₀ i j) (f₁ i j)
    theorem MvQPF.mem_supp {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) (i : Fin2 n) (u : α i) :
    u MvFunctor.supp x i ∀ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = xu f i '' Set.univ
    theorem MvQPF.supp_eq {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {i : Fin2 n} (x : F α) :
    MvFunctor.supp x i = {u : α i | ∀ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = xu f i '' Set.univ}
    theorem MvQPF.has_good_supp_iff {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) :
    (∀ (p : (i : Fin2 n) → α iProp), MvFunctor.LiftP p x ∀ (i : Fin2 n), uMvFunctor.supp x i, p i u) ∃ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = x ∀ (i : Fin2 n) (a' : (MvQPF.P F).A) (f' : TypeVec.Arrow ((MvQPF.P F).B a') α), MvQPF.abs { fst := a', snd := f' } = xf i '' Set.univ f' i '' Set.univ
    def MvQPF.IsUniform {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :

    A qpf is said to be uniform if every polynomial functor representing a single value all have the same range.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def MvQPF.LiftPPreservation {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :

      does abs preserve liftp?

      Equations
      Instances For
        def MvQPF.SuppPreservation {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :

        does abs preserve supp?

        Equations
        Instances For
          theorem MvQPF.supp_eq_of_isUniform {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α) (i : Fin2 n) :
          MvFunctor.supp (MvQPF.abs { fst := a, snd := f }) i = f i '' Set.univ
          theorem MvQPF.liftP_iff_of_isUniform {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (x : F α) (p : (i : Fin2 n) → α iProp) :
          MvFunctor.LiftP p x ∀ (i : Fin2 n), uMvFunctor.supp x i, p i u
          theorem MvQPF.supp_map {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) (x : F α) (i : Fin2 n) :
          theorem MvQPF.suppPreservation_iff_isUniform {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :
          MvQPF.SuppPreservation MvQPF.IsUniform
          theorem MvQPF.suppPreservation_iff_liftpPreservation {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :
          MvQPF.SuppPreservation MvQPF.LiftPPreservation
          theorem MvQPF.liftpPreservation_iff_uniform {n : } {F : TypeVec.{u} nType u_1} [MvFunctor F] [q : MvQPF F] :
          MvQPF.LiftPPreservation MvQPF.IsUniform
          def MvQPF.ofEquiv {n : } {F : TypeVec.{u} nType u_2} {F' : TypeVec.{u} nType u_3} [MvFunctor F'] [q : MvQPF F'] [MvFunctor F] (eqv : (α : TypeVec.{u} n) → F α F' α) (map_eq : autoParam (∀ (α β : TypeVec.{u} n) (f : TypeVec.Arrow α β) (a : F α), MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a))) _auto✝) :

          Any type function F that is (extensionally) equivalent to a QPF, is itself a QPF, assuming that the functorial map of F behaves similar to MvFunctor.ofEquiv eqv

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance MvPFunctor.instMvQPFObj {n : } (P : MvPFunctor.{u_1} n) :
            MvQPF P

            Every polynomial functor is a (trivial) QPF

            Equations
            • One or more equations did not get rendered due to their size.