Zulip Chat Archive

Stream: new members

Topic: Unable to unfold


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

Mario Carneiro (Nov 02 2018 at 04:28):

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

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

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

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?

Mario Carneiro (Nov 02 2018 at 04:33):

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

Mario Carneiro (Nov 02 2018 at 04:34):

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

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

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

AHan (Nov 02 2018 at 04:37):

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

AHan (Nov 02 2018 at 05:25):

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


Last updated: Dec 20 2023 at 11:08 UTC