incorrect def/lemma

Stream: general

[Floris van Doorn]

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

https://gist.github.com/fpvandoorn/bdc82881ba8e6461460e8028c291162f

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]

Kenny once found some applications of simp in mathlib which could be changed to rfl

[Kevin Buzzard]

But that might be asking too much

[Rob Lewis]

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]

(Note, this definition of size has very little correlation to compile time, partly because it ignores auxiliary declarations.)

[Rob Lewis]

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]

(deleted)

[Mario Carneiro]

It's surprising that yoneda_lemma achieves both the #2 and #3 positions on this list, considering the size of the proof script. Perhaps the obviously isn't obvious after all?

[Kevin Buzzard]

It's obvious to mathematicians :P

[Sebastien Gouezel]

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]

I would say olympic champion for refusing to split off lemmas.

[Sebastien Gouezel]

I jus had a look at the proof, it is not that bad (150 lines, no obvious lemma to split off).

[Rob Lewis]

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]

Oh, duh. category_theory.yoneda._proof_4 isn't category_theory.yoneda_lemma._proof_4. That one's bigger (but still loads okay).

[Scott Morrison]

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]

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]

@Floris van Doorn Thanks for building these lists! They are useful reminders of maintenance work that we shouldn't forget about.

[Scott Morrison]

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]

Good catch!