Stream: Equations devs & users

Topic: Derive NoConfusionHom for an eq-like type


view this post on Zulip 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.

view this post on Zulip James Wood (Sep 21 2022 at 16:28):

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: Jan 29 2023 at 15:02 UTC