Stream: Equations devs & users

Topic: `noconf` in goal


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jun 10 2023 at 23:01 UTC