mathlib documentation

data.qpf.univariate.basic

Quotients of Polynomial Functors

We assume the following:

P : a polynomial functor W : its W-type M : its M-type F : a functor

We define:

q : qpf data, representing F as a quotient of P

The main goal is to construct:

fix : the initial algebra with structure map F fix → fix. cofix : the final coalgebra with structure map cofix → F cofix

We also show that the composition of qpfs is a qpf, and that the quotient of a qpf is a qpf.

The present theory focuses on the univariate case for qpfs

References

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

@[class]

structure qpf (F : Type u → Type u) [functor F] :

Type (u+1)

P : pfunctor
abs : Π {α : Type ?}, (qpf.P F).obj α → F α
repr : Π {α : Type ?}, F α → (qpf.P F).obj α
abs_repr : ∀ {α : Type ?} (x : F α), qpf.abs (qpf.repr x) = x
abs_map : ∀ {α β : Type ?} (f : α → β) (p : (qpf.P F).obj α), qpf.abs (f <$> p) = f <$> qpf.abs p

Quotients of polynomial functors.

Roughly speaking, saying that F is a quotient of a polynomial functor means that for each α, elements of F α are represented by pairs ⟨a, f⟩, where a is the shape of the object and f indexes the relevant elements of α, in a suitably natural manner.

theorem qpf.id_map {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) :

id <$> x = x

theorem qpf.comp_map {F : Type u → Type u} [functor F] [q : qpf F] {α β γ : Type u} (f : α → β) (g : β → γ) (x : F α) :

(g ∘ f) <$> x = g <$> f <$> x

theorem qpf.is_lawful_functor {F : Type u → Type u} [functor F] [q : qpf F] (h : ∀ (α β : Type u), functor.map_const = functor.map ∘ function.const β) :

is_lawful_functor F

theorem qpf.liftp_iff {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (p : α → Prop) (x : F α) :

functor.liftp p x ↔ ∃ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), x = qpf.abs ⟨a, f⟩ ∧ ∀ (i : (qpf.P F).B a), p (f i)

theorem qpf.liftp_iff' {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (p : α → Prop) (x : F α) :

functor.liftp p x ↔ ∃ (u : (qpf.P F).obj α), qpf.abs u = x ∧ ∀ (i : (qpf.P F).B u.fst), p (u.snd i)

