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
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
you can see the exact definition in
base.v in stdpp, but
EqDecision is a notation for
eq, which in turn is a "subclass" of
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: Jan 31 2023 at 12:01 UTC