feat: Add elaboration of elimination constraints

dev/ci/user-overlays/21417-mattam82-elab-elim-constraints.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/mattam82/coq-elpi elab-elim-constraints 21417

dev/top_printers.dbg

@@ -73,6 +73,7 @@ install_printer Top_printers.pperelevance
 install_printer Top_printers.ppqvar
 install_printer Top_printers.ppuni_level
 install_printer Top_printers.ppqvarset
+install_printer Top_printers.ppqset
 install_printer Top_printers.ppuniverse_set
 install_printer Top_printers.ppuniverse_instance
 install_printer Top_printers.ppuniverse_einstance
@@ -90,6 +91,7 @@ install_printer Top_printers.ppuniverseconstraints
 install_printer Top_printers.ppuniverse_context_future
 install_printer Top_printers.ppuniverses
 install_printer Top_printers.ppqualities
+install_printer Top_printers.ppelim_constraints
 install_printer Top_printers.pp_partialfsubst
 install_printer Top_printers.pp_partialsubst
 install_printer Top_printers.ppnamedcontextval

dev/top_printers.ml

@@ -290,6 +290,7 @@ let pperelevance r = pprelevance (EConstr.Unsafe.to_relevance r)
 let prlev l = UnivNames.pr_level_with_global_universes l
 let prqvar q = UnivNames.pr_quality_with_global_universes q
 let ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc prqvar (QVar.Set.elements l) ++ str "}"))
+let ppqset qs = pp (hov 1 (str "{" ++ prlist_with_sep spc (Quality.pr prqvar) (Quality.Set.elements qs) ++ str "}"))
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
 let ppuniverse_einstance l = ppuniverse_instance (EConstr.Unsafe.to_instance l)
@@ -308,6 +309,7 @@ let ppuniverse_context_future c =
     ppuniverse_context ctx
 let ppuniverses u = pp (UGraph.pr_universes Level.raw_pr (UGraph.repr u))
 let ppqualities q = pp (QGraph.pr_qualities Quality.raw_pr q)
+let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr prqvar cstrs)
 let ppnamedcontextval e =
   let env = Global.env () in
   let sigma = Evd.from_env env in

dev/top_printers.mli

@@ -154,6 +154,7 @@ val ppesorts : EConstr.ESorts.t -> unit
 val pperelevance : EConstr.ERelevance.t -> unit
 val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
 val ppqvarset : Sorts.QVar.Set.t -> unit
+val ppqset : Sorts.Quality.Set.t -> unit
 val ppuniverse_set : Univ.Level.Set.t -> unit
 val ppuniverse_instance : UVars.Instance.t -> unit
 val ppuniverse_einstance : EConstr.EInstance.t -> unit
@@ -171,6 +172,7 @@ val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : UVars.UContext.t Future.computation -> unit
 val ppuniverses : UGraph.t -> unit
 val ppqualities : QGraph.t -> unit
