Zulip Chat Archive
Stream: general
Topic: popular tactics
Neil Strickland (Mar 01 2019 at 19:45):
A little while ago, there was some discussion about the large number of available tactics, and how to document them. To inform that discussion, the following page might be interesting: http://bim.shef.ac.uk/lean/tactic_count.html. It shows the number of times various tactics are used in mathlib, starting as follows:
| Tactic | Count |
|---|---|
| simp | 10254 |
| rw | 5355 |
| exact | 3936 |
| assume | 3284 |
| have | 3047 |
| from | 1851 |
| cases | 1727 |
| let | 1558 |
| apply | 1510 |
| refl | 1499 |
| refine | 1107 |
| ext | 1014 |
Johan Commelin (Mar 01 2019 at 19:52):
Cool! I'm actually somewhat surprised. simp is used almost twice as often as nr.2 and I would also have expected that apply would win from cases... interesting statistics!
Neil Strickland (Mar 01 2019 at 20:07):
Actually, I think that the regexp (which is just "\bsimp\b") is allowing @[simp] as an instance of simp, so the first entry is misleading. That must inflate the count for ext as well, but probably not too many other things.
Kevin Buzzard (Mar 01 2019 at 20:08):
I think that mathlib style implies that any simp will have a space before it. If you're in the middle of a proof in tactic mode then I think you must be indented, and if you're in term mode then it would be by simp or whatever.
Kevin Buzzard (Mar 01 2019 at 20:09):
meh, {simp } is probably OK too
Johan Commelin (Mar 01 2019 at 20:12):
git grep " simp " | wc -l 4774
Neil Strickland (Mar 01 2019 at 20:13):
The count for " simp\b" (with a space) is 5944. I am using grep -RIoh (regexp) src | wc -l.
Scott Morrison (Mar 01 2019 at 22:23):
It's also important to note that regex's will not notice any auto_param tactics!
Chris Hughes (Mar 01 2019 at 22:25):
I'm surprised by the ext count, and the refl count. Is this picking up lemmas with these words in the name?
Last updated: Dec 20 2023 at 11:08 UTC