Hello! I have used to have several inductive propositions.
However due to some problems, I had to change to use recursive definitions than inductive.
Specifically, performing inversion in ssreflect is quite finicky, while inductive definitions often call for inversion.
I would still like inductive definitions, as it would not allow unfolding of recursive definitions.
Is it possible to use inductive propositions idiomatically with ssreflect?
https://sympa.inria.fr/sympa/arc/ssreflect/2014-10/msg00004.html is probably still relevant — note Gonthier's answer
(not just the linked message, but the two replies).
FTR, there are ways to block the unfolding of recursive definitions, see for example
Arguments ... : simpl ....
I do not get this part:
(1) generate new constants for the dependent indices of the instance of predicate family being inverted, and equations relating them to the actual indices; replacing the actual indices with the corresponding constants in the instance (2) destruct the predicate; this replaces the constants introduced in (1) with the index value specified by individual constructors, in the equations; note that this also introduces the constructor arguments.
Could you explain this part in detail, preferably with an example?
Enrico: Thank you! Just realized, the arguments one might be useful for me!
Last updated: Jan 29 2023 at 19:02 UTC