## Stream: math-comp users

### Topic: ✔ Are inductive propositions unidiomatic in ssreflect?

#### 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: Jul 25 2024 at 16:02 UTC