Hi ! I've got the usual mutually declared type

```
Inductive expr : Set :=
| Enat : nat -> expr
| Evar : string -> expr
| Ecall : expr -> list expr -> expr
```

and I'd like to derive a decidable equality with ` Global Instance expr_dec_eq (e e' : expr) : Decision (e = e').`

I'm using stdpp and `solve_decision`

doesn't succeed, my guess is because of `list expr`

.

Is there a way to declare a mutually defined Instance to have expr_dec_eq and list_expr_dec_eq defined at the same time ? Or do I have to do that by hand ?

FYI I managed to do a very quick proof by applying what's described here: https://coq.discourse.group/t/proving-properties-for-inductives-with-nested-inductives/174

in the usual jargon, the above example is (as the link implies) called "nested inductive", and mutual is reserved for declarations using Coq's mutual declaration mechanism.

you probably want to use `EqDecision expr`

(without the arguments) instead of `Decision (e = e')`

What's the difference between `EqDecision`

and `Decision`

?

you can see the exact definition in `base.v`

in stdpp, but `EqDecision`

is a notation for `RelDecision`

on `eq`

, which in turn is a "subclass" of `Decision`

Karl is right, but a few of the solutions (those using fixpoints) don't let you write EqDecision directly...

Eg https://github.com/Blaisorblade/dot-iris/blob/master/theories/Dot/syn/syn.v#L311. Here I think you'd just need a Fixpoint, and to manually declare it as an instance in the proof.

Oh, here you can declare it as an EqDecision instance, and use fix manually in the proof

But I haven't found an ideal way to replicate that for mutual fixpoints (without repeating the proof search, at least).

Vincent Siles has marked this topic as resolved.

Last updated: Oct 04 2023 at 23:01 UTC