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.
Thanks! Is the documentation clear on why that is?
And incidentally, is there anything that derives all these injectivity lemmas for me?
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).
James Wood has marked this topic as resolved.
Last updated: Sep 25 2023 at 14:01 UTC