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

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