Stream: new members
Topic: Usage of simplifier
AHan (Nov 02 2018 at 08:02):
Although having read the simplifier in the tutorial: Theorem Proving in Lean and the The Lean Reference Manual
I'm still not quite understand when to use simplifier and why or why can't simp succeed in some cases,
Take a self-defined prime field for an example, when I'm trying to prove the well-definedness of the addition of the field,. Since in the line 60 and 61, it's kind of redundant, I'm thinking of using simplifier to simplify the code. Anyway I couldn't succeed...
Johan Commelin (Nov 02 2018 at 08:17):
@AHan This is not answering your question, but why do you include
% p in your definition of addition. If would just use
of_int (m + n). It will make a lot of proofs that come afterwards a lot easier.
AHan (Nov 02 2018 at 08:27):
oh yeah! You're right!
I didn't notice this since I defined the addition before the equivalence....
AHan (Nov 02 2018 at 08:31):
@Johan Commelin It did simplify a lot ! Totally get rid of the redundant part that I mentioned! (Though still confuse about the usage of simplifier) Thank you very much!!
Last updated: May 14 2021 at 03:27 UTC