The W construction as a multivariate polynomial functor. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

W types are well-founded tree-like structures. They are defined as the least fixpoint of a polynomial functor.

Main definitions #

W_mk - constructor
`W_dest - destructor
W_rec - recursor: basis for defining functions by structural recursion on P.W α
W_rec_eq - defining equation for W_rec
W_ind - induction principle for P.W α

Implementation notes #

Three views of M-types:

Wp: polynomial functor
W: data type inductively defined by a triple: shape of the root, data in the root and children of the root
W: least fixed point of a polynomial functor

Specifically, we define the polynomial functor Wp as:

A := a tree-like structure without information in the nodes
B := given the tree-like structure t, B t is a valid path (specified inductively by W_path) from the root of t to any given node.

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

Reference #

Jeremy Avigad, Mario M. Carneiro and Simon Hudon. Data Types as Quotients of Polynomial Functors

source

inductive mvpfunctor.W_path {n : ℕ} (P : mvpfunctor (n + 1)) :

P.last.W → fin2 n → Type u

root : Π {n : ℕ} {P : mvpfunctor (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : fin2 n), P.drop.B a i → P.W_path (W_type.mk a f) i
child : Π {n : ℕ} {P : mvpfunctor (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : fin2 n) (j : P.last.B a), P.W_path (f j) i → P.W_path (W_type.mk a f) i

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

Instances for mvpfunctor.W_path

mvpfunctor.W_path.has_sizeof_inst
mvpfunctor.W_path.inhabited

source

@[protected, instance]

def mvpfunctor.W_path.inhabited {n : ℕ} (P : mvpfunctor (n + 1)) (x : P.last.W) {i : fin2 n} [I : inhabited (P.drop.B x.head i)] :

inhabited (P.W_path x i)

Equations

mvpfunctor.W_path.inhabited P x = {default := mvpfunctor.W_path.inhabited._match_1 P x I}
mvpfunctor.W_path.inhabited._match_1 P (W_type.mk a f) I = mvpfunctor.W_path.root a f i inhabited.default

source

def mvpfunctor.W_path_cases_on {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

typevec.arrow (P.W_path (W_type.mk a f)) α

Specialized destructor on W_path

Equations

P.W_path_cases_on g' g = id (λ (i : fin2 n) (x : P.W_path (W_type.mk a f) i), x.cases_on (λ (x_a : P.A) (x_f : P.last.B x_a → P.last.W) (x_i : fin2 n) (x_c : P.drop.B x_a x_i) (H_1 : W_type.mk a f = W_type.mk x_a x_f), W_type.no_confusion H_1 (λ (a_eq : a = x_a), eq.rec (λ (x_f : P.last.B a → P.last.W) (x_c : P.drop.B a x_i) (f_eq : f == x_f), eq.rec (λ (H_2 : i = x_i), eq.rec (λ (x_c : P.drop.B a i) (H_3 : x == mvpfunctor.W_path.root a f i x_c), eq.rec ((λ (f : P.last.B a → P.last.W) (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) (i : fin2 n) (c : P.drop.B a i), g' i c) f g' g i x_c) _) H_2 x_c) _) a_eq x_f x_c)) (λ (x_a : P.A) (x_f : P.last.B x_a → P.last.W) (x_i : fin2 n) (x_j : P.last.B x_a) (x_c : P.W_path (x_f x_j) x_i) (H_1 : W_type.mk a f = W_type.mk x_a x_f), W_type.no_confusion H_1 (λ (a_eq : a = x_a), eq.rec (λ (x_f : P.last.B a → P.last.W) (x_j : P.last.B a) (x_c : P.W_path (x_f x_j) x_i) (f_eq : f == x_f), eq.rec (λ (x_c : P.W_path (f x_j) x_i) (H_2 : i = x_i), eq.rec (λ (x_c : P.W_path (f x_j) i) (H_3 : x == mvpfunctor.W_path.child a f i x_j x_c), eq.rec ((λ (f : P.last.B a → P.last.W) (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) (i : fin2 n) (j : P.last.B a) (c : P.W_path (f j) i), g j i c) f g' g i x_j x_c) _) H_2 x_c) _ x_c) a_eq x_f x_j x_c)) _ _ _)

source

def mvpfunctor.W_path_dest_left {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (h : typevec.arrow (P.W_path (W_type.mk a f)) α) :

(P.drop.B a).arrow α

Specialized destructor on W_path

Equations

P.W_path_dest_left h = λ (i : fin2 n) (c : P.drop.B a i), h i (mvpfunctor.W_path.root a f i c)

source

def mvpfunctor.W_path_dest_right {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (h : typevec.arrow (P.W_path (W_type.mk a f)) α) (j : P.last.B a) :

typevec.arrow (P.W_path (f j)) α

Specialized destructor on W_path

Equations

P.W_path_dest_right h = λ (j : P.last.B a) (i : fin2 n) (c : P.W_path (f j) i), h i (mvpfunctor.W_path.child a f i j c)

source

theorem mvpfunctor.W_path_dest_left_W_path_cases_on {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

P.W_path_dest_left (P.W_path_cases_on g' g) = g'

source

theorem mvpfunctor.W_path_dest_right_W_path_cases_on {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

P.W_path_dest_right (P.W_path_cases_on g' g) = g

source

theorem mvpfunctor.W_path_cases_on_eta {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {a : P.A} {f : P.last.B a → P.last.W} (h : typevec.arrow (P.W_path (W_type.mk a f)) α) :

P.W_path_cases_on (P.W_path_dest_left h) (P.W_path_dest_right h) = h

source

theorem mvpfunctor.comp_W_path_cases_on {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {β : typevec n} (h : α.arrow β) {a : P.A} {f : P.last.B a → P.last.W} (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

typevec.comp h (P.W_path_cases_on g' g) = P.W_path_cases_on (typevec.comp h g') (λ (i : P.last.B a), typevec.comp h (g i))

source

def mvpfunctor.Wp {n : ℕ} (P : mvpfunctor (n + 1)) :

mvpfunctor n

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.W_path}

source

@[nolint]

def mvpfunctor.W {n : ℕ} (P : mvpfunctor (n + 1)) (α : typevec n) :

Type u

W-type of P

Equations

P.W α = P.Wp.obj α

Instances for mvpfunctor.W

mvpfunctor.mvfunctor_W

source

@[protected, instance]

def mvpfunctor.mvfunctor_W {n : ℕ} (P : mvpfunctor (n + 1)) :

mvfunctor P.W

Equations

P.mvfunctor_W = id (mvpfunctor.obj.mvfunctor P.Wp)

First, describe operations on W as a polynomial functor.

source

def mvpfunctor.Wp_mk {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f : P.last.B a → P.last.W) (f' : typevec.arrow (P.W_path (W_type.mk a f)) α) :

P.W α

Constructor for Wp

Equations

P.Wp_mk a f f' = ⟨W_type.mk a f, f'⟩

source

def mvpfunctor.Wp_rec {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_2} (g : Π (a : P.A) (f : P.last.B a → P.last.W), typevec.arrow (P.W_path (W_type.mk a f)) α → (P.last.B a → C) → C) (x : P.last.W) (f' : typevec.arrow (P.W_path x) α) :

Recursor for Wp

Equations

P.Wp_rec g (W_type.mk a f) f' = g a f f' (λ (i : P.last.B a), P.Wp_rec g (f i) (P.W_path_dest_right f' i))

source

theorem mvpfunctor.Wp_rec_eq {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_2} (g : Π (a : P.A) (f : P.last.B a → P.last.W), typevec.arrow (P.W_path (W_type.mk a f)) α → (P.last.B a → C) → C) (a : P.A) (f : P.last.B a → P.last.W) (f' : typevec.arrow (P.W_path (W_type.mk a f)) α) :

P.Wp_rec g (W_type.mk a f) f' = g a f f' (λ (i : P.last.B a), P.Wp_rec g (f i) (P.W_path_dest_right f' i))

source

theorem mvpfunctor.Wp_ind {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : Π (x : P.last.W), typevec.arrow (P.W_path x) α → Prop} (ih : ∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : typevec.arrow (P.W_path (W_type.mk a f)) α), (∀ (i : P.last.B a), C (f i) (P.W_path_dest_right f' i)) → C (W_type.mk a f) f') (x : P.last.W) (f' : typevec.arrow (P.W_path x) α) :

C x f'

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

a : P.A is the shape of the top node
f' : P.drop.B a ⟹ α is the contents of the top node
f : P.last.B a → P.last.W are the subtrees

source

def mvpfunctor.W_mk {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) :

P.W α

Constructor for W

Equations

P.W_mk a f' f = let g : P.last.B a → P.last.W := λ (i : P.last.B a), (f i).fst, g' : typevec.arrow (P.W_path (W_type.mk a g)) α := P.W_path_cases_on f' (λ (i : P.last.B a), (f i).snd) in ⟨W_type.mk a g, g'⟩

source

def mvpfunctor.W_rec {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_1} (g : Π (a : P.A), (P.drop.B a).arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C) :

P.W α → C

Recursor for W

Equations

P.W_rec g ⟨a, f'⟩ = let g' : Π (a : P.A) (f : P.last.B a → P.last.W), typevec.arrow (P.W_path (W_type.mk a f)) α → (P.last.B a → C) → C := λ (a : P.A) (f : P.last.B a → P.last.W) (h : typevec.arrow (P.W_path (W_type.mk a f)) α) (h' : P.last.B a → C), g a (P.W_path_dest_left h) (λ (i : P.last.B a), ⟨f i, P.W_path_dest_right h i⟩) h' in P.Wp_rec g' a f'

source

theorem mvpfunctor.W_rec_eq {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : Type u_1} (g : Π (a : P.A), (P.drop.B a).arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) :

P.W_rec g (P.W_mk a f' f) = g a f' f (λ (i : P.last.B a), P.W_rec g (f i))

Defining equation for the recursor of W

source

theorem mvpfunctor.W_ind {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : P.W α → Prop} (ih : ∀ (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.W_mk a f' f)) (x : P.W α) :

C x

Induction principle for W

source

theorem mvpfunctor.W_cases {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {C : P.W α → Prop} (ih : ∀ (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α), C (P.W_mk a f' f)) (x : P.W α) :

C x

source

def mvpfunctor.W_map {n : ℕ} (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) :

P.W α → P.W β

W-types are functorial

Equations

P.W_map g = λ (x : P.W α), mvfunctor.map g x

source

theorem mvpfunctor.W_mk_eq {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f : P.last.B a → P.last.W) (g' : (P.drop.B a).arrow α) (g : Π (j : P.last.B a), typevec.arrow (P.W_path (f j)) α) :

P.W_mk a g' (λ (i : P.last.B a), ⟨f i, g i⟩) = ⟨W_type.mk a f, P.W_path_cases_on g' g⟩

source

theorem mvpfunctor.W_map_W_mk {n : ℕ} (P : mvpfunctor (n + 1)) {α β : typevec n} (g : α.arrow β) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) :

mvfunctor.map g (P.W_mk a f' f) = P.W_mk a (typevec.comp g f') (λ (i : P.last.B a), mvfunctor.map g (f i))

source

@[reducible]

def mvpfunctor.obj_append1 {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u} (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → β) :

P.obj (α ::: β)

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

Equations

P.obj_append1 a f' f = ⟨a, typevec.split_fun f' f⟩

source

theorem mvpfunctor.map_obj_append1 {n : ℕ} (P : mvpfunctor (n + 1)) {α γ : typevec n} (g : α.arrow γ) (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) :

mvfunctor.map (g ::: P.W_map g) (P.obj_append1 a f' f) = P.obj_append1 a (typevec.comp g f') (λ (x : P.last.B a), P.W_map 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.

source

def mvpfunctor.W_mk' {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} :

P.obj (α ::: P.W α) → P.W α

Constructor for the W-type of P

Equations

P.W_mk' ⟨a, f⟩ = P.W_mk a (typevec.drop_fun f) (typevec.last_fun f)

source

def mvpfunctor.W_dest' {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} :

P.W α → P.obj (α ::: P.W α)

Destructor for the W-type of P

Equations

P.W_dest' = P.W_rec (λ (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) (_x : P.last.B a → P.obj (α ::: P.W α)), ⟨a, typevec.split_fun f' f⟩)

source

theorem mvpfunctor.W_dest'_W_mk {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} (a : P.A) (f' : (P.drop.B a).arrow α) (f : P.last.B a → P.W α) :

P.W_dest' (P.W_mk a f' f) = ⟨a, typevec.split_fun f' f⟩

source

theorem mvpfunctor.W_dest'_W_mk' {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec n} (x : P.obj (α ::: P.W α)) :

P.W_dest' (P.W_mk' x) = x