Topic: incorrect def/lemma
Floris van Doorn (Aug 13 2019 at 03:37):
In the latest installment of my
#sanity_check command, here is a list of all declarations in mathlib that either
- are a lemma/theorem but construct data
- are a definition, but define an element of a proposition
Maybe some of them are intended to be like this, but most of them should be changed.
The ultimate goal of the
#sanity_check command is that you put it at the bottom of your file while working on it, and it will give you warnings for things you're probably doing wrong. What other (realistic) features would you like it to detect?
Kevin Buzzard (Aug 13 2019 at 07:12):
Kenny once found some applications of
simp in mathlib which could be changed to
Kevin Buzzard (Aug 13 2019 at 07:12):
But that might be asking too much
Rob Lewis (Aug 13 2019 at 08:17):
I was wondering if we could use this to flag particularly large or slow proofs. Quiz: if we define
meta def expr.size (e : expr) : ℕ := e.fold 0 $ λ _ _, nat.succ, what do you think is biggest declaration in mathlib? No cheating.
Rob Lewis (Aug 13 2019 at 08:19):
(Note, this definition of size has very little correlation to compile time, partly because it ignores auxiliary declarations.)
Rob Lewis (Aug 13 2019 at 08:56):
Here are the top 50. The average is 337.
(81923, Gromov_Hausdorff.totally_bounded) (51474, category_theory.yoneda_lemma._proof_4) (51307, category_theory.yoneda_lemma._proof_5) (45050, filter.is_lawful_monad) (44764, emetric.countable_closure_of_compact) (39488, dense_Inter_of_open_nat) (38767, is_integral_of_mem_of_fg) (38442, category_theory.whiskering_left._proof_13) (36064, category_theory.adjunction.cocones_iso._proof_5) (35121, _private.51918499.mul_le_of_limit_aux) (32774, category_theory.whiskering_right._proof_13) (32371, category_theory.category_of_elements._proof_5) (30707, category_theory.whiskering_right._proof_12) (30515, category_theory.adjunction.cones_iso._proof_5) (29441, measure_theory.simple_func_sequence_tendsto) (28014, real.exists_sup) (27209, category_theory.uncurry._proof_9) (26970, category_theory.category_of_elements.to_comma._proof_7) (26028, set.is_lawful_monad) (25754, ring.direct_limit.of.zero_exact_aux) (25726, is_noetherian_pi) (25578, ordinal.add_le_of_limit) (24060, nat.partrec.code.evaln_complete) (24005, Gromov_Hausdorff.second_countable) (23577, category_theory.uncurry._proof_7) (23420, category_theory.whiskering_right._proof_11) (23065, exists_preimage_norm_le) (22119, bounded_continuous_function.arzela_ascoli₁) (22105, hash_map.mem_insert) (21108, free_group.is_lawful_monad) (21004, real.pi_gt_314) (20566, turing.TM2to1.tr_respects_aux₂) (20254, turing.TM2to1.tr_supports) (19701, category_theory.lax_monoidal_functor.mk.inj_eq) (19439, nat.partrec.code.evaln_prim) (19291, category_theory.uncurry._proof_8) (19029, nat.partrec.code.evaln_sound) (18929, writer_t.is_lawful_monad) (18766, category_theory.adjunction.functoriality_is_right_adjoint._proof_5) (18704, real.pi_lt_315) (18639, onote.repr_power_aux₂) (18530, category_theory.adjunction.functoriality_is_left_adjoint._proof_5) (18514, category_theory.adjunction.functoriality_is_left_adjoint._proof_6) (18498, category_theory.adjunction.functoriality_is_right_adjoint._proof_6) (18435, exists_of_linear_independent_of_finite_span) (17418, semiquot.is_lawful_monad) (17392, category_theory.whiskering_left._proof_12) (17372, except_t.is_lawful_monad) (17075, turing.TM1to1.tr_supports) (17057, category_theory.adjunction.cocones_iso._proof_3)
Chris Hughes (Aug 13 2019 at 12:15):
Mario Carneiro (Aug 13 2019 at 16:12):
Kevin Buzzard (Aug 13 2019 at 16:13):
It's obvious to mathematicians :P
Sebastien Gouezel (Aug 13 2019 at 16:21):
I see that
Gromov_Hausdorff.totally_bounded comes first. Since I wrote it, does it make me an olympic champion for writing such a big proof, or an olympic loser for being unable to write optimized proofs?
Patrick Massot (Aug 13 2019 at 16:24):
I would say olympic champion for refusing to split off lemmas.
Sebastien Gouezel (Aug 13 2019 at 16:31):
I jus had a look at the proof, it is not that bad (150 lines, no obvious lemma to split off).
Rob Lewis (Aug 13 2019 at 17:10):
It's funny. Printing the long proofs from
tidy isn't so bad, even with
pp.all. In contrast,
Gromov_Hausdorff.totally_bounded locks up VS Code for me. Where is the complexity in
yoneda coming from?
import category_theory.yoneda topology.metric_space.gromov_hausdorff set_option pp.all true #print category_theory.yoneda._proof_4
Rob Lewis (Aug 13 2019 at 17:27):
category_theory.yoneda_lemma._proof_4. That one's bigger (but still loads okay).
Scott Morrison (Aug 13 2019 at 22:41):
I'll try to have a look sometime. I suspect all the category theory lemmas appearing here is just a consequence of the category theory library actually using dependent types all over, and hence expressions tend to have huge invisible implicit arguments, often repeated many times over. I bet if we could measure the "weight" of an expression deduplicating repeated subexpressions these lemmas would fall down the list somewhat.
Scott Morrison (Aug 15 2019 at 08:46):
Could sanity check even check for duplicate definitions? That is, find a definition in this file which is definitionally equal to some imported definition?
Johan Commelin (Aug 24 2019 at 15:11):
@Floris van Doorn Thanks for building these lists! They are useful reminders of maintenance work that we shouldn't forget about.
Scott Morrison (Sep 03 2019 at 00:27):
All of the "defs that should be lemmas" in the category theory library were being created by
restate_axiom. I've updated this to create lemmas when appropriate, in #1390.
Kevin Buzzard (Sep 03 2019 at 10:10):
Last updated: May 13 2021 at 21:12 UTC