mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

When do we introduce simp?

Open PatrickMassot opened this issue 4 years ago • 1 comments

From Zulip:

Another general remark about my tutorials: I never tell my students about simp. That would be too powerful, and it would encourage them to try simp every other line instead of thinking.

Note that I do introduce ring and linarith very early. There are much better than simp because students are not too tempted to try them on each and every goal (although linarith is a bit too powerful here, especially when it comes to find contradiction, so I delay its introduction some more).

Anyway, we need to decide when we introduce simp.

PatrickMassot avatar Apr 28 '20 17:04 PatrickMassot

It is now mentioned briefly in Logic, and we start to use it more substantially in Sets, Functions, and Relations. We don't give a detailed discussion or exhaustive overview, but, rather, show a few common usages.

At some point, we should re-evaluate, decide whether to be more systematic, decide what more to say about simp, and decide where to say it.

avigad avatar Jul 09 '20 01:07 avigad