theorem qpf.liftr_iff {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (r : α → α → Prop) (x y : F α) :

functor.liftr r x y ↔ ∃ (a : (qpf.P F).A) (f₀ f₁ : (qpf.P F).B a → α), x = qpf.abs ⟨a, f₀⟩ ∧ y = qpf.abs ⟨a, f₁⟩ ∧ ∀ (i : (qpf.P F).B a), r (f₀ i) (f₁ i)

def qpf.recF {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (a : (qpf.P F).W) :

α

does recursion on q.P.W using g : F α → α rather than g : P α → α

Equations

qpf.recF g (W.mk a f) = g (qpf.abs ⟨a, λ (x : (qpf.P F).B a), qpf.recF g (f x)⟩)

theorem qpf.recF_eq {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (x : (qpf.P F).W) :

qpf.recF g x = g (qpf.abs (qpf.recF g <$> x.dest))

theorem qpf.recF_eq' {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (a : (qpf.P F).A) (f : (qpf.P F).B a → (qpf.P F).W) :

qpf.recF g (W.mk a f) = g (qpf.abs (qpf.recF g <$> ⟨a, f⟩))

inductive qpf.Wequiv {F : Type u → Type u} [functor F] [q : qpf F] (a a_1 : (qpf.P F).W) :

Prop

ind : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (a : (qpf.P F).A) (f f' : (qpf.P F).B a → (qpf.P F).W), (∀ (x : (qpf.P F).B a), qpf.Wequiv (f x) (f' x)) → qpf.Wequiv (W.mk a f) (W.mk a f')
abs : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (a : (qpf.P F).A) (f : (qpf.P F).B a → (qpf.P F).W) (a' : (qpf.P F).A) (f' : (qpf.P F).B a' → (qpf.P F).W), qpf.abs ⟨a, f⟩ = qpf.abs ⟨a', f'⟩ → qpf.Wequiv (W.mk a f) (W.mk a' f')
trans : ∀ {F : Type u → Type u} [_inst_1 : functor F] [q : qpf F] (u v w : (qpf.P F).W), qpf.Wequiv u v → qpf.Wequiv v w → qpf.Wequiv u w

two trees are equivalent if their F-abstractions are

theorem qpf.recF_eq_of_Wequiv {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (u : F α → α) (x y : (qpf.P F).W) (a : qpf.Wequiv x y) :

qpf.recF u x = qpf.recF u y

recF is insensitive to the representation

theorem qpf.Wequiv.abs' {F : Type u → Type u} [functor F] [q : qpf F] (x y : (qpf.P F).W) (h : qpf.abs x.dest = qpf.abs y.dest) :

theorem qpf.Wequiv.refl {F : Type u → Type u} [functor F] [q : qpf F] (x : (qpf.P F).W) :

theorem qpf.Wequiv.symm {F : Type u → Type u} [functor F] [q : qpf F] (x y : (qpf.P F).W) (a : qpf.Wequiv x y) :

def qpf.Wrepr {F : Type u → Type u} [functor F] [q : qpf F] (a : (qpf.P F).W) :

maps every element of the W type to a canonical representative

Equations

qpf.Wrepr = qpf.recF (pfunctor.W.mk ∘ qpf.repr)

theorem qpf.Wrepr_equiv {F : Type u → Type u} [functor F] [q : qpf F] (x : (qpf.P F).W) :

qpf.Wequiv (qpf.Wrepr x) x

def qpf.W_setoid {F : Type u → Type u} [functor F] [q : qpf F] :

setoid (qpf.P F).W

Define the fixed point as the quotient of trees under the equivalence relation Wequiv.

Equations

qpf.W_setoid = {r := qpf.Wequiv q, iseqv := _}

@[nolint]

def qpf.fix (F : Type u → Type u) [functor F] [q : qpf F] :

Type u

inductive type defined as initial algebra of a Quotient of Polynomial Functor

Equations

qpf.fix F = quotient qpf.W_setoid

def qpf.fix.rec {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (a : qpf.fix F) :

α

recursor of a type defined by a qpf

Equations

qpf.fix.rec g = quot.lift (qpf.recF g) _

def qpf.fix_to_W {F : Type u → Type u} [functor F] [q : qpf F] (a : qpf.fix F) :

access the underlying W-type of a fixpoint data type

Equations

qpf.fix_to_W = quotient.lift qpf.Wrepr qpf.fix_to_W._proof_1

def qpf.fix.mk {F : Type u → Type u} [functor F] [q : qpf F] (x : F (qpf.fix F)) :

constructor of a type defined by a qpf

Equations

qpf.fix.mk x = quot.mk setoid.r (pfunctor.W.mk (qpf.fix_to_W <$> qpf.repr x))

def qpf.fix.dest {F : Type u → Type u} [functor F] [q : qpf F] (a : qpf.fix F) :

destructor of a type defined by a qpf

Equations

qpf.fix.dest = qpf.fix.rec (functor.map qpf.fix.mk)

theorem qpf.fix.rec_eq {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (x : F (qpf.fix F)) :

qpf.fix.rec g (qpf.fix.mk x) = g (qpf.fix.rec g <$> x)

theorem qpf.fix.ind_aux {F : Type u → Type u} [functor F] [q : qpf F] (a : (qpf.P F).A) (f : (qpf.P F).B a → (qpf.P F).W) :

qpf.fix.mk (qpf.abs ⟨a, λ (x : (qpf.P F).B a), ⟦f x⟧⟩) = ⟦W.mk a f⟧

theorem qpf.fix.ind_rec {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g₁ g₂ : qpf.fix F → α) (h : ∀ (x : F (qpf.fix F)), g₁ <$> x = g₂ <$> x → g₁ (qpf.fix.mk x) = g₂ (qpf.fix.mk x)) (x : qpf.fix F) :

g₁ x = g₂ x

theorem qpf.fix.rec_unique {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (h : qpf.fix F → α) (hyp : ∀ (x : F (qpf.fix F)), h (qpf.fix.mk x) = g (h <$> x)) :

qpf.fix.rec g = h

theorem qpf.fix.mk_dest {F : Type u → Type u} [functor F] [q : qpf F] (x : qpf.fix F) :

qpf.fix.mk x.dest = x

theorem qpf.fix.dest_mk {F : Type u → Type u} [functor F] [q : qpf F] (x : F (qpf.fix F)) :

(qpf.fix.mk x).dest = x

theorem qpf.fix.ind {F : Type u → Type u} [functor F] [q : qpf F] (p : qpf.fix F → Prop) (h : ∀ (x : F (qpf.fix F)), functor.liftp p x → p (qpf.fix.mk x)) (x : qpf.fix F) :

p x

def qpf.corecF {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (a : α) :

does recursion on q.P.M using g : α → F α rather than g : α → P α

Equations

qpf.corecF g = pfunctor.M.corec (λ (x : α), qpf.repr (g x))

theorem qpf.corecF_eq {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (x : α) :

(qpf.corecF g x).dest = qpf.corecF g <$> qpf.repr (g x)

def qpf.is_precongr {F : Type u → Type u} [functor F] [q : qpf F] (r : (qpf.P F).M → (qpf.P F).M → Prop) :

Prop

A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric.

Equations

qpf.is_precongr r = ∀ ⦃x y : (qpf.P F).M⦄, r x y → qpf.abs (quot.mk r <$> x.dest) = qpf.abs (quot.mk r <$> y.dest)

def qpf.Mcongr {F : Type u → Type u} [functor F] [q : qpf F] (a a_1 : (qpf.P F).M) :

Prop

The maximal congruence on q.P.M

Equations

qpf.Mcongr = λ (x y : (qpf.P F).M), ∃ (r : (qpf.P F).M → (qpf.P F).M → Prop), qpf.is_precongr r ∧ r x y

def qpf.cofix (F : Type u → Type u) [functor F] [q : qpf F] :

Type u

coinductive type defined as the final coalgebra of a qpf

Equations

qpf.cofix F = quot qpf.Mcongr

@[instance]

def qpf.inhabited {F : Type u → Type u} [functor F] [q : qpf F] [inhabited (qpf.P F).A] :

inhabited (qpf.cofix F)

Equations

qpf.inhabited = {default := quot.mk qpf.Mcongr (default (qpf.P F).M)}

def qpf.cofix.corec {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (x : α) :

corecursor for type defined by cofix

Equations

qpf.cofix.corec g x = quot.mk qpf.Mcongr (qpf.corecF g x)

def qpf.cofix.dest {F : Type u → Type u} [functor F] [q : qpf F] (a : qpf.cofix F) :

F (qpf.cofix F)

destructor for type defined by cofix

Equations

qpf.cofix.dest = quot.lift (λ (x : (qpf.P F).M), quot.mk qpf.Mcongr <$> qpf.abs x.dest) qpf.cofix.dest._proof_1

theorem qpf.cofix.dest_corec {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (x : α) :

(qpf.cofix.corec g x).dest = qpf.cofix.corec g <$> g x

theorem qpf.cofix.bisim_rel {F : Type u → Type u} [functor F] [q : qpf F] (r : qpf.cofix F → qpf.cofix F → Prop) (h : ∀ (x y : qpf.cofix F), r x y → quot.mk r <$> x.dest = quot.mk r <$> y.dest) (x y : qpf.cofix F) (a : r x y) :

x = y

theorem qpf.cofix.bisim {F : Type u → Type u} [functor F] [q : qpf F] (r : qpf.cofix F → qpf.cofix F → Prop) (h : ∀ (x y : qpf.cofix F), r x y → functor.liftr r x.dest y.dest) (x y : qpf.cofix F) (a : r x y) :

x = y

theorem qpf.cofix.bisim' {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u_1} (Q : α → Prop) (u v : α → qpf.cofix F) (h : ∀ (x : α), Q x → (∃ (a : (qpf.P F).A) (f f' : (qpf.P F).B a → qpf.cofix F), (u x).dest = qpf.abs ⟨a, f⟩ ∧ (v x).dest = qpf.abs ⟨a, f'⟩ ∧ ∀ (i : (qpf.P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x')) (x : α) (a : Q x) :

u x = v x

def qpf.comp {F₂ : Type u → Type u} [functor F₂] [q₂ : qpf F₂] {F₁ : Type u → Type u} [functor F₁] [q₁ : qpf F₁] :

qpf (functor.comp F₂ F₁)

composition of qpfs gives another qpf

Equations

qpf.comp = {P := (qpf.P F₂).comp (qpf.P F₁), abs := λ (α : Type u), id (λ (p : ((qpf.P F₂).comp (qpf.P F₁)).obj α), qpf.abs ⟨p.fst.fst, λ (x : (qpf.P F₂).B p.fst.fst), qpf.abs ⟨p.fst.snd x, λ (y : (qpf.P F₁).B (p.fst.snd x)), p.snd ⟨x, y⟩⟩⟩), repr := λ (α : Type u), id (λ (y : F₂ (F₁ α)), ⟨⟨(qpf.repr y).fst, λ (u : (qpf.P F₂).B (qpf.repr y).fst), (qpf.repr ((qpf.repr y).snd u)).fst⟩, id (λ (x : Σ (u : (qpf.P F₂).B (qpf.repr y).fst), (qpf.P F₁).B (qpf.repr ((qpf.repr y).snd u)).fst), (qpf.repr ((qpf.repr y).snd x.fst)).snd x.snd)⟩), abs_repr := _, abs_map := _}

def qpf.quotient_qpf {F : Type u → Type u} [functor F] [q : qpf F] {G : Type u → Type u} [functor G] {FG_abs : Π {α : Type u}, F α → G α} {FG_repr : Π {α : Type u}, G α → F α} (FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x) :

Given a qpf F and a well-behaved surjection FG_abs from F α to functor G α, G is a qpf. We can consider G a quotient on F where elements x y : F α are in the same equivalence class if FG_abs x = FG_abs y

Equations

qpf.quotient_qpf FG_abs_repr FG_abs_map = {P := qpf.P F q, abs := λ {α : Type u} (p : (qpf.P F).obj α), FG_abs (qpf.abs p), repr := λ {α : Type u} (x : G α), qpf.repr (FG_repr x), abs_repr := _, abs_map := _}

theorem qpf.mem_supp {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) (u : α) :

u ∈ functor.supp x ↔ ∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs ⟨a, f⟩ = x → u ∈ f '' set.univ

theorem qpf.supp_eq {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) :

functor.supp x = {u : α | ∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs ⟨a, f⟩ = x → u ∈ f '' set.univ}

theorem qpf.has_good_supp_iff {F : Type u → Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) :

(∀ (p : α → Prop), functor.liftp p x ↔ ∀ (u : α), u ∈ functor.supp x → p u) ↔ ∃ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs ⟨a, f⟩ = x ∧ ∀ (a' : (qpf.P F).A) (f' : (qpf.P F).B a' → α), qpf.abs ⟨a', f'⟩ = x → f '' set.univ ⊆ f' '' set.univ

def qpf.is_uniform {F : Type u → Type u} [functor F] (q : qpf F) :

Prop

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

Equations

q.is_uniform = ∀ ⦃α : Type u⦄ (a a' : (qpf.P F).A) (f : (qpf.P F).B a → α) (f' : (qpf.P F).B a' → α), qpf.abs ⟨a, f⟩ = qpf.abs ⟨a', f'⟩ → f '' set.univ = f' '' set.univ

def qpf.liftp_preservation {F : Type u → Type u} [functor F] (q : qpf F) :

Prop

does abs preserve liftp?

Equations

q.liftp_preservation = ∀ ⦃α : Type u⦄ (p : α → Prop) (x : (qpf.P F).obj α), functor.liftp p (qpf.abs x) ↔ functor.liftp p x

def qpf.supp_preservation {F : Type u → Type u} [functor F] (q : qpf F) :

Prop

does abs preserve supp?

Equations

q.supp_preservation = ∀ ⦃α : Type u⦄ (x : (qpf.P F).obj α), functor.supp (qpf.abs x) = functor.supp x

theorem qpf.supp_eq_of_is_uniform {F : Type u → Type u} [functor F] [q : qpf F] (h : q.is_uniform) {α : Type u} (a : (qpf.P F).A) (f : (qpf.P F).B a → α) :

functor.supp (qpf.abs ⟨a, f⟩) = f '' set.univ

theorem qpf.liftp_iff_of_is_uniform {F : Type u → Type u} [functor F] [q : qpf F] (h : q.is_uniform) {α : Type u} (x : F α) (p : α → Prop) :

functor.liftp p x ↔ ∀ (u : α), u ∈ functor.supp x → p u

theorem qpf.supp_map {F : Type u → Type u} [functor F] [q : qpf F] (h : q.is_uniform) {α β : Type u} (g : α → β) (x : F α) :

functor.supp (g <$> x) = g '' functor.supp x

theorem qpf.supp_preservation_iff_uniform {F : Type u → Type u} [functor F] [q : qpf F] :

q.supp_preservation ↔ q.is_uniform

theorem qpf.supp_preservation_iff_liftp_preservation {F : Type u → Type u} [functor F] [q : qpf F] :

q.supp_preservation ↔ q.liftp_preservation

theorem qpf.liftp_preservation_iff_uniform {F : Type u → Type u} [functor F] [q : qpf F] :

q.liftp_preservation ↔ q.is_uniform