abab9579 (Sep 01 2022 at 07:17): abab9579 (Sep 01 2022 at 07:17):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?
Paolo Giarrusso (Sep 01 2022 at 09:38):https://sympa.inria.fr/sympa/arc/ssreflect/2014-10/msg00004.html is probably still relevant — note Gonthier's answer
Paolo Giarrusso (Sep 01 2022 at 09:38):(not just the linked message, but the two replies).
Enrico Tassi (Sep 01 2022 at 10:11):FTR, there are ways to block the unfolding of recursive definitions, see for example nosimpl or Arguments ... : simpl ....
abab9579 (Sep 01 2022 at 15:32):Paolo: 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?
EDIT: Nvm, I got it!
abab9579 (Sep 02 2022 at 00:02):Enrico: Thank you! Just realized, the arguments one might be useful for me!
Notification Bot (Sep 02 2022 at 00:35):abab9579 has marked this topic as resolved.
abab9579 (Sep 02 2022 at 00:59):By the way, it turned out me NOT simplifying was causing problem. That caused it to (likely) go for normal form when it had to be reduced.
Last updated: Apr 19 2024 at 00:02 UTC