Skip to content

feat: Generate sort poly scheme with elim constraints #21567

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
TDiazT wants to merge 3 commits into
base: master
Choose a base branch
from
+96 −40
Draft

feat: Generate sort poly scheme with elim constraints #21567

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5f6b5da
feat: Generate sort poly scheme with elim constraints
tabareau Jul 1, 2025
ac38f52
misc: Add comment
TDiazT Jan 30, 2026
6adba70
Update tactics/elimschemes.ml
TDiazT Feb 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 39 additions & 2 deletions tactics/elimschemes.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,25 @@ let default_case_analysis_dependence env ind =
(* Induction/recursion schemes *)
(* **************************************************** *)

let build_induction_scheme_in_sort_var env dep ind =
let sigma = Evd.from_env env in
let sigma, pind =
Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind
in
(* Get new sort for output *)
let sigma, pred_sort = Evd.new_sort_variable UnivRigid sigma in
let pred_quality = EConstr.ESorts.quality sigma pred_sort in
(* Get sort of inductive *)
let _, ind_sort =
EConstr.destArity sigma
(Retyping.get_type_of env sigma (EConstr.mkIndU pind))
in
let ind_quality = EConstr.ESorts.quality sigma ind_sort in
(* Set elimination constraint from inductive to output's sort *)
let sigma = Evd.set_elim_to sigma ind_quality pred_quality in
let sigma, c = build_induction_scheme env sigma pind dep pred_sort in
(EConstr.to_constr sigma c, Evd.ustate sigma)

let build_induction_scheme_in_type env dep sort ind =
let sigma = Evd.from_env env in
let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
Expand All @@ -76,6 +95,10 @@ let sind_dep =
declare_individual_scheme_object "sind_dep"
(fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.sprop x)

let poly_dep =
declare_individual_scheme_object "poly_dep"
(fun env _ x -> build_induction_scheme_in_sort_var env true x)

let rect_nodep =
declare_individual_scheme_object "rect_nodep"
(fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.qtype x)
Expand All @@ -92,6 +115,10 @@ let sind_nodep =
declare_individual_scheme_object "sind_nodep"
(fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.sprop x)

let poly_nodep =
declare_individual_scheme_object "poly_nodep"
(fun env _ x -> build_induction_scheme_in_sort_var env false x)

let elim_scheme ~dep ~to_kind =
let open QualityOrSet in
match to_kind with
Expand All @@ -100,10 +127,12 @@ let elim_scheme ~dep ~to_kind =
match q with
| QConstant QSProp when dep -> sind_dep
| QConstant QProp when dep -> ind_dep
| (QConstant QType | QVar _) when dep -> rect_dep
| QConstant QType when dep -> rect_dep
| Sorts.Quality.QVar _ when dep -> poly_dep
| QConstant QSProp -> sind_nodep
| QConstant QProp -> ind_nodep
| QConstant QType | QVar _ -> rect_nodep
| QConstant QType -> rect_nodep
| Sorts.Quality.QVar _ -> poly_nodep
end
| Set -> if dep then rec_dep else rec_nodep

Expand Down Expand Up @@ -199,6 +228,14 @@ let case_nodep =
declare_individual_scheme_object "case_nodep"
(fun env _ x -> build_case_analysis_scheme_in_type env false QualityOrSet.qtype x)

let case_poly_dep q =
declare_individual_scheme_object "case_poly_dep"
(fun env _ x -> build_case_analysis_scheme_in_type env true (QualityOrSet.Qual q) x)

let case_poly_nodep q =
declare_individual_scheme_object "case_poly_nodep"
(fun env _ x -> build_case_analysis_scheme_in_type env false (QualityOrSet.Qual q) x)

let casep_dep =
declare_individual_scheme_object "casep_dep"
(fun env _ x -> build_case_analysis_scheme_in_type env true QualityOrSet.prop x)
Expand Down
2 changes: 2 additions & 0 deletions tactics/elimschemes.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ val elim_scheme : dep:bool -> to_kind:UnivGen.QualityOrSet.t -> individual schem
val case_dep : individual scheme_kind
val case_nodep : individual scheme_kind
val casep_dep : individual scheme_kind
val case_poly_dep : Sorts.Quality.t -> individual scheme_kind
val case_poly_nodep : Sorts.Quality.t -> individual scheme_kind
Comment on lines +39 to +40
Copy link
Contributor Author

@TDiazT TDiazT Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

idem, recheck

val casep_nodep : individual scheme_kind

(** Recursor names utilities *)
Expand Down
93 changes: 55 additions & 38 deletions vernac/indschemes.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -218,45 +218,61 @@ let declare_one_case_analysis_scheme ?loc ind =

(* Induction/recursion schemes *)

let declare_one_induction_scheme ?loc ind =
let (mib,mip) as specif = Global.lookup_inductive ind in
let kind = Elimschemes.pseudo_sort_quality_for_elim ind mip in
let from_prop = Sorts.Quality.is_qprop kind in
let depelim = Inductiveops.has_dependent_elim specif in
let kelim mip = Inductiveops.constant_sorts_below
@@ Inductiveops.elim_sort (mib,mip) in
let kelim =
List.fold_right (fun x acc ->
List.intersect UnivGen.QualityOrSet.equal acc x)
(List.map kelim (Array.to_list mib.mind_packets))
[UnivGen.QualityOrSet.qtype; UnivGen.QualityOrSet.prop; UnivGen.QualityOrSet.set; UnivGen.QualityOrSet.sprop] in
let kelim =
if Global.sprop_allowed ()
then kelim
else List.filter (fun s -> not (UnivGen.QualityOrSet.is_sprop s)) kelim
in
let elims =
List.filter (fun (sort,_) -> List.mem_f UnivGen.QualityOrSet.equal sort kelim)
[(UnivGen.QualityOrSet.qtype, "rect");
(UnivGen.QualityOrSet.prop, "ind");
(UnivGen.QualityOrSet.set, "rec");
(UnivGen.QualityOrSet.sprop, "sind")]
let declare_one_induction_scheme_poly ?loc ind (mib, mip) q =
let scheme_kind =
elim_scheme ~dep:true ~to_kind:(UnivGen.QualityOrSet.Qual q)
in
let elims = List.map (fun (to_kind,dflt_suff) ->
if from_prop then elim_scheme ~dep:false ~to_kind, Some dflt_suff
else if depelim then elim_scheme ~dep:true ~to_kind, Some dflt_suff
else elim_scheme ~dep:false ~to_kind, None)
let suff = "_poly_rec" in
let id = Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ suff)) in
define_individual_scheme ?loc scheme_kind id ind

