Zulip Chat Archive

Stream: general

Topic: incorrect def/lemma

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 13 2019 at 07:12):

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

view this post on Zulip Kevin Buzzard (Aug 13 2019 at 07:12):

But that might be asking too much

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Aug 13 2019 at 12:15):


view this post on Zulip Mario Carneiro (Aug 13 2019 at 16:12):

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?

view this post on Zulip Kevin Buzzard (Aug 13 2019 at 16:13):

It's obvious to mathematicians :P

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 13 2019 at 16:24):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Rob Lewis (Aug 13 2019 at 17:27):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 03 2019 at 10:10):

Good catch!

Last updated: May 13 2021 at 21:12 UTC