Stream: Equations devs & users

Topic: Derive EqDec failing silently


view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 21:39):

Is there a way to get info about failures of Equations' Derive EqDec? The example below fails silently — derivation completes but produces no instance. While I found how to fix this example (by accident), but that doesn't help in a bigger example using mutual inductive, some of which are indexed (where decide equality also fails). Equations will tell me that I should use Derive Signature, but not that EqDec instances are missing for some contained type.

Require Import Coq.Numbers.BinNums.

From Equations Require Import Equations.

Derive EqDec for positive.

Instance positive_eqdec : EqDec positive.
Proof.
Fail apply _.
Abort.

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 21:51):

My _actual_ failure is on https://github.com/Blaisorblade/dot-iris/blob/3e991e814b42acc2448ccde0790d18534c521e7a/theories/Dot/syn/syn.v#L330 (and it is about a 6-way mutual inductive with 32 constructors:
https://github.com/Blaisorblade/dot-iris/blob/3e991e814b42acc2448ccde0790d18534c521e7a/theories/Dot/syn/syn.v#L39-L81). If needed, I could easily minimize it to exclude iris and stdpp — whose Unset Transparent Obligations. breaks Derive Eqdec even in simpler cases.

FWIW, derivation takes 5-7 seconds to fail, irrespective of how many reasons it has to fail — say, even if EqDec positive is missing.

view this post on Zulip Paolo Giarrusso (Jun 22 2020 at 18:47):

Ah. As usual, Next Obligation. shows what's missing (but the equation count is hidden from vscoq, causing the confusion). However, in the actual example, decidable equality opens an obligation for... decidable equality on one of the sorts :-(.

view this post on Zulip Matthieu Sozeau (Jun 23 2020 at 10:44):

Hmm, the tactic should certainly be hardened to ensure the prerequesites are available. There is now support for that in the Derive framework.

view this post on Zulip Matthieu Sozeau (Jun 23 2020 at 11:08):

It currently does not support mutual inductive types though, as it tries to derive EqDec independently for all the inductives in the mutual block. Should be doable though.

view this post on Zulip Paolo Giarrusso (Jun 23 2020 at 12:40):

Yeah, for now I resorted to writing the equations by hand with noind — at least the equation count is still linear (unlike the term size and equation count):
https://github.com/Blaisorblade/Coq-playground/blob/32e830b494565268f7409b1de0bf153ae0bb666c/theories/test_isyn.v#L132-L212


Last updated: Jan 29 2023 at 14:02 UTC