James Wood (Sep 21 2022 at 15:00): James Wood (Sep 21 2022 at 15:00):The following minimised example generates 3 unsolved obligations.
From Equations Require Import Equations.
Inductive blob : Type := | base.
Variant myeq : blob -> blob -> Type :=
| myrefl {x} : myeq x x.
Derive NoConfusion EqDec for blob.
Derive NoConfusionHom for myeq.
I can solve the obligations by essentially aimless elimination until everything becomes trivial, as shown below. However, I think there should be a way to make use of the fact that blob is an h-set to dismiss these obligations, justified by the fact that (I think) dependent elimination "just works" with UIP. What would be the best approach, given that I want to add more inductive constructors to blob and more non-inductive constructors to myeq?
Next Obligation.
destruct a.
destruct x.
dependent elimination b1 as [myrefl].
reflexivity.
Defined.
Next Obligation.
destruct a.
destruct x.
dependent elimination b1 as [myrefl].
destruct e.
reflexivity.
Defined.
Next Obligation.
destruct b1.
destruct x.
reflexivity.
Defined.
Ah, there's a similar example in the issues (https://github.com/mattam82/Coq-Equations/issues/414), but I'd imagine there too that UIP for the type of the indices would be enough.
Last updated: Jun 10 2023 at 23:01 UTC