An example of why formalization is useful

Stream: general

[Riccardo Brasca]

I really like what is going on with #12777. @Sebastian Monnet proved that if E,F and K are fields such that finite_dimensional F E, then fintype (E →ₐ[F] K). We already have docs#field.alg_hom.fintype, that is exactly the same statement with the additional assumption is_separable F E.

The interesting part of the PR is that, with the new theorem, the linter will automatically flag all the theorem that can be generalized (for free!), removing the separability assumption. I think in normal math this is very difficult to achieve, if I generalize a 50 years old paper that assumes p ≠ 2 to all primes, there is no way I can manually check and maybe generalize all the papers that use the old one.

[Riccardo Brasca]

OK, of course right after I write this, Lean decided that something is wrong and didn't accept the new result, but still, the story is in principle interesting...

[Damiano Testa]

I completely agree with you! Automated reduction of assumptions is great!

In a similar vein, I was very impressed with I changed the definition of ideal to use comm_semiring instead of comm_ring and then noticing that essentially the only proofs that failed were the ones that explicitly involved using -!

[Sebastien Gouezel]

This happened to me a lot with the Bochner integral refactor, in which I removed a second_countable_topology assumption. Then I had to go through a bunch of linting steps, where the linter complained that I had useless assumptions in a bunch of files that do not directly depend on integration theory (notably many results in complex analysis).

[Scott Morrison]

Whatever happened to the optional linter (I think written by @Alex J. Best?) that tried to determine if a type class assumption was too strong (not just unnecessary)? It was far too slow to put into the automatic linting step, but it would be lovely to have it run once a day and put the output somewhere easily accessible.

[Scott Morrison]

ah, I found some messages with Alex, and what you're meant to be able to do is (in mathlib):

leanpkg add https://github.com/alexjbest/lean-generalisation

then add import generalisation_linter in a file, and then run #lint as normally.

Right now this fails with cannot find revision lean-3.42.0 in repository _target/deps/lean-generalisation at the leanpkg add step.

[Scott Morrison]

Alex's talk about the generalisation linter is at https://www.youtube.com/watch?v=pudd4F749tE.

[Eric Rodriguez]

i tried bumping at https://github.com/ericrbg/lean-generalisation, and trying to run it overnight on my laptop on mathlib. will report back what it finds!

[Scott Morrison]

I ran it just up to import algebra.group.basic. There are essentially four classes of suggestions:

