Stream: Coq users

Topic: ✔ Nested inductive decidable equality

Vincent Siles (Sep 28 2021 at 09:02):

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 ?

Vincent Siles (Sep 28 2021 at 11:04):

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

Karl Palmskog (Sep 28 2021 at 11:23):

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.

Karl Palmskog (Sep 28 2021 at 11:26):

you probably want to use EqDecision expr (without the arguments) instead of Decision (e = e')

Vincent Siles (Sep 28 2021 at 11:30):

What's the difference between EqDecision and Decision ?

Karl Palmskog (Sep 28 2021 at 11:31):

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

Paolo Giarrusso (Sep 28 2021 at 11:32):

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

Paolo Giarrusso (Sep 28 2021 at 11:35):

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.

Paolo Giarrusso (Sep 28 2021 at 11:36):

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

Paolo Giarrusso (Sep 28 2021 at 11:38):

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

Notification Bot (Nov 24 2021 at 08:19):

Vincent Siles has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC