Stream: Equations devs & users

Topic: ✔ Not finding a NoConfusion?

James Wood (May 18 2022 at 16:29):

Why do I get the following error at the end of the following file? I don't think I can get UIP on tree A without having UIP on A, but I surely do already have NoConfusion for any by the fact that I wrote the relevant Derive command and there didn't seem to be any errors or unsolved obligations at that point.

From Equations Require Import Equations.

Inductive tree {A : Type} : Type :=
  | zero | plus (s t : tree) | one (x : A).
Arguments tree A : clear implicits.
Derive NoConfusion for tree.

Inductive any {A} {T : A -> Type} : tree A -> Type :=
| here' {x} : T x -> any (one x)
| ll {s t} : any s -> any (plus s t)
| rr {s t} : any t -> any (plus s t).
Arguments any {A} T t.
Derive NoConfusion for any.

Equations here'_inj {A T x t u} : @here' A T x t = here' u -> t = u :=
| eq_refl => eq_refl.

Error:
[noConfusion] Cannot simplify without UIP on type
(tree A) or NoConfusion for family any

Kenji Maillard (May 18 2022 at 16:36):

You need the homogeneous NoConfusion principle here: Derive Signature NoConfusionHom for any.

James Wood (May 18 2022 at 16:38):

Thanks! Is the documentation clear on why that is?

James Wood (May 18 2022 at 16:42):

And incidentally, is there anything that derives all these injectivity lemmas for me?

Kenji Maillard (May 18 2022 at 16:46):

I think that the content of the derived NoConfusion(Hom) record is essentially what you are asking for (but in packed form). The documentation isn't ideal on that point (or at least I don't fully understand it).

Notification Bot (May 18 2022 at 16:46):

James Wood has marked this topic as resolved.

Last updated: Sep 25 2023 at 14:01 UTC