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