Stream: Coq users

Topic: ✔ Nested inductive decidable equality


view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 28 2021 at 11:26):

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

view this post on Zulip Vincent Siles (Sep 28 2021 at 11:30):

What's the difference between EqDecision and Decision ?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Notification Bot (Nov 24 2021 at 08:19):

Vincent Siles has marked this topic as resolved.


Last updated: Jan 31 2023 at 12:01 UTC