+val ppelim_constraints : Sorts.ElimConstraints.t -> unit
 
 val pp_partialfsubst : (CClosure.fconstr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit
 val pp_partialsubst : (EConstr.constr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit

doc/changelog/02-specification-language/21417-elab-elim-constraints-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  implicit elaboration of :ref:`elimination constraints <elim-constraints>`
+  (`#21417 <https://github.com/rocq-prover/rocq/pull/21417>`_,
+  by Tomas Diaz).

doc/sphinx/addendum/universe-polymorphism.rst

@@ -855,22 +855,22 @@ witness these temporary variables.
 Sort polymorphic inductives may be declared when every instantiation
 is valid.
 
-Elimination at a given universe instance requires that elimination is
-allowed at every ground instantiation of the sort variables in the
-instance. Additionally if the output sort at the given universe
-instance is sort polymorphic, the return type of the elimination must
-be at the same quality. These restrictions ignore :flag:`Definitional
-UIP`.
+.. _elim-constraints:
 
-For instance
+Elimination of Sort-Polymorphic Inductives
+------------------------------------------
+
+Sort-polymorphic inductives follow rules for their elimination, both
+when the target sort is polymorphic or not. We illustrate the first case
+on the following example:
 
 .. rocqtop:: all reset
 
    Set Universe Polymorphism.
 
    Inductive Squash@{s;u} (A:Type@{s;u}) : Prop := squash (_:A).
 
-Elimination to `Prop` and `SProp` is always allowed, so `Squash_ind`
+Here, elimination to `Prop` and `SProp` is always allowed, so `Squash_ind`
 and `Squash_sind` are automatically defined.
 
 Elimination to `Type` is not allowed with variable `s`, because the
@@ -890,19 +890,94 @@ However elimination to `Type` or to a polymorphic sort with `s := Prop` is allow
      : forall s, P s
      := fun s => match s with squash _ x => H x end.
 
+In fact, for a given universe instance, elimination is allowed if:
+
+- it is allowed for every ground instantiation of the sort variables in the instance, or
+
+- the output sort at the given universe instance is sort polymorphic and
+  the return type of the elimination is at the same quality.
+
+For instance, for the following inductive, elimination is not allowed unless the target sort of
+the inductive matches the sort it is eliminated to.
+
+.. rocqtop:: all
+
+   Inductive sum@{sl sr s;ul ur} (A:Type@{sl;ul}) (B:Type@{sr;ur}) : Type@{s;max(ul,ur)} :=
+   | inl (_:A)
+   | inr (_:B).
+
+.. rocqtop:: none
+
+   Arguments inl {_ _} _.
+   Arguments inr {_ _} _.
+
+.. rocqtop:: all
+
+   Fail Definition sum_elim@{sl sr s s';ul ur u'|}
+     (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+     (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+     (v : sum@{sl sr s;ul ur} A B) : P v :=
+         match v with
+         | inl x => fl x
+         | inr y => fr y
+         end.
+
+As this greatly inhibits the possibilities of sort polymorphism, we have introduced *elimination
+constraints* to manage these cases. Here, the annotation `s -> s'` can be added
+to tell Rocq that the definition is allowed for *every* sorts `s`, `s'` such that `s` eliminates
+into `s'`.
+
+.. rocqtop:: all
+
+   Definition sum_elim@{sl sr s s';ul ur u'|s -> s'}
+     (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+     (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+     (v : sum@{sl sr s;ul ur} A B) : P v :=
+         match v with
+         | inl x => fl x
+         | inr y => fr y
+         end.
+
+It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and `Prop` or
+`Prop` and `SProp`, but cannot be instantiated to e.g., `Prop` and `Type` or `SProp` and
+`Prop`.
+
+.. rocqtop:: all
+
+   Check sum_elim@{_ _ Type Prop;_ _ _}.
+   Check sum_elim@{_ _ Prop SProp;_ _ _}.
+   Fail Check sum_elim@{_ _ Prop Type;_ _ _}.
+   Fail Check sum_elim@{_ _ SProp Prop;_ _ _}.
+
 .. note::
 
-   Since inductive types with sort polymorphic output may only be
-   polymorphically eliminated to the same sort quality, containers
-   such as sigma types may be better defined as primitive records (which
-   do not have this restriction) when possible.
+   As with universe level constraints, elimination constraints can be elaborated
+   automatically if the constraints are denoted extensible with `+` **or** if they
+   are totally omitted. For instance, the two following definitions are legal.
 
    .. rocqtop:: all
 
-      Set Primitive Projections.
-      Record sigma@{s;u v} (A:Type@{s;u}) (B:A -> Type@{s;v})
-        : Type@{s;max(u,v)}
-        := pair { pr1 : A; pr2 : B pr1 }.
+      Definition sum_elim_ext@{sl sr s s';ul ur u'|+}
+        (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+        (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+        (v : sum@{sl sr s;ul ur} A B) : P v :=
+            match v with
+                | inl x => fl x
+                | inr y => fr y
+                end.
+
+      Definition sum_elim_elab@{sl sr s s';ul ur u'}
+        (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+        (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+        (v : sum@{sl sr s;ul ur} A B) : P v :=
+            match v with
+                | inl x => fl x
+                | inr y => fr y
+                end.
+
+.. note::
+
+    These restrictions ignore :flag:`Definitional UIP`.
 
 .. flag:: Printing Sort Qualities
 
@@ -915,7 +990,8 @@ However elimination to `Type` or to a polymorphic sort with `s := Prop` is allow
 Explicit Sorts
 ---------------
 
-Similar to universes, fresh global sorts can be declared with the :cmd:`Sort`.
+Similar to universes, fresh global sorts can be declared with the :cmd:`Sort`, and elimination
+constraint on global sorts can be declared with the :cmd:`Constraint`.
 
 .. cmd:: Sort {+ @ident }
          Sorts {+ @ident }

engine/eConstr.mli

@@ -331,6 +331,8 @@ val whd_evar : Evd.evar_map -> constr -> constr
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
 val eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
+(** Does not produce QLeq nor QElimTo constraints *)
+
 val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
 val eq_existential : Evd.evar_map ->  (t -> t -> bool) -> existential -> existential -> bool
 

engine/evd.ml

@@ -1176,6 +1176,9 @@ let set_above_prop evd q =
   add_constraints evd @@
     UnivProblem.Set.singleton (QLeq (Sorts.Quality.qprop, q))
 
+let set_elim_to evd q1 q2 =
+  add_constraints evd @@ UnivProblem.Set.singleton (QElimTo (q1, q2))
+
 let check_eq evd s s' =
   let quals = elim_graph evd in
   let ustate = evd.universes in

engine/evd.mli

@@ -597,6 +597,7 @@ val set_eq_instances : ?flex:bool ->
   evar_map -> einstance -> einstance -> evar_map
 
 val set_eq_qualities : evar_map -> Sorts.Quality.t -> Sorts.Quality.t -> evar_map
+val set_elim_to : evar_map -> Sorts.Quality.t -> Sorts.Quality.t -> evar_map
 val set_above_prop : evar_map -> Sorts.Quality.t -> evar_map
 
 val check_eq : evar_map -> esorts -> esorts -> bool

engine/uState.ml

@@ -284,10 +284,12 @@ let collapse ?(except=QSet.empty) m =
 
 let pr prqvar_opt ({ qmap; elims; rigid } as m) =
   let open Pp in
+  (* Print the QVar using its name if any, e.g. "α1" or "s" *)
   let prqvar q = match prqvar_opt q with
     | None -> QVar.raw_pr q
     | Some qid -> Libnames.pr_qualid qid
   in
+  (* Print the "body" of the QVar, e.g. "α1 := Type", "α2 >= Prop" *)
   let prbody u = function
   | None ->
     if is_above_prop m u then str " >= Prop"
@@ -298,12 +300,15 @@ let pr prqvar_opt ({ qmap; elims; rigid } as m) =
     let q = Quality.pr prqvar q in
     str " := " ++ q
   in
+  (* Print the "name" (given by the user) of the Qvar, e.g. "(named s)" *)
   let prqvar_name q =
     match prqvar_opt q with
-    | None -> mt()
+    | None -> mt ()
     | Some qid -> str " (named " ++ Libnames.pr_qualid qid ++ str ")"
   in
-  h (prlist_with_sep fnl (fun (u, v) -> QVar.raw_pr u ++ prbody u v ++ prqvar_name u) (QMap.bindings qmap))
+  let prqvar_full (q1, q2) = QVar.raw_pr q1 ++ prbody q1 q2 ++ prqvar_name q1 in
+  hov 0 (prlist_with_sep fnl prqvar_full (QMap.bindings qmap) ++
+    str " |=" ++ brk (1, 2) ++ hov 0 (QGraph.pr_qualities (Quality.pr prqvar) elims))
 
 let elims m = m.elims
 
@@ -703,6 +708,7 @@ let process_constraints uctx cstrs =
     Sorts.subst_fn ((qnormalize sorts), subst_univs_universe normalize) s
   in
   let nf_constraint sorts = function
+    | QElimTo (a, b) -> QElimTo (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | QLeq (a, b) -> QLeq (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | QEq (a, b) -> QEq (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
@@ -787,6 +793,7 @@ let process_constraints uctx cstrs =
       match cst with
     | QEq (a, b) -> unify_quality univs CONV (mk a) (mk b) local
     | QLeq (a, b) -> unify_quality univs CUMUL (mk a) (mk b) local
+    | QElimTo (a, b) -> { local with local_cst = PConstraints.add_quality (a, ElimTo, b) local.local_cst }
     | ULe (l, r) ->
       let local = unify_quality univs CUMUL l r local in
       let l = normalize_sort local.local_sorts l in
@@ -902,20 +909,22 @@ let problem_of_univ_constraints cstrs =
       in UnivProblem.Set.add cstr' acc)
     cstrs UnivProblem.Set.empty
 
+let problem_of_elim_constraints cstrs =
+  ElimConstraints.fold (fun (l, k, r) pbs ->
+      let open ElimConstraint in
+      match k with
+      | ElimTo -> UnivProblem.Set.add (QElimTo (l, r)) pbs
+      | Equal -> UnivProblem.Set.add (QEq (l, r)) pbs)
+    cstrs UnivProblem.Set.empty
+
 let add_univ_constraints uctx cstrs =
   let cstrs = problem_of_univ_constraints cstrs in
   add_constraints ~src:Static uctx cstrs
 
 let add_poly_constraints ?src uctx (qcstrs, ucstrs) =
-  let ucstrs = problem_of_univ_constraints ucstrs in
-  (* XXX when elimination constraints become available in unification we should
-     rely on it rather than playing this little dance *)
-  let fold (s1, pb, s2) (qeq, qelm) = match pb with
-  | ElimConstraint.ElimTo -> (qeq, ElimConstraints.add (s1, pb, s2) qelm)
-  | ElimConstraint.Equal -> (UnivProblem.Set.add (QEq (s1, s2)) qeq, qelm)
-  in
-  let qeq, qcstrs = ElimConstraints.fold fold qcstrs (UnivProblem.Set.empty, ElimConstraints.empty) in
-  let uctx = add_constraints ?src uctx (UnivProblem.Set.union ucstrs qeq) in
+  let lvl_pbs = problem_of_univ_constraints ucstrs in
+  let elim_pbs = problem_of_elim_constraints qcstrs in
+  let uctx = add_constraints ?src uctx (UnivProblem.Set.union lvl_pbs elim_pbs) in
   let local = on_snd (fun cst -> PConstraints.union cst (PConstraints.of_qualities qcstrs)) uctx.local in
   let sort_variables = QState.merge_constraints (fun cst -> merge_elim_constraints ?src uctx qcstrs cst) uctx.sort_variables in
   { uctx with local; sort_variables }
@@ -945,6 +954,10 @@ let check_constraint uctx (c:UnivProblem.t) =
         | QConstant QProp, QVar q -> QState.is_above_prop uctx.sort_variables q
         | (QConstant _ | QVar _), _ -> false
       end
+  | QElimTo (a, b) ->
+    let a = nf_quality uctx a in
+    let b = nf_quality uctx b in
+    Inductive.eliminates_to (QState.elims uctx.sort_variables) a b
   | ULe (u,v) -> UGraph.check_leq_sort (elim_graph uctx) uctx.universes u v
   | UEq (u,v) -> UGraph.check_eq_sort (elim_graph uctx) uctx.universes u v
   | ULub (u,v) -> UGraph.check_eq_level uctx.universes u v

engine/univProblem.ml

@@ -14,19 +14,21 @@ open Sorts
 type t =
   | QEq of Quality.t * Quality.t
   | QLeq of Quality.t * Quality.t
+  | QElimTo of Quality.t * Quality.t
   | ULe of Sorts.t * Sorts.t
   | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t
   | UWeak of Level.t * Level.t
 
 let is_trivial = function
   | QLeq (a,b) -> Inductive.raw_eliminates_to a b
+  | QElimTo (a, b) -> Inductive.raw_eliminates_to a b
   | QEq (a, b) -> Quality.equal a b
   | ULe (u, v) | UEq (u, v) -> Sorts.equal u v
   | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
 let force = function
-  | QEq _ | QLeq _ | ULe _ | UEq _ | UWeak _ as cst -> cst
+  | QEq _ | QElimTo _ | QLeq _ | ULe _ | UEq _ | UWeak _ as cst -> cst
   | ULub (u,v) -> UEq (Sorts.sort_of_univ @@ Universe.make u, Sorts.sort_of_univ @@ Universe.make v)
 
 let check_eq_level g u v = UGraph.check_eq_level g u v
@@ -37,12 +39,15 @@ module Set = struct
     type nonrec t = t
 
     let compare x y =
-      match x, y with
-      | (QEq (a, b) | QLeq (a, b)),
-        (QEq (a', b') | QLeq (a', b')) ->
+      let compare_qualities (a, b) (a', b') =
         let i = Quality.compare a a' in
         if i <> 0 then i
         else Quality.compare b b'
+      in
+      match x, y with
+      | QEq (a, b), QEq (a', b')
+      | QLeq (a, b), QLeq (a', b')
+      | QElimTo (a, b), QElimTo (a', b') -> compare_qualities (a, b) (a', b')
       | ULe (u, v), ULe (u', v') ->
         let i = Sorts.compare u u' in
         if Int.equal i 0 then Sorts.compare v v'
@@ -61,6 +66,8 @@ module Set = struct
       | _, QEq _ -> 1
       | QLeq _, _ -> -1
       | _, QLeq _ -> 1
+      | QElimTo _, _ -> -1
+      | _, QElimTo _ -> 1
       | ULe _, _ -> -1
       | _, ULe _ -> 1
       | UEq _, _ -> -1
@@ -78,6 +85,7 @@ module Set = struct
   let pr_one = let open Pp in function
     | QEq (a, b) -> Quality.raw_pr a ++ str " = " ++ Quality.raw_pr b
     | QLeq (a, b) -> Quality.raw_pr a ++ str " <= " ++ Quality.raw_pr b
+    | QElimTo (a, b) -> Quality.raw_pr a ++ str " -> " ++ Quality.raw_pr b
     | ULe (u, v) -> Sorts.debug_print u ++ str " <= " ++ Sorts.debug_print v
     | UEq (u, v) -> Sorts.debug_print u ++ str " = " ++ Sorts.debug_print v
     | ULub (u, v) -> Level.raw_pr u ++ str " /\\ " ++ Level.raw_pr v

engine/univProblem.mli

@@ -23,6 +23,7 @@ open UVars
 type t =
   | QEq of Sorts.Quality.t * Sorts.Quality.t
   | QLeq of Sorts.Quality.t * Sorts.Quality.t
+  | QElimTo of Sorts.Quality.t * Sorts.Quality.t
   | ULe of Sorts.t * Sorts.t
   | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t

kernel/pConstraints.ml

@@ -61,9 +61,10 @@ let filter_univs f (qc, lc) =
 
 let pr prv prl (qc, lc) =
   let open Pp in
-  let ppelim = if ElimConstraints.is_empty qc then mt()
-               else ElimConstraints.pr prv qc ++ str"," in
-  v 0 (ppelim ++ UnivConstraints.pr prl lc)
+  let sep = if ElimConstraints.is_empty qc || UnivConstraints.is_empty lc
+            then mt ()
+            else pr_comma () in
+  v 0 (ElimConstraints.pr prv qc ++ sep ++ UnivConstraints.pr prl lc)
 
 module HPConstraints =
   Hashcons.Make(