feat(data/multivariate/qpf): definition (#3395)

Part of #3317

src/control/functor/multivariate.lean

@@ -49,7 +49,7 @@ def liftr {α : typevec n} (r : Π {i}, α i → α i → Prop) (x y : F α) : P
 /-- given `x : F α` and a projection `i` of type vector `α`, `supp x i` is the set
 of `α.i` contained in `x` -/
 def supp {α : typevec n} (x : F α) (i : fin2 n) : set (α i) :=
-{ y : α i | ∀ {p}, liftp p x → p i y }
+{ y : α i | ∀ ⦃p⦄, liftp p x → p i y }
 
 theorem of_mem_supp {α : typevec n} {x : F α} {p : Π ⦃i⦄, α i → Prop} (h : liftp p x) (i : fin2 n):
   ∀ y ∈ supp x i, p y :=

src/data/pfunctor/multivariate/basic.lean

@@ -0,0 +1,208 @@
+/-
+Copyright (c) 2018 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+-/
+import control.functor.multivariate
+import data.pfunctor.univariate
+import data.sigma
+
+/-!
+# Multivariate polynomial functors.
+
+Multivariate polynomial functors are used for defining M-types and W-types. 
+They map a type vector `α` to the type `Σ a : A, B a ⟹ α`, with `A : Type` and
+`B : A → typevec n`. They interact well with Lean's inductive definitions because
+they guarantee that occurrences of `α` are positive.
+-/
+
+universes u v
+open_locale mvfunctor
+
+/--
+multivariate polynomial functors
+-/
+structure mvpfunctor (n : ℕ) :=
+(A : Type.{u}) (B : A → typevec.{u} n)
+
+namespace mvpfunctor
+open mvfunctor (liftp liftr)
+
+variables {n m : ℕ} (P : mvpfunctor.{u} n)
+
+/-- Applying `P` to an object of `Type` -/
+def obj (α : typevec.{u} n) : Type u := Σ a : P.A, P.B a ⟹ α
+
+/-- Applying `P` to a morphism of `Type` -/
+def map {α β : typevec n} (f : α ⟹ β) : P.obj α → P.obj β :=
+λ ⟨a, g⟩, ⟨a, typevec.comp f g⟩
+
+instance : inhabited (mvpfunctor n) :=
+⟨ ⟨default _, λ _, default _⟩ ⟩
+
+instance obj.inhabited {α : typevec n} [inhabited P.A] [Π i, inhabited (α i)] :
+  inhabited (P.obj α) :=
+⟨ ⟨default _, λ _ _, default _⟩ ⟩
+
+instance : mvfunctor P.obj :=
+⟨@mvpfunctor.map n P⟩
+
+theorem map_eq {α β : typevec n} (g : α ⟹ β) (a : P.A) (f : P.B a ⟹ α) :
+  @mvfunctor.map _ P.obj _ _ _ g ⟨a, f⟩ = ⟨a, g ⊚ f⟩ :=
+rfl
+
+theorem id_map {α : typevec n} : ∀ x : P.obj α, typevec.id <$$> x = x
+| ⟨a, g⟩ := rfl
+
+theorem comp_map {α β γ : typevec n} (f : α ⟹ β) (g : β ⟹ γ) :
+  ∀ x : P.obj α, (g ⊚ f) <$$> x = g <$$> (f <$$> x)
+| ⟨a, h⟩ := rfl
+
+/-- Constant functor where the input object does not affect the output -/
+def const (n : ℕ) (A : Type u) : mvpfunctor n :=
+{ A := A, B := λ a i, pempty }
+
+section const
+variables (n) {A : Type u}  {α β : typevec.{u} n}
+
+/-- Constructor for the constant functor -/
+def const.mk (x : A) {α} : (const n A).obj α :=
+⟨ x, λ i a, pempty.elim a ⟩
+
+variables {n A}
+
+/-- Destructor for the constant functor -/
+def const.get (x : (const n A).obj α) : A :=
+x.1
+
+@[simp]
+lemma const.get_map (f : α ⟹ β) (x : (const n A).obj α) :
+  const.get (f <$$> x) = const.get x :=
+by cases x; refl
+
+@[simp]
+lemma const.get_mk (x : A) : const.get (const.mk n x : (const n A).obj α) = x :=
+by refl
+
+@[simp]
+lemma const.mk_get (x : (const n A).obj α) : const.mk n (const.get x) = x :=
+by cases x; dsimp [const.get,const.mk]; congr; ext _ ⟨ ⟩
+
+end const
+
+/-- Functor composition on polynomial functors -/
+def comp (P : mvpfunctor.{u} n) (Q : fin2 n → mvpfunctor.{u} m) : mvpfunctor m :=
+{ A := Σ a₂ : P.1, Π i, P.2 a₂ i → (Q i).1,
+  B := λ a, λ i, Σ j (b : P.2 a.1 j), (Q j).2 (a.snd j b) i }
+
+variables {P} {Q : fin2 n → mvpfunctor.{u} m} {α β : typevec.{u} m}
+
+/-- Constructor for functor composition -/
+def comp.mk (x : P.obj (λ i, (Q i).obj α)) : (comp P Q).obj α :=
+⟨ ⟨ x.1, λ i a, (x.2 _ a).1  ⟩, λ i a, (x.snd a.fst (a.snd).fst).snd i (a.snd).snd ⟩
+
+/-- Destructor for functor composition -/
+def comp.get (x : (comp P Q).obj α) : P.obj (λ i, (Q i).obj α) :=
+⟨ x.1.1, λ i a, ⟨x.fst.snd i a, λ (j : fin2 m) (b : (Q i).B _ j), x.snd j ⟨i, ⟨a, b⟩⟩⟩ ⟩
+
+lemma comp.get_map (f : α ⟹ β) (x : (comp P Q).obj α) :
+  comp.get (f <$$> x) = (λ i (x : (Q i).obj α), f <$$> x) <$$> comp.get x :=
+by cases x; refl
+
+@[simp]
+lemma comp.get_mk (x : P.obj (λ i, (Q i).obj α)) : comp.get (comp.mk x) = x :=
+begin
+  cases x,
+  simp! [comp.get,comp.mk],
+end
+
+@[simp]
+lemma comp.mk_get (x : (comp P Q).obj α) : comp.mk (comp.get x) = x :=
+begin
+  cases x,
+  dsimp [comp.get,comp.mk],
+  ext; intros, refl, refl,
+  congr, ext; intros; refl,
+  ext, congr, rcases x_1 with ⟨a,b,c⟩; refl,
+end
+
+/-
+lifting predicates and relations
+-/
+
+theorem liftp_iff {α : typevec n} (p : Π ⦃i⦄ , α i → Prop) (x : P.obj α) :
+  liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ i j, p (f i j) :=
+begin
+  split,
+  { rintros ⟨y, hy⟩, cases h : y with a f,
+    refine ⟨a, λ i j, (f i j).val, _, λ i j, (f i j).property⟩,
+    rw [←hy, h, map_eq], refl },
+  rintros ⟨a, f, xeq, pf⟩,
+  use ⟨a, λ i j, ⟨f i j, pf i j⟩⟩,
+  rw [xeq], reflexivity
+end
+
+theorem liftp_iff' {α : typevec n} (p : Π ⦃i⦄ , α i → Prop) (a : P.A) (f : P.B a ⟹ α) :
+  @liftp.{u} _ P.obj _ α p ⟨a,f⟩ ↔ ∀ i x, p (f i x) :=
+begin
+  simp only [liftp_iff, sigma.mk.inj_iff]; split; intro,
+  { casesm* [Exists _, _ ∧ _], subst_vars, assumption },
+  repeat { constructor <|> assumption }
+end
+
+theorem liftr_iff {α : typevec n} (r : Π ⦃i⦄, α i → α i → Prop) (x y : P.obj α) :
+  liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ i j, r (f₀ i j) (f₁ i j) :=
+begin
+  split,
+  { rintros ⟨u, xeq, yeq⟩, cases h : u with a f,
+    use [a, λ i j, (f i j).val.fst, λ i j, (f i j).val.snd],
+    split, { rw [←xeq, h], refl },
+    split, { rw [←yeq, h], refl },
+    intros i j, exact (f i j).property },
+  rintros ⟨a, f₀, f₁, xeq, yeq, h⟩,
+  use ⟨a, λ i j, ⟨(f₀ i j, f₁ i j), h i j⟩⟩,
+  dsimp, split,
+  { rw [xeq], refl },
+  rw [yeq], refl
+end
+
+open set mvfunctor
+
+theorem supp_eq {α : typevec n} (a : P.A) (f : P.B a ⟹ α) (i) :
+  @supp.{u} _ P.obj _ α  (⟨a,f⟩ : P.obj α) i = f i '' univ :=
+begin
+  ext, simp only [supp, image_univ, mem_range, mem_set_of_eq],
+  split; intro h,
+  { apply @h (λ i x, ∃ (y : P.B a i), f i y = x),
+    rw liftp_iff', intros, refine ⟨_,rfl⟩ },
+  { simp only [liftp_iff'], cases h, subst x,
+    tauto }
+end
+
+end mvpfunctor
+
+/-
+Decomposing an n+1-ary pfunctor.
+-/
+
+namespace mvpfunctor
+open typevec
+variables {n : ℕ} (P : mvpfunctor.{u} (n+1))
+
+/-- Split polynomial functor, get a n-ary functor
+from a `n+1`-ary functor -/
+def drop : mvpfunctor n :=
+{ A := P.A, B := λ a, (P.B a).drop }
+
+/-- Split polynomial functor, get a univariate functor
+from a `n+1`-ary functor -/
+def last : pfunctor :=
+{ A := P.A, B := λ a, (P.B a).last }
+
+/-- append arrows of a polynomial functor application -/
+@[reducible] def append_contents {α : typevec n} {β : Type*}
+    {a : P.A} (f' : P.drop.B a ⟹ α) (f : P.last.B a → β) :
+  P.B a ⟹ α ::: β :=
+split_fun f' f
+
+end mvpfunctor

src/data/pfunctor/univariate/basic.lean

@@ -69,6 +69,14 @@ such that `P.B a` is empty to yield a finite tree -/
 attribute [nolint has_inhabited_instance] W
 variables {P}
 
+/-- root element  of a W tree -/
+def W.head : W P → P.A
+| ⟨a, f⟩ := a
+
+/-- children of the root of a W tree -/
+def W.children : Π x : W P, P.B (W.head x) → W P
+| ⟨a, f⟩ := f
+
 /-- destructor for W-types -/
 def W.dest : W P → P.obj (W P)
 | ⟨a, f⟩ := ⟨a, f⟩