James Wood (May 18 2022 at 16:29): 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
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: May 28 2023 at 20:30 UTC