let declare_one_induction_scheme_const ?loc ind (mib, mip as specif) kind =
let from_prop = Sorts.Quality.is_qprop kind in
let depelim = Inductiveops.has_dependent_elim specif in
let kelim mip = Inductiveops.constant_sorts_below
@@ Inductiveops.elim_sort (mib,mip) in
let kelim =
List.fold_right (fun x acc ->
List.intersect UnivGen.QualityOrSet.equal acc x)
(List.map kelim (Array.to_list mib.mind_packets))
[UnivGen.QualityOrSet.qtype; UnivGen.QualityOrSet.prop; UnivGen.QualityOrSet.set; UnivGen.QualityOrSet.sprop] in
let kelim =
if Global.sprop_allowed ()
then kelim
else List.filter (fun s -> not (UnivGen.QualityOrSet.is_sprop s)) kelim
in
let elims =
List.filter (fun (sort, _) -> List.mem_f UnivGen.QualityOrSet.equal sort kelim)
(* NB: the order is important, it makes it so that _rec is
defined using _rect but _ind is not. *)
[(UnivGen.QualityOrSet.qtype, "rect");
(UnivGen.QualityOrSet.prop, "ind");
(UnivGen.QualityOrSet.set, "rec");
(UnivGen.QualityOrSet.sprop, "sind")]
in
let elims = List.map (fun (to_kind, dflt_suff) ->
if from_prop then elim_scheme ~dep:false ~to_kind, Some dflt_suff
Copy link
Contributor

@thomas-lamiaux thomas-lamiaux Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not in your code, you do dependent by default

Copy link
Contributor

@thomas-lamiaux thomas-lamiaux Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can't you mege both functions as before by simply adding an element to elims ?

Copy link
Contributor Author

@TDiazT TDiazT Feb 2, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yup, that's what I was doing before but, to be honest, a lot of the code in the original declare_one_induction_scheme was really adhoc for handling Type, Prop, and SProp specific cases.

For sort variables it's really short actually, so I preferred to separate them, making it easier to understand imo. I just renamed the original declare_one_induction_scheme to declare_one_induction_scheme_const but otherwise is the same code.

else if depelim then elim_scheme ~dep:true ~to_kind, Some dflt_suff
else elim_scheme ~dep:false ~to_kind, None)
elims
in
List.iter (fun (kind, suff) ->
let id = match suff with
| None -> None
| Some suff ->
(* the auto generated eliminator may be called "rect" instead of eg "rect_dep" *)
Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ "_" ^ suff))
in
define_individual_scheme ?loc kind id ind)
elims
in
List.iter (fun (kind, suff) ->
let id = match suff with
| None -> None
| Some suff ->
(* the auto generated eliminator may be called "rect" instead of eg "rect_dep" *)
Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ "_" ^ suff))
in
define_individual_scheme ?loc kind id ind)
elims

let declare_one_induction_scheme ?loc ind =
let ((mib, mip) as specif) = Global.lookup_inductive ind in
let quality = Elimschemes.pseudo_sort_quality_for_elim ind mip in
if Sorts.Quality.is_qvar quality then
declare_one_induction_scheme_poly ?loc ind specif quality
else
declare_one_induction_scheme_const ?loc ind specif quality

let declare_induction_schemes ?(locmap=Locmap.default None) kn =
let mib = Global.lookup_mind kn in
Expand Down Expand Up @@ -414,7 +430,8 @@ let do_mutual_induction_scheme ~register ?(force_mutual=false) env ?(isrec=true)
else match sort with
| Qual (QConstant QType) -> Some (if dep then case_dep else case_nodep)
| Qual (QConstant QProp) -> Some (if dep then casep_dep else casep_nodep)
| Set | Qual (QConstant QSProp | QVar _) ->
| Qual (QVar _ as q) -> Some (if dep then case_poly_dep q else case_poly_nodep q)
| Set | Qual (QConstant QSProp) ->
Comment on lines +433 to +434
Copy link
Contributor Author

@TDiazT TDiazT Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Need to recheck this. Probably extend build_case_analysis_scheme_in_type in the same way as the other.

Copy link
Contributor

@thomas-lamiaux thomas-lamiaux Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks alright to me

(* currently we don't have standard scheme kinds for this *)
None
in
Expand Down
Loading