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):

https://github.com/Blaisorblade/Coq-playground/blob/32e830b494565268f7409b1de0bf153ae0bb666c/theories/test_isyn.v#L132-L212

Last updated: Oct 13 2024 at 01:02 UTC