Hi! Is there a way to use
noconf to simplify an equality goal? Since
NoConfusionPackage contains both direction, it seems we could do the symmetric of what
noconf currently does right?
Yes, I think it's actually easily programmable, by looking up the NoConfusionPackage and applying the right lemma
But not in Ltac right?
repeat eapply noConfusion doesn't seem to be the best one can do.
I suppose you have
C x x' = C y y' in your goal and want to simplify to
(x, x') = (y, y') and then maybe two subgoals
x = y and
x' = y'? You will need to also try to apply the lemma about equality in sigma-types inbetween
apply noConfusion calls.
Yeah I expect to have a goal which is an equality between two elements of an inductive type (which I know) and would like to simplify it to equality between the different bits.
I was wondering if there was a general approach, I'll try something specialised I guess. Thanks.
Last updated: Jun 10 2023 at 23:01 UTC