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.
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 :-(.
Hmm, the tactic should certainly be hardened to ensure the prerequesites are available. There is now support for that in the Derive framework.
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.
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):
Last updated: Jan 29 2023 at 14:02 UTC