search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.87k stars 656 forks source link

Ltac2 Constr.Unsafe.case type should expose the inductive and the number of parameters #10940

Open JasonGross opened 5 years ago

JasonGross commented 5 years ago

Description of the problem

It is useful when writing inversion-style automation to know how many parameters an inductive type should have. It is also sometimes important to know, given a match statement, which inductive is being matched. Hence there should be projections case -> inductive and case -> int (perahaps inductive_of_case and nbparameters_of_case?) which correspond to ci_ind and ci_npar in constr.mli¹ and to the tuple ind_and_nbparams in template-coq².

¹ https://github.com/coq/coq/blob/e6991dce306c41352c359a8ba5d6d9d6c5e6dfb2/kernel/constr.mli#L38-L39

² https://github.com/MetaCoq/metacoq/blob/1086391b66b82d10e9aa8d23411344ae9a49bbd4/template-coq/theories/Ast.v#L52

cc @ppedrot @andres-erbsen

Coq Version

master

Zimmi48 commented 4 years ago

@ppedrot Do you intend to address this in time for 8.12? If that's the case, there should be an assignee. If not, please remove or adjust the milestone.

ppedrot commented 4 years ago

This is not urgent, so postponing.

Zimmi48 commented 4 years ago

This was already postponed once. Not a problem, but maybe the milestone could be simply removed?

samuelgruetter commented 4 years ago

Having access to the number of parameters of an Inductive would be a useful feature! Lack of this feature in Ltac 1 made me come up with hacks like this one, where I derive the number of parameters by checking for how many arguments passed to a constructor, the induction principle can be specialized with the argument (which is only the case for parameters, but not for indices).

gares commented 4 years ago

@ppedrot I'd like an update w.r.t. this PR and its milestone

ppedrot commented 4 years ago

It's an issue, not a PR, so postpone.

gares commented 4 years ago

My interpretation of milestoned issues, is that they have something to do with that release. So I'm not postponing, but rather clearing the milestone.