• broken ones that include no_meet_fake_name in the output
• suggestions that might well be okay, but I'm not interested in: #check @comp_mul_right /- _inst_1: semigroup ↝ has_mul is_associative -/
• some that are "obviously silly": `#check @group.to_monoid /- _inst_1: group ↝ monoid -/
• and some good ones!

The first three classes are pretty easy to filter out. To ignore a superset of the second class, we can just filter out everything that suggests replacing one typeclass with multiple typeclasses. (They may well be valid, but I probably less valuable.) The third class would require a filter that declines suggestions that weaken a typeclass if the declaration is in the namespace.

The remaining suggestions up to algebra.group.basic I've implemented as #13092; we'll see what CI says.

[Scott Morrison]

Okay, this is kind of fun. :-) Many of the suggestions up to (an arbitrarily chosen target) algebra.ring.pi are in #13094, #13095, #13096, #13097, #13098, #13099.

[Eric Rodriguez]

meanwhile, the version running on mk_all still hasn't finished... mypoor macbook :)

[Eric Rodriguez]

worryingly, it also throws some errors of the form:

WARNING types not equal
<def algebraic_geometry.Scheme.open_cover.finite_subcover : Π {X : algebraic_geometry.Scheme},
  X.open_cover →
  Π [H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)], X.open_cover := λ
{X : algebraic_geometry.Scheme} (𝒰 : X.open_cover)
[H : compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)],
  let t : finset ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) := _.some
  in {J := ↥t,
      obj := λ (x : ↥t), 𝒰.obj (𝒰.f x.val),
      map := λ (x : ↥t), 𝒰.map (𝒰.f x.val),
      f := λ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), Exists.some _,
      covers := _,
      is_open := _}>
WARNING types not equal
<def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom : Π {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f],
  algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace Y f ⟶ Y := λ {C : Type u}
[_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_products C]
{X : algebraic_geometry.PresheafedSpace C} (Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y.to_PresheafedSpace)
[H : algebraic_geometry.PresheafedSpace.is_open_immersion f], f>

not sure how this happens

[Yaël Dillies]

Just noting that we have branch#generalising_typeclasses

[Oliver Nash]

Thanks @Yaël Dillies Is anyone brave enough to merge master into a branch 2752 commits behind?

[Yaël Dillies]

I already did but then let the branch rot again :upside_down:

[Scott Morrison]

Ah, nice, after following the generalisation linters hints for a while, I realised it was going to be possible to generalise module to work over a non_assoc_semiring. This is now in #13111.

[Scott Morrison]

I wonder if we can bring lie_module back into the fold. :-)

[Eric Wieser]

I think I decided not to make that generalization at the time because it didn't actually have any obvious instances

[Eric Wieser]

In particular, a non associative ring can't be a module over itself, because mul_smul is just associativity

[Eric Wieser]

In fact, I think mul_smul implies the action behaves as if the ring were associative

[Eric Rodriguez]

are you saying this is the same as docs#monoid.exponent in that any module ends up automatically implying associativity?

[Yaël Dillies]

I will update generalising_typeclasses once you are done with all this, Scott.

[Eric Wieser]

It's not quite as strong as implying associativity

[Eric Wieser]

Just that the action factors via an embedding into something associative

[Eric Wieser]

((a * b) * c) • x = (a * (b * c)) • x is implied by the module axioms

[Eric Rodriguez]

not sure how quotients work in non-assoc rings, but can you make a module of R into its "associtivisation"?

[Reid Barton]

This example or a related one was discussed here some time ago

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20on.20module/near/267627989

[Scott Morrison]

Yeah, okay, I think I won't bother with that PR. :-)

[Scott Morrison]

I guess it is actually non_unital_ring that we may want modules for, for C^*-algebra purposes...?

[Eric Rodriguez]

i still don't know why we didn't call those rngs... we're going to need 4k screens to fit Lean text soon

[Yaël Dillies]

random_number_generator?

[Eric Rodriguez]

ring without the identity

[Eric Rodriguez]

if you mean it'd get confused with that, it seems to already be called docs#rand_g

[Scott Morrison]

and rig for semiring (ring without negative), and presumably rgs for the silliest ones?

[Yaël Dillies]

A name without vowels is likely to be read as an abbreviation.

[Eric Rodriguez]

These are common names

[Moritz Doll]

Is it possible to run the generalization linter alone? #lint dies on many files on my machine.

[Eric Rodriguez]

just type generalization_linter

[Eric Rodriguez]

after #lint

[Eric Rodriguez]

but it's really expensive it's still running on my laptop since ~yday 10GMT

[Moritz Doll]

thanks, unfortunately it still times out..

[Riccardo Brasca]

Is it possible to run it from the command line?

[Riccardo Brasca]

And not in VS Code

[Floris van Doorn]

You need to type #lint only generalization_linter if you don't want to do the default tests.

[Eric Rodriguez]

oh dear, my poor CPU cycles are probably re-running simp-nf...

[Eric Rodriguez]

still running, albeit single-threaded so hopefully it's nearly done... how long did it take to run the first time?

[Scott Morrison]

I'm not sure it's ever been run on the entire library! :-)

[Eric Rodriguez]

OK, I've tried now twice and it just outputs errors and never any suggestions :/ maybe this is a memory issue though, so I guess these results are going to have to wait.

https://gist.github.com/ericrbg/e78cd06e2930763a07fd2f22c14a67d0

[Riccardo Brasca]

If someone is ready to explain me how to do it I have some cpu time (and memory) to spare

[Eric Rodriguez]

1. Take a mathlib clone with cache
2. leanpkg add https://github.com/ericrbg/lean-generalisation
3. mk_all.sh to get an all.lean
4. Make a file that imports all and generalisation_linter, and under all that put #lint only generalisation_linter
5. lean --make that file into some output file

If this works as I think it should, piping from that file should give you the output. It's likely worth trying step 4 with logic.basic instead of all first to check things are working as they should

[Riccardo Brasca]

import all
import generalisation_linter

#lint only generalisation_linter

and lean --make src/test_linter.lean > res gives

/- Checking 0 declarations (plus 0 automatically generated ones) in the current file with 1 linters -/


/- All linting checks passed! -/

:rolling_eyes:

[Floris van Doorn]

You'll want #lint_mathlib only generalisation_linter or #lint_all only generalisation_linter

[Eric Rodriguez]

oopsies, yes, wrong lint command!

[Riccardo Brasca]

Ah yes, with logic.basic it does something

[Riccardo Brasca]

For future reference: one has to redirect stderr to obtain a file with the result

[Riccardo Brasca]

It is of course still working, but the first output is

WARNING types not equal
<def category_theory.nat_trans.right_derived : Π {C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1}
[_inst_2 : category_theory.category D] [_inst_3 : category_theory.abelian C]
[_inst_4 : category_theory.has_injective_resolutions C] [_inst_5 : category_theory.abelian D] {F G : C ⥤ D}
[_inst_6 : F.additive] [_inst_7 : G.additive], (F ⟶ G) → Π (n : ℕ), F.right_derived n ⟶ G.right_derived n := λ
{C : Type u} [_inst_1 : category_theory.category C] {D : Type u_1} [_inst_2 : category_theory.category D]
[_inst_3 : category_theory.abelian C] [_inst_4 : category_theory.has_injective_resolutions C]
[_inst_5 : category_theory.abelian D] {F G : C ⥤ D} [_inst_6 : F.additive] [_inst_7 : G.additive] (α : F ⟶ G)
(n : ℕ),
  category_theory.whisker_left (category_theory.injective_resolutions C)
    (category_theory.whisker_right (category_theory.nat_trans.map_homotopy_category α (complex_shape.up ℕ))
       (homotopy_category.homology_functor D (complex_shape.up ℕ) n))>
WARNING types not equal
<def category_theory.exp_terminal_iso_self : Π {C : Type u} [_inst_1 : category_theory.category C] {X : C}
[_inst_2 : category_theory.limits.has_finite_products C] [_inst_4 : category_theory.exponentiable (⊤_ C)],
  (category_theory.exp (⊤_ C)).obj X ≅ X := λ {C : Type u} [_inst_1 : category_theory.category C] {X : C}
[_inst_2 : category_theory.limits.has_finite_products C] [_inst_4 : category_theory.exponentiable (⊤_ C)],
  category_theory.yoneda.ext ((category_theory.exp (⊤_ C)).obj X) X
    (λ (Y : C) (f : Y ⟶ (category_theory.exp (⊤_ C)).obj X),
       (category_theory.limits.prod.left_unitor Y).inv ≫ category_theory.cartesian_closed.uncurry f)
    (λ (Y : C) (f : Y ⟶ X),
       category_theory.cartesian_closed.curry ((category_theory.limits.prod.left_unitor Y).hom ≫ f))
    category_theory.exp_terminal_iso_self._proof_9
    category_theory.exp_terminal_iso_self._proof_10
    category_theory.exp_terminal_iso_self._proof_11>
WARNING types not equal
<def category_theory.injective.exact.desc : Π {C : Type u} [_inst_1 : category_theory.category C]
[_inst_2 : category_theory.limits.has_zero_morphisms C] [_inst_3 : category_theory.limits.has_images Cᵒᵖ]
[_inst_4 : category_theory.limits.has_equalizers Cᵒᵖ] {J Q R S : C} [_inst_5 : category_theory.injective J]
(h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) [_inst_6 : category_theory.exact g.op f.op], f ≫ h = 0 → (S ⟶ J) := λ
{C : Type u} [_inst_1 : category_theory.category C] [_inst_2 : category_theory.limits.has_zero_morphisms C]
[_inst_3 : category_theory.limits.has_images Cᵒᵖ] [_inst_4 : category_theory.limits.has_equalizers Cᵒᵖ]
{J Q R S : C} [_inst_5 : category_theory.injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S)
[_inst_6 : category_theory.exact g.op f.op] (w : f ≫ h = 0), (category_theory.exact.lift h.op g.op f.op _).unop>

that looks Eric's

[Riccardo Brasca]

Voilà. The interesting output starts at line 605.

[Eric Rodriguez]

this is amazing! I already see some nice generalisations here...

[Eric Rodriguez]

this also reveals things that other linters should catch; for example, docs#algebra.id.smul_eq_mul was purportedly about the smul from algebra.id, but it is about has_mul.to_has_scalar. (This linter catches it as we can generalise this lemma to has_mulR, even though that makes no sense for algebra)

[Eric Wieser]

Some of those lemmas I just left behind for easy unification

[Eric Wieser]

docs#smul_eq_mul is the same as docs#algebra.id.smul_eq_mul

[Eric Wieser]

I didn't measure the effects of that, but note that the simp_nf linter doesn't seem to reject the dumplication

[Eric Wieser]

Similarly for docs#algebra.mul_smul_comm vs docs#mul_smul_comm

[Eric Rodriguez]

Oh, because Lean doesn't have to dig as far for the has_mul? That makes some sense

[Eric Wieser]

Maybe, who knows

[Eric Wieser]

I only wanted to light and put back out again so many fires at once in some PRs related to those, and leaving behind the less general lemmas was a nice way to avoid the fire growing

[Eric Rodriguez]

also interesteing that it gets some wrong in some weird ways (l632 of above):

#check @no_zero_smul_divisors.iff_algebra_map_injective
/- _inst_2: ring ↝ euclidean_domain no_zero_divisors
_inst_3: is_domain ↝ no_zero_divisors nontrivial
 -/

[Eric Wieser]

is_domain could in theory be replaced by those two typeclasses everywhere

[Eric Wieser]

It exists to make the spelling shorter

[Eric Rodriguez]

I meant more the ring ↝ euclidean_domain

[Eric Rodriguez]

first from this new full dataset: #13252

[Yaël Dillies]

@Eric Rodriguez, as it turns out I caught in #13268 the same generalization as the linter in #13260 :sweat_smile:

[Yaël Dillies]

Too bad I'm not running on a very powerful machine.

[Eric Rodriguez]

Riccardo Brasca said:

Voilà. The interesting output starts at line 605.

if you want to PR results from it, here's some of the outputs. I'm working on PRing some of this stuff as a side-hobby

[Yaël Dillies]

Yeah I read it but this was on my mind's queue after the "Rename nat.neg_one_pow_of_even" task :laughing:

[Scott Morrison]

I did a little editorial clean-up of @Riccardo Brasca's output, trying to remove the "garbage".

https://gist.github.com/semorrison/bdf8e3a5e4e6da34071f94821cec805c

[Scott Morrison]

In particular I simply removed everything that replaces a single type class with multiple ones, as these appear to often incorrect or in any case low priority.

[Yaël Dillies]

Do we want the separated_space ↝ t2_space? I remember some discussion about this.

[Scott Morrison]

I did the suggestions for data/polynomials/* in #13342.

[Yaël Dillies]

And me some of the suggestions (which I once again found independently :sweat_smile:) for order.bounded_order in #13419.

[Eric Rodriguez]

The API for with_top and the API for with_top somehow...

;b

[Yaël Dillies]

Whooops

[Yaël Dillies]

#13443 for number_theory.