Tactic uses in mathlib

Stream: mathlib4

[Kenny Lau]

I wrote a script to count the number of tactic uses in Mathlib.

Script:

# Put me in a folder inside mathlib.
# Hard-coded tactic list in tactics.txt generated with:
"""
import Mathlib

#help tactic
"""

import re
import os
import sys

tacticRegex = "(?<= )[a-zA-Z0-9_]+['!?₁₂]*(?= |\n)"

tactics = dict()
with open("tactics.txt", "r", encoding="UTF-8") as auto:
    for line in auto.read().split("\n"):
        tactics[line] = 0

def process(filename, file):
    for potential in re.findall(tacticRegex, file):
        if potential in tactics:
            tactics[potential] += 1

fileCount = 0
for root, dirs, files in os.walk('../Mathlib'):
    for file in files:
        filename = os.path.join(root, file)
        with open(filename, "r", encoding="UTF-8") as auto:
            fileCount += 1
            if fileCount % 100 == 0:
                sys.stdout.write("\r%d files processed."%fileCount)
                sys.stdout.flush()
            process(filename, auto.read())

print("\r%d files processed." % fileCount)
print("Number of recognised tactics: %d"%len(tactics.keys()))
print("%d tactic calls processed." % sum(tactics[i] for i in tactics))
print()

keys = sorted(tactics.keys(), key=lambda i:tactics[i], reverse=True)
for t in keys:
    print("%d: %s"%(tactics[t],t))

[Kenny Lau]

Full output:

6616 files processed.
Number of recognised tactics: 475
511237 tactic calls processed.

