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 `nosimpl`

or `Arguments ... : simpl ...`

.

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!

Enrico: Thank you! Just realized, the arguments one might be useful for me!

abab9579 has marked this topic as resolved.

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