Théo Winterhalter (Apr 20 2021 at 13:06): Théo Winterhalter (Apr 20 2021 at 13:06):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?
Matthieu Sozeau (Apr 20 2021 at 16:23):Yes, I think it's actually easily programmable, by looking up the NoConfusionPackage and applying the right lemma
Théo Winterhalter (Apr 20 2021 at 17:13):But not in Ltac right? repeat eapply noConfusion doesn't seem to be the best one can do.
Matthieu Sozeau (Apr 20 2021 at 18:55):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.
Théo Winterhalter (Apr 20 2021 at 18:58):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: Jan 29 2023 at 15:02 UTC