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

.

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