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]

source
class MvQPF {n : ℕ} (F : TypeVec.{u} n → Type u_1) extends MvFunctor F :
Type (max (u + 1) u_1)

Multivariate quotients of polynomial functors.

Instances

    Show that every MvQPF is a lawful MvFunctor. #

    source
    theorem MvQPF.id_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) :
    MvFunctor.map TypeVec.id x = x
    source
    @[simp]
    theorem MvQPF.comp_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : F α) :
    MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)
    source
    @[instance 100]
    instance MvQPF.lawfulMvFunctor {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
    LawfulMvFunctor F
    Equations
    • ⋯ = ⋯
    source
    theorem MvQPF.liftP_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : F α) :
    MvFunctor.LiftP p x ↔ ∃ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), x = MvQPF.abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), p (f i j)
    source
    theorem MvQPF.liftR_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (r : {i : Fin2 n} → α i → α i → Prop) (x y : F α) :
    MvFunctor.LiftR (fun {i : Fin2 n} => r) x y ↔ ∃ (a : (MvQPF.P F).A) (f₀ : ((MvQPF.P F).B a).Arrow α) (f₁ : ((MvQPF.P F).B a).Arrow α), x = MvQPF.abs ⟨a, f₀⟩ ∧ y = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), r (f₀ i j) (f₁ i j)
    source
    theorem MvQPF.mem_supp {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) (i : Fin2 n) (u : α i) :
    u ∈ MvFunctor.supp x i ↔ ∀ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ
    source
    theorem MvQPF.supp_eq {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} {i : Fin2 n} (x : F α) :
    MvFunctor.supp x i = {u : α i | ∀ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ}
    source
    theorem MvQPF.has_good_supp_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) :
    (∀ (p : (i : Fin2 n) → α i → Prop), MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u) ↔ ∃ (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α), MvQPF.abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (MvQPF.P F).A) (f' : ((MvQPF.P F).B a').Arrow α), MvQPF.abs ⟨a', f'⟩ = x → f i '' Set.univ ⊆ f' i '' Set.univ
    source
    def MvQPF.IsUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
    Prop

    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
      source
      def MvQPF.LiftPPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
      Prop

      does abs preserve liftp?

      Equations
      Instances For
        source
        def MvQPF.SuppPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
        Prop

        does abs preserve supp?

        Equations
        Instances For
          source
          theorem MvQPF.supp_eq_of_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f : ((MvQPF.P F).B a).Arrow α) (i : Fin2 n) :
          MvFunctor.supp (MvQPF.abs ⟨a, f⟩) i = f i '' Set.univ
          source
          theorem MvQPF.liftP_iff_of_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (x : F α) (p : (i : Fin2 n) → α i → Prop) :
          MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u
          source
          theorem MvQPF.supp_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] (h : MvQPF.IsUniform) {α β : TypeVec.{u} n} (g : α.Arrow β) (x : F α) (i : Fin2 n) :
          MvFunctor.supp (MvFunctor.map g x) i = g i '' MvFunctor.supp x i
          source
          theorem MvQPF.suppPreservation_iff_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
          MvQPF.SuppPreservation ↔ MvQPF.IsUniform
          source
          theorem MvQPF.suppPreservation_iff_liftpPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
          MvQPF.SuppPreservation ↔ MvQPF.LiftPPreservation
          source
          theorem MvQPF.liftpPreservation_iff_uniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] :
          MvQPF.LiftPPreservation ↔ MvQPF.IsUniform
          source
          def MvQPF.ofEquiv {n : ℕ} {F : TypeVec.{u} n → Type u_2} {F' : TypeVec.{u} n → Type u_3} [q : MvQPF F'] [MvFunctor F] (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) (map_eq : ∀ (α β : TypeVec.{u} n) (f : α.Arrow β) (a : F α), MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a)) := by intros; rfl) :
          MvQPF F

          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
            source
            instance MvPFunctor.instMvQPFObj {n : ℕ} (P : MvPFunctor.{u_1} n) :
            MvQPF ↑P

            Every polynomial functor is a (trivial) QPF

            Equations