feat(data/univariate/qpf): compositional data type framework for (co)…

…inductive types (#3325)

Define univariate QPFs (quotients of polynomial functors).  This is the first part of #3317.

docs/references.bib

@@ -274,3 +274,47 @@ @misc{wedhorn_adic
 Year = {2019},
 Eprint = {arXiv:1910.05934},
 }
+
+@inproceedings{avigad-carneiro-hudon2019,
+  author    = {Jeremy Avigad and
+               Mario M. Carneiro and
+               Simon Hudon},
+  editor    = {John Harrison and
+               John O'Leary and
+               Andrew Tolmach},
+  title     = {Data Types as Quotients of Polynomial Functors},
+  booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
+               2019, September 9-12, 2019, Portland, OR, {USA}},
+  series    = {LIPIcs},
+  volume    = {141},
+  pages     = {6:1--6:19},
+  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+  year      = {2019},
+  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
+  doi       = {10.4230/LIPIcs.ITP.2019.6},
+  timestamp = {Fri, 27 Sep 2019 15:57:06 +0200},
+  biburl    = {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{fuerer-lochbihler-schneider-traytel2020,
+  author    = {Basil F{\"{u}}rer and
+               Andreas Lochbihler and
+               Joshua Schneider and
+               Dmitriy Traytel},
+  editor    = {Nicolas Peltier and
+               Viorica Sofronie{-}Stokkermans},
+  title     = {Quotients of Bounded Natural Functors},
+  booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
+               2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {12167},
+  pages     = {58--78},
+  publisher = {Springer},
+  year      = {2020},
+  url       = {https://doi.org/10.1007/978-3-030-51054-1\_4},
+  doi       = {10.1007/978-3-030-51054-1\_4},
+  timestamp = {Mon, 06 Jul 2020 09:05:32 +0200},
+  biburl    = {https://dblp.org/rec/conf/cade/FurerLST20.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}

src/control/functor.lean

@@ -172,6 +172,27 @@ instance : applicative (comp F G) :=
 
 end comp
 
+variables {F : Type u → Type u} [functor F]
+
+/-- If we consider `x : F α` to, in some sense, contain values of type `α`, 
+predicate `liftp p x` holds iff, every value contained by `x` satisfies `p` -/
+def liftp {α : Type u} (p : α → Prop) (x : F α) : Prop :=
+∃ u : F (subtype p), subtype.val <$> u = x
+
+/-- `liftr r x y` relates `x` and `y` iff `x` and `y` have the same shape and that 
+we can pair values `a` from `x` and `b` from `y` so that `r a b` holds -/
+def liftr {α : Type u} (r : α → α → Prop) (x y : F α) : Prop :=
+∃ u : F {p : α × α // r p.fst p.snd},
+  (λ t : {p : α × α // r p.fst p.snd}, t.val.fst) <$> u = x ∧
+  (λ t : {p : α × α // r p.fst p.snd}, t.val.snd) <$> u = y
+
+/-- `supp x` is the set of values of type `α` that `x` contains -/
+def supp {α : Type u} (x : F α) : set α := { y : α | ∀ ⦃p⦄, liftp p x → p y }
+
+theorem of_mem_supp {α : Type u} {x : F α} {p : α → Prop} (h : liftp p x) :
+  ∀ y ∈ supp x, p y :=
+λ y hy, hy h
+
 end functor
 
 namespace ulift