Paolo Giarrusso (Jun 18 2020 at 21:39): 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.
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.
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 :-(.
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.
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.
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: Jun 11 2023 at 00:30 UTC