Zulip Chat Archive

Stream: new members

Topic: Unable to unfold


view this post on Zulip AHan (Nov 02 2018 at 04:24):

I'm trying to prove the prime field addition that I defined is correct, but somehow I can't unfold the equation...
https://gist.github.com/potsrevennil/0cbf2204a8a16daa6eab367f153be748#file-primefield-lean-L71

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:28):

from your definitions it looks like the proof is just eq.symm (add_equiv _)

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:31):

if you want to get at this by unfolding, you should dsimp [pf.add, (+)], although this might unfold too much

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:32):

normally we would state a simp lemma expressing the definitional unfolding here, exactly because it's hard to get at unless you say it explicitly

view this post on Zulip AHan (Nov 02 2018 at 04:32):

what's dism's usage?
And why is that I can unfold eq in add_equiv but not of_int_add?

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:33):

because of_int_add does not have the form of_int ... = of_int ...

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:34):

you have to unfold the addition on the lhs first, then you can unfold eq

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:34):

dsimp and unfold are very similar, they are implemented as the same tactic behind the scenes with different configuration options

view this post on Zulip Mario Carneiro (Nov 02 2018 at 04:35):

in this case it's just because dsimp accepts operators like (+) for simplifying and unfold doesn't

view this post on Zulip AHan (Nov 02 2018 at 04:37):

oh yes I should unfold addition first!
But after unfold add, I still cannot unfold eq....

view this post on Zulip AHan (Nov 02 2018 at 05:25):

Anyway eq.symm (add_equiv _) is really a nice solution, thanks a lot!


Last updated: May 17 2021 at 22:15 UTC