73107: rw
57481: simp
46826: exact
33592: have
30528: rfl
20869: refine
17766: apply
16243: let
13406: obtain
13133: simpa
12929: intro
10718: ext
7851: set
7847: rintro
7839: rcases
7377: simp_rw
5124: dsimp
4976: use
4719: cases
4340: ring
4334: rwa
4186: by_cases
3817: convert
3758: else
3553: induction
3511: constructor
3291: show
3015: suffices
2946: group
2781: calc
2697: congr
2688: change
2598: left
2574: classical
2398: order
2368: right
2313: haveI
2126: case
2090: lift
2045: infer_instance
2031: letI
2000: open
1862: match
1646: filter_upwards
1632: replace
1597: first
1364: funext
1322: exists
1311: module
1254: split_ifs
1181: subst
1073: aesop
1026: gcongr
938: unfold
934: trivial
872: assumption
858: choose
847: simp_all
817: contrapose!
816: bound
811: erw
787: ext1
786: intros
766: omega
757: monoidal
736: aesop_cat
680: linarith
653: symm
645: induction'
631: norm_cast
589: exacts
577: swap
575: positivity
553: by_contra
553: specialize
547: trans
536: norm_num
499: all_goals
493: conv_rhs
466: split
457: try
447: field_simp
444: find
438: conv_lhs
393: says
389: clear
387: nth_rw
382: fun_prop
364: tauto
348: trace
342: continuity
332: abel
331: next
327: tfae_have
326: decide
325: conv
320: revert
319: absurd
314: delta
311: by_contra!
308: contradiction
296: generalize
293: push_neg
285: nontriviality
284: slice_lhs
279: linear_combination
266: apply_fun
262: congr!
254: push_cast
226: rewrite
216: injection
215: wlog
214: forward
204: ring_nf
203: mono
196: fin_cases
196: ring1
194: bicategory
193: exact_mod_cast
181: subsingleton
177: reduce
160: done
156: slice_rhs
144: repeat
139: rel
132: exfalso
129: iterate
125: hint
124: introv
116: grind
114: rename
112: simp?
110: finiteness
106: on_goal
101: choose!
101: measurability
92: inhabit
92: valid
91: fapply
90: nth_rewrite
87: borelize
85: apply_rules
82: solve
80: elementwise
78: fail
75: nlinarith
74: contrapose
70: tfae_finish
68: convert_to
64: sorry
63: ac_rfl
62: rotate_left
61: algebraize
60: rename_i
58: skip
56: clear_value
55: coherence
55: repeat'
52: solve_by_elim
51: any_goals
50: fconstructor
50: subst_vars
45: rsuffices
44: generalize_proofs
43: congrm
42: whnf
41: unreachable!
39: norm_num1
38: simp!
36: mfld_set_tac
35: transitivity
34: substs
33: nofun
33: peel
33: rw_mod_cast
31: admit
30: stop
29: set_option
27: match_scalars
26: clear!
25: cc
25: focus
24: abel_nf
24: monoidal_coherence
24: recover
24: zify
23: assumption_mod_cast
21: with_unfolding_all
20: refine'
20: with_reducible_and_instances
19: clean
19: subst_hom_lift
18: injections
18: with_reducible
17: dbg_trace
16: frac_tac
14: interval_cases
14: try?
13: beta_reduce
13: rcongr
12: noncomm_ring
12: qify
11: casesm
11: nomatch
11: pick_goal
10: case'
10: existsi
10: unfold_projs
10: unit_interval
9: algebraize_only
9: compute_degree
9: compute_degree!
9: ghost_fun_tac
9: ghost_simp
9: init_ring
9: map_fun_tac
9: polyrith
9: rify
9: try_this
8: apply_assumption
8: assumption'
8: ghost_calc
8: isBoundedDefault
8: itauto
8: linear_combination'
8: observe
8: tauto_set
7: aesop?
7: fin_omega
7: move_mul
7: pgame_wf_tac
7: ring!
7: witt_truncateFun_tac
6: bicategory_coherence
6: cases'
6: extract_goal
6: guard_hyp
5: abel1
5: decreasing_tactic
5: grewrite
5: grw
5: pi_lower_bound
5: pi_upper_bound
5: simp_wf
5: simpa?
5: smul_tac
5: to_encard_tac
5: triv
5: use!
4: apply_mod_cast
4: decreasing_trivial
4: reduce_mod_char
3: aesop_graph
3: arith_mult
3: as_aux_lemma
3: cancel_denoms
3: compareOfLessAndEq_rfl
3: fail_if_success
3: infer_param
3: mem_tac_aux
3: move_add
3: mv_bisim
3: plausible
3: refold_let
3: rename'
3: split_ands
3: unfold_let
2: abel1!
2: ac_change
2: and_intros
2: aux_group₂
2: bitwise_assoc_tac
2: cfc_tac
2: discrete_cases
2: eta_expand
2: fail_if_no_progress
2: get_elem_tactic
2: itauto!
2: mem_tac
2: monoidal_simps
2: move_oper
2: pure_coherence
2: refine_lift
2: rename_bvar
2: rfl_cat
2: ring1!
2: ring_nf!
2: run_tac
2: set!
2: simp_all!
2: simp_intro
2: sorry_if_sorry
2: whisker_simps
1: aesop_cat?
1: aesop_mat
1: apply_gmonoid_gnpowRec_succ_tac
1: apply_gmonoid_gnpowRec_zero_tac
1: aux_group₁
1: cases_type
1: change?
1: check_compositions
1: clear_aux_decl
1: constructorm
1: conv'
1: exact?
1: fun_induction
1: have'
1: have?
1: lift_lets
1: mod_cases
1: norm_cast0
1: reduce_mod_char!
1: repeat1
1: restrict_tac
1: ring1_nf
1: rotate_right
1: show_term
1: simp_all?
1: simpa!
1: sleep
1: sleep_heartbeats
1: specialize_all
1: success_if_fail_with_msg
1: swap_var
1: use_finite_instance
0: abel!
0: abel_nf!
0: ac_nf
0: ac_nf0
0: aesop_cat_nonterminal
0: aesop_graph?
0: aesop_graph_nonterminal
0: aesop_unfold
0: apply?
0: apply_ext_theorem
0: apply_rewrite
0: apply_rfl
0: apply_rw
0: arith_mult?
0: array_get_dec
0: array_mem_dec
0: attempt_all
0: bddDefault
0: bicategory_nf
0: bv_check
0: bv_decide
0: bv_decide?
0: bv_normalize
0: bv_omega
0: calc?
0: cases_first_enat
0: cases_type!
0: casesm!
0: cfc_cont_tac
0: cfc_zero_tac
0: clean_wf
0: clear_
0: congrm?
0: continuity?
0: conv?
0: count_heartbeats
0: decreasing_trivial_pre_omega
0: decreasing_with
0: dsimp!
0: dsimp?
0: dsimp?!
0: eapply
0: econstructor
0: elementwise!
0: enat_to_nat
0: eq_refl
0: erw?
0: eta_reduce
0: eta_struct
0: expose_names
0: extract_lets
0: false_or_by_contra
0: field_simp_discharge
0: finiteness?
0: finiteness_nonterminal
0: forward?
0: fun_cases
0: gcongr?
0: gcongr_discharger
0: generalize'
0: get_elem_tactic_extensible
0: get_elem_tactic_trivial
0: grind?
0: guard_expr
0: guard_goal_nums
0: guard_hyp_nums
0: guard_target
0: have!?
0: have?!
0: let'
0: let_to_have
0: liftable_prefixes
0: linarith!
0: linear_combination2
0: map_tacs
0: massumption
0: match_target
0: mcases
0: mclear
0: mconstructor
0: mdup
0: measurability!
0: measurability!?
0: measurability?
0: mexact
0: mexfalso
0: mexists
0: mframe
0: mhave
0: mintro
0: mleft
0: monicity
0: monicity!
0: monoidal_nf
0: mpure
0: mpure_intro
0: mrefine
0: mreplace
0: mrevert
0: mright
0: mspec
0: mspec_no_bind
0: mspec_no_simp
0: mspecialize
0: mspecialize_pure
0: mstart
0: mstop
0: mvcgen
0: mvcgen_no_trivial
0: mvcgen_step
0: native_decide
0: nlinarith!
0: nth_grewrite
0: nth_grw
0: observe?
0: pnat_positivity
0: pnat_to_nat
0: refine_lift'
0: repeat1'
0: restrict_tac?
0: rfl'
0: ring1_nf!
0: rw?
0: rw??
0: rw_search
0: saturate
0: saturate?
0: simp?!
0: simp_all?!
0: simp_all_arith
0: simp_all_arith!
0: simp_arith
0: simp_arith!
0: simpa?!
0: sizeOf_list_dec
0: squeeze_scope
0: subst_eqs
0: suggest_premises
0: symm_saturate
0: toFinite_tac
0: trace_state
0: try_suggestions
0: type_check
0: unfold?
0: unhygienic
0: uniqueDiffWithinAt_Ici_Iic_univ
0: use_discharger
0: volume_tac
0: wait_for_unblock_async
0: with_panel_widgets

[Kenny Lau]

First 30:

73107: rw
57481: simp
46826: exact
33592: have
30528: rfl
20869: refine
17766: apply
16243: let
13406: obtain
13133: simpa
12929: intro
10718: ext
7851: set
7847: rintro
7839: rcases
7377: simp_rw
5124: dsimp
4976: use
4719: cases
4340: ring
4334: rwa
4186: by_cases
3817: convert
3758: else
3553: induction
3511: constructor
3291: show
3015: suffices
2946: group
2781: calc

[Edward van de Meent]

there's a use of sleep in mathlib??

[Edward van de Meent]

or are you including tests or something?

[Jireh Loreaux]

Are we really still using continuity that much?! We need to fix that.

[Kenny Lau]

Edward van de Meent said:

or are you including tests or something?

I included all files in Mathlib

[Ruben Van de Velde]

I'm pretty sure there's no 31 admits in Mathlib itself

[Aaron Liu]

test files?

[Edward van de Meent]

also, how is there more else than if?

[Aaron Liu]

I'm grepping for sleep

[Edward van de Meent]

Q:
Edward van de Meent said:

also, how is there more else than if?

A: because there's no if tactic

[Aaron Liu]

is there an else tactic???

[Aaron Liu]

I thought there is an if-then-else tactic

[Kenny Lau]

it's not a very rigid script, i just searched for the words surrounded by spaces :upside_down:

[Edward van de Meent]

Aaron Liu said:

I thought there is an if-then-else tactic

yea, i think that's sorta the point... it's just that the #help tactic command shows its name as else

[Damiano Testa]

If you inspect the output of #help tactic, you may instead grep for the actual names of the tactics. This will not be as precise as using some metaprogramming, but will probably be pretty close.

[Aaron Liu]

Kenny Lau said:

it's not a very rigid script, i just searched for the words surrounded by spaces :upside_down:

I though you were at least using Lean to do it, but I scroll up to the top of this thread and I see python

[Damiano Testa]

I think that the deprecatedSyntax linter already extracts (most?) SyntaxNodeKinds from every syntax node. If you make that linter print it out, then you can grep the output and you'll get very precise information on tactic use.

[Damiano Testa]

Figuring out what tactics are used is (very slightly) tricky, since they usually do not leave an explicit mark in the declaration that makes it to makes it to the environment, this is why using a linter is useful: it sees the syntax trees of (almost) all the commands in every file.

[Kevin Buzzard]

@Kenny Lau you can do this in lean and get a more accurate answer. Right now you're counting comments etc

[Jireh Loreaux]

Yes, this probably explains the "continuity". I bet there are many false positives there.

[Alex Meiburg]

That regex would also fail to recognize e.g. rw[h] or simp+decide, or the simp in first |simp | trivial, or the positivity in exact someThm (by positivity), or the volume_tac in (h : ... := by volume_tac). All five are valid Lean, but I think probably only the last two are stylistically permissible within Mathlib...

[Robin Carlier]

Am I correct when guessing that this does count autoparams? Pretty sure the category theory library would make aesop_cat one of the first tactic if autoparams were accounted for.

[Damiano Testa]

To find out about autoparams, you would probably have to traverse the InfoTrees. Maybe having a global statistic of SyntaxNodeKinds across mathlib would be interesting.

[Filippo A. E. Nuccio]

Jireh Loreaux said:

Yes, this probably explains the "continuity". I bet there are many false positives there.

#27035