preparing for lean-3.13.0

Stream: general

[Johan Commelin]

If you look at https://github.com/leanprover-community/lean/commits/master, which of yesterdays commits is most likely to cause breakage in category_theory/whiskering?

[Johan Commelin]

rewrite tactic failed, did not find instance of the pattern in the target expression
  X.map ?m_3 ≫ f.app ?m_2
state:
C : Type u₁,
_inst_1 : category C,
D : Type u₂,
_inst_2 : category D,
E : Type u₃,
_inst_3 : category E,
F G : C ⥤ D,
τ : F ⟶ G,
X Y : D ⥤ E,
f : X ⟶ Y,
x : C
⊢ (whisker_left F f).app x ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ (whisker_left G f).app x

@[simps] def whiskering_left : (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)) :=
{ obj := λ F,
  { obj := λ G, F ⋙ G,
    map := λ G H α, whisker_left F α },
  map := λ F G τ,
  { app := λ H,
    { app := λ c, H.map (τ.app c),
      naturality' := λ X Y f, begin dsimp, rw [←H.map_comp, ←H.map_comp, ←τ.naturality] end },
    naturality' := λ X Y f, begin ext, dsimp, rw [f.naturality] end } }
-- error under the final `rw`

[Reid Barton]

Probably the congr_lemma/simp_lemma stuff, but partly because I don't know what those are

[Johan Commelin]

I can replace the rw with erw, and after that refl closes the goal. But I'd rather understand what went wrong...

[Reid Barton]

My guess would be that the goal after dsimp changed somehow

[Johan Commelin]

Probably, yes

[Johan Commelin]

Can you check what the goal looks like in current mathlib?

[Reid Barton]

Not easily at the moment

[Johan Commelin]

⊢ f.app (F.obj x) ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ f.app (G.obj x)

(I found a second copy of mathlib on my disk.)

[Reid Barton]

I strongly suggest keeping a build of the last working version available when doing upgrades for things like this

[Johan Commelin]

So yes, dsimp changed.

[Johan Commelin]

@Gabriel Ebner Is this expected behaviour? Is dsimp supposed to behave differently?

[Reid Barton]

I'll type this out so you can just paste it:

set_option trace.simplify.rewrite true

[Reid Barton]

It could also be that the lemma that's supposed to be used changed in some way

[Gabriel Ebner]

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23229/near/197722657

[Johan Commelin]

@Gabriel Ebner thanks for the pointer. I'll see how much I can fix.

[Gabriel Ebner]

That's the only change I needed for mathlib to compile after the simp_cache PR.

[Johan Commelin]

I'm surprised that I didn't have any trouble with this "breaking change" in simp for the entire dependency tree of number_theory/quadratic_reciprocity. (Ok, I had to add mul_assoc to a simp only exactly once.)

[Johan Commelin]

Aah, you're saying I should apply that patch, and hopefully be done with it?

[Gabriel Ebner]

Yes!

[Johan Commelin]

I've applied the patch. Trying to compile now.

[Johan Commelin]

@Gabriel Ebner If this all compiles, would you consider releasing 3.13?

[Gabriel Ebner]

It's the weekend. But you can release 3.13 yourself if you want. Just submit a PR like lean#235, let bors merge it, and then tag the merged commit with v3.13.0.

[Johan Commelin]

If you're fine with me releasing it, then I'll try to do that.

[Johan Commelin]

Hooray! This branch compiles :tada:

[Johan Commelin]

What's left is sorting out the copyright stuff.

[Johan Commelin]

I'll leave that to others

[Kevin Buzzard]

I emailed Leo but didn't hear back yet

[Bryan Gin-ge Chen]

I put lean#243 on the queue and I'll tag it when the build finishes.

[Johan Commelin]

@Bryan Gin-ge Chen Thanks!

[Bryan Gin-ge Chen]

Linting failed, not too surprisingly. I'm guessing we should just add a bunch of stuff to nolints.txt and fix it later?

Also, some tests failed.

[Mario Carneiro]

int.int.sub_self?

[Mario Carneiro]

also int.int.eq_zero_or_eq_zero_of_mul_eq_zero

[Mario Carneiro]

why are we setting a bunch of lemmas as protected in mathlib rather than in core?

[Mario Carneiro]

There is obviously going to be a second "cleanup phase" to remove init_ from mathlib, but I guess the intent is to delay that until after the initial version bump PR

[Mario Carneiro]

and probably lint cleanups should be delayed until then

[Bryan Gin-ge Chen]

Where's int.int.sub_self? The linter didn't seem to catch that one: https://github.com/leanprover-community/mathlib/runs/681449690#step:14:121

[Mario Carneiro]

It's mentioned by name in the mk_protected call

[Mario Carneiro]

it's in core

[Bryan Gin-ge Chen]

Ah, yeah. Looks like they're both in int.dat.int.order.

[Bryan Gin-ge Chen]

Should I release 3.13.1 with those fixed?

[Bryan Gin-ge Chen]

PR: lean#245

[Mario Carneiro]

what about the protected definitions?

[Bryan Gin-ge Chen]

I could add that too if you think it's a good idea.

[Mario Carneiro]

I do

[Mario Carneiro]

Johan has conveniently already made a list

[Bryan Gin-ge Chen]

OK, I'll add it to this PR after dinner.

[Mario Carneiro]

(I should have #xy'd it when he was asking about mk_protected)

[Bryan Gin-ge Chen]

I wonder why these int lemmas are in a list called "nat_lemmas"...

[Bryan Gin-ge Chen]

Ah, I figured it out. int.mul_pos is already protected in core and int.mul_le_mul is in the second list, so those are supposed to be nat..

[Bryan Gin-ge Chen]

What's the purpose of int.mul_sub and int.sub_mul? Can I delete them?

[Bryan Gin-ge Chen]

@Mario Carneiro

[Mario Carneiro]

they are aliases

[Mario Carneiro]

I think int.mul_sub_left_distrib should just be renamed to int.mul_sub

[Mario Carneiro]

we don't need aliases for specialized lemmas that will be superceded later

[Bryan Gin-ge Chen]

OK, I'll just rename them. It's weird that they were made defs.

[Ryan Lahfa]

Lean is already being bumped to 3.13.0 on Nix unstable :'D, https://github.com/NixOS/nixpkgs/pull/88002/files

[Bryan Gin-ge Chen]

I just added a comment there.

[Mario Carneiro]

they are defs because you can skip the type if you do that

[Mario Carneiro]

mathlib has alias for this sort of thing

[Bryan Gin-ge Chen]

Oh, OK. Makes sense.

lean#245 looks ready, by the way. Should I merge it and release 3.13.1, or do you think I should wait for Gabriel (even though it's the weekend)?

[Mario Carneiro]

I think it should be okay to move forward with it. I'm working on the mathlib 3.13 cleanup and this will make things easier

[Bryan Gin-ge Chen]

Great, I'll move forward then.

[Bryan Gin-ge Chen]

@Mario Carneiro 3.13.1 has been released and the binaries are ready.

[Johan Commelin]

Thanks! Sorry for the double namespace issue.

[Bryan Gin-ge Chen]

No problem! I'm preparing a nolints.txt locally and I'll push again when that's done.

[Mario Carneiro]

I'm getting a simp loop:

0. [simplify.rewrite] [coe_fn_coe_base]: ⇑hnp ==> ⇑↑hnp
0. [simplify.rewrite] [coe_add_monoid_hom]: ⇑↑hnp ==> ⇑hnp
0. [simplify.rewrite] [coe_fn_coe_base]: ⇑hnp ==> ⇑↑hnp
0. [simplify.rewrite] [coe_add_monoid_hom]: ⇑↑hnp ==> ⇑hnp
0. [simplify.rewrite] [coe_fn_coe_base]: ⇑hnp ==> ⇑↑hnp
0. [simplify.rewrite] [coe_add_monoid_hom]: ⇑↑hnp ==> ⇑hnp
0. [simplify.rewrite] [coe_fn_coe_base]: ⇑hnp ==> ⇑↑hnp
0. [simplify.rewrite] [coe_add_monoid_hom]: ⇑↑hnp ==> ⇑hnp

is this my fault, or was this present before 3.13?

[Mario Carneiro]

MWE:

import algebra.ring
example {α β} [semiring α] [semiring β] (f : α →+* β) :
  ⇑(f : α →+ β) = f := by simp

[Yury G. Kudryashov]

Why does it pick the wrong instance for coercion of ring_hom to function?

[Yury G. Kudryashov]

Somehow it prefers the transitive instance to the explicit has_coe_to_fun.

[Mario Carneiro]

I'm rearranging theorems, so that might be my fault

[Mario Carneiro]

are you getting the transitive instance?

[Alex J. Best]

Works for me in mathlib from 5 days ago

[Yury G. Kudryashov]

In current master: no

[Mario Carneiro]

where is the has_coe_to_fun instance?

[Yury G. Kudryashov]

In algebra.ring

[Yury G. Kudryashov]

here

[Yury G. Kudryashov]

Your MWE works for me in the 3.13 branch

[Mario Carneiro]

Hm, that is still there in the right order with other things

[Mario Carneiro]

well, it's broken on my current open-heart-surgery version of the file

[Mario Carneiro]

Here's a MWE that should work on the latest version of #2707:

import algebra.group.hom algebra.group.is_unit
import tactic.norm_cast tactic.split_ifs algebra.group.units

universes u v w
variable {α : Type u}

set_option default_priority 100 -- see Note [default priority]
set_option old_structure_cmd true

@[ancestor has_mul has_add]
class distrib (α : Type u) extends has_mul α, has_add α :=
(left_distrib : ∀ a b c : α, a * (b + c) = (a * b) + (a * c))
(right_distrib : ∀ a b c : α, (a + b) * c = (a * c) + (b * c))

@[ancestor has_mul has_zero]
class mul_zero_class (α : Type u) extends has_mul α, has_zero α :=
(zero_mul : ∀ a : α, 0 * a = 0)
(mul_zero : ∀ a : α, a * 0 = 0)

@[ancestor add_comm_monoid monoid distrib mul_zero_class]
class semiring (α : Type u) extends add_comm_monoid α, monoid α, distrib α, mul_zero_class α

structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β]
  extends monoid_hom α β, add_monoid_hom α β

infixr ` →+* `:25 := ring_hom

instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe_to_fun (α →+* β) :=
⟨_, ring_hom.to_fun⟩

instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe (α →+* β) (α →+ β) :=
⟨ring_hom.to_add_monoid_hom⟩

@[simp, norm_cast]
lemma coe_add_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
  ⇑(f : α →+ β) = f := rfl

example {α β} [semiring α] [semiring β] (f : α →+* β) :
  ⇑(f : α →+ β) = f := by simp

[Yury G. Kudryashov]

Note that #2707 build fails somewhere in _init.

[Yury G. Kudryashov]

I think that has_coe_to_fun instance in master has default priority, not 100.

[Yury G. Kudryashov]

BTW, it would be nice if Lean generated the ancestor information for old_structure_cmd classes.

[Mario Carneiro]

I know #2707 is not done yet, but the files that are imported here should be working

[Yury G. Kudryashov]

I think that has_coe_to_fun instance in master has default priority, not 100.

:up:

[Mario Carneiro]

brilliant, that did it

[Mario Carneiro]

Yury G. Kudryashov said:

BTW, it would be nice if Lean generated the ancestor information for old_structure_cmd classes.

Indeed, it wasn't until I did the refactor that I even realized we are doing all this duplicate work

[Mario Carneiro]

it's very confusing having important attributes declared in completely different files from the declaration

[Yury G. Kudryashov]

Currently @[ancestor] attributes are used, e.g., by to_additive to map functions like group.to_monoid.

[Bryan Gin-ge Chen]

What's the point of this part of test/doc_commands.lean:

/-- ok -/
add_decl_doc division_ring

#eval do
ds ← doc_string ``division_ring,
guard $ ds = "ok"

The test is failing because division_ring is no longer automatically imported.

Should I search for another random undocumented declaration from core to use or can I just delete this? The next part of the file adds a random def foo with no docstring and tests that, so I think we're not losing anything, unless the behavior is somehow really different for imported declarations.

[Yury G. Kudryashov]

I think that the test should not rely on a declaration being undocumented.

[Yury G. Kudryashov]

I mean, we should try to avoid assumptions like this.

[Yury G. Kudryashov]

Recently I had to fix a test in core because it assumed that no file in core has a module docstring.

[Yury G. Kudryashov]

(and I added one module docstring)

[Bryan Gin-ge Chen]

OK, I agree. I'll just delete that part of the test.

[Bryan Gin-ge Chen]

Another test question, this time for test/monotonicity.lean:

import tactic.monotonicity tactic.norm_num
import algebra.ordered_ring
import data.list.defs

open list tactic tactic.interactive

example
  (h : 3 ≤ (4 : ℤ))
  (h' : 5 ≤ (6 : ℤ))
: (1 + 3 + 2) - 6 ≤ (4 + 2 + 1 : ℤ) - 5 :=
by ac_mono
/-
monotonic context not found
state:
h : 3 ≤ 4,
h' : 5 ≤ 6
⊢ (1 + 3 + 2).sub 6 ≤ (4 + 2 + 1).sub 5
-/

I think the fix is probably to add some more lemmas to the end of tactic.monotonicity.basic. Does anyone know off the top of their heads what I should add there?

[Bryan Gin-ge Chen]

@Simon Hudon ?

[Yury G. Kudryashov]

I wonder why it shows - as a.sub b. Is it possible that mono fails to understand that int.sub is the same as add_group.sub?

[Yury G. Kudryashov]

If yes, then it needs versions of sub lemmas for int.

[Bryan Gin-ge Chen]

Adding attribute [mono] int.sub_le_sub didn't help, unfortunately.

[Bryan Gin-ge Chen]

Ah, you were on the right track. I added int.sub here and it fixed it. I wonder if that's enough.

[Bryan Gin-ge Chen]

Specifically: should I also add nat.sub?

[Yury G. Kudryashov]

I think that the answer is no because int.sub is a + -b while nat.sub is an inductive definition.

[Bryan Gin-ge Chen]

Ah, right. Looks like this example with nat subtraction doesn't work in my 3.11.0 playground, so I won't try to make it work with 3.13.1:

example
  (h : 3 + 6 ≤ 4 + 5)
: 1 + 3 + 2 - 6 ≤ 4 + 2 - 1 + 5 :=
begin
  ac_mono,
end
/-
monotonic context not found
state:
h : 3 + 6 ≤ 4 + 5
⊢ nat.sub (1 + 3 + 2) 6 ≤ nat.sub (4 + 2) 1 + 5
-/

[Mario Carneiro]

I think that unfold directive should first make sure it's unfolding to a + -b

[Mario Carneiro]

that is, it should not unfold has_sub.sub but rather simp only [sub_eq_add_neg]

[Bryan Gin-ge Chen]

When I replace that dunfold ... with simp only [sub_eq_add_neg], the first example I posted (with ints) fails with

tactic failed, there are no goals to be solved
state:
no goals

[Bryan Gin-ge Chen]

It also doesn't help with the nat subtraction example.

[Bryan Gin-ge Chen]

Anyways, I'm done with #2697 for now. I think it should have a green check mark... :fingers_crossed:

[Yury G. Kudryashov]

In the first case I think that simp only performs some computations even if you don't ask it for this.

[Yury G. Kudryashov]

So this simp only [sub_eq_add_neg] solves the goal.

[Gabriel Ebner]

simp will try refl and trivial afterwards, this might be the case here.

[Bryan Gin-ge Chen]

#2697 indeed builds, should we try and merge it?

[Sebastien Gouezel]

How does it interact with #2707? I mean, isn't #2707 suppose to supercede #2697?

[Sebastien Gouezel]

And will merging #2697 break #2707?

[Sebastien Gouezel]

In fact, all the commits of #2697 are already integrated into #2707, so there shouldn't be any problem. I say go ahead!

[Bryan Gin-ge Chen]

OK, let's go then.

[Mario Carneiro]

Oh, I just realized that one of the areas I was most looking forward to refactoring as a result of the move, the stuff on order structures, was not included as part of the big move. Have we looked at giving the same treatment to the preorder, partial_order, linear_order classes in core?

[Patrick Massot]

It was decided to postpone this to the next big refactor, to keep things vaguely under control.

[Bryan Gin-ge Chen]

Presumably it's much easier than removing algebra because we don't have to worry about norm_num, right?

[Patrick Massot]

But you're very welcome to take the next step, at least assume we sorted out this copyright line question

[Mario Carneiro]

I haven't done much with the copyright line in #2707, I'm just merging the author lists

[Kevin Buzzard]

I didn't hear back from Leo

[Kevin Buzzard]

The license says that what we're doing is ok though, as far as I can see

[Patrick Massot]

There is no license issue, this is a politeness issue

[Mario Carneiro]

what is the politeness issue? The author lists are being preserved

[Mario Carneiro]

plus lean 3 is still there on leanprover/lean where it has always been

[Bryan Gin-ge Chen]

Did the module doc change in 3.13.0 (lean#241) cause module docs to stop showing up in the mathlib docs? Compare https://leanprover-community.github.io/mathlib_docs/algebra/group_with_zero.html and https://github.com/leanprover-community/mathlib/blob/f23c361/src/algebra/group_with_zero.lean

[Rob Lewis]

Are there no tests in core for the module doc retrieval functions?

[Bryan Gin-ge Chen]

For reference, here's the diff where module docs were removed (the commit corresponding to #2697).

There are two tests that mention module_doc_strings 1 2 and they both passed. Is there something else to check?

[Rob Lewis]

Neither of those test that docs from earlier modules stick around. They're both assuming that no earlier imports have module docs (which makes them fragile tests).

[Bryan Gin-ge Chen]

Oh, I was looking at the wrong function. module_doc_strings only looks in the current file.

Yes, olean_doc_strings isn't tested and seems to behave strangely now.

Compare:

open tactic

run_cmd olean_doc_strings >>= trace
/-
empty.lean:4:0: information trace output
[((some /Users/chb/.elan/toolchains/leanprover-community-lean-3.13.1/lib/lean/library/init/meta/case_tag.lean),
  [(⟨8, 0⟩, # General operations on functions),
   (⟨9, 0⟩,
    # Case tags

Case tags are an internal mechanism used by certain tactics to communicate with
each other. They are generated by the tactics `cases`, `induction` and
`with_cases` ('cases-like tactics'), which generate goals corresponding to the
'cases' of an inductive hypothesis. Each of these goals carries a case tag. They
are consumed by the `case` tactic, which focuses on one of these cases. Their
purpose is twofold:

1. Give intuitive names to case goals. For example, when performing induction on
   a natural number, two cases are generated: one tagged with `nat.zero` and
   one tagged with `nat.succ`. Users can then focus on e.g. the second goal with
   `case succ {...}`.
2. Communicate which new hypotheses were introduced by the cases-like tactic
   that generated the goal. For example, when performing induction on a
   `list α`, the `cons` case introduces two hypotheses corresponding to the two
   arguments of the `cons` constructor. `case` allows users to name these with
   `case cons : x xs {...}`. To perform this renaming, `case` needs to know
   which hypotheses to rename; this information is contained in the case tag for
   the `cons` goal.

## Module contents

This module defines

1. what a case tag is (see `case_tag`);
2. how to render a `case_tag` as a list of names (see `render`);
3. how to parse  a `case_tag` from a list of names (see `parse`);
4. how to match a `case_tag` with a sequence of names given by the user
   (see `match_tag`).)]),
 (none, [])]

-/

If I add import doc where doc.lean contains just /-! hi -/:

import doc
open tactic

run_cmd olean_doc_strings >>= trace
/-
empty.lean:4:0: information trace output
[((some /Users/chb/Documents/lean/my_project_2/src/doc.lean),
  [(⟨8, 0⟩, # General operations on functions),
   (⟨9, 0⟩,
    # Case tags

Case tags are an internal mechanism used by certain tactics to communicate with
each other. They are generated by the tactics `cases`, `induction` and
`with_cases` ('cases-like tactics'), which generate goals corresponding to the
'cases' of an inductive hypothesis. Each of these goals carries a case tag. They
are consumed by the `case` tactic, which focuses on one of these cases. Their
purpose is twofold:

1. Give intuitive names to case goals. For example, when performing induction on
   a natural number, two cases are generated: one tagged with `nat.zero` and
   one tagged with `nat.succ`. Users can then focus on e.g. the second goal with
   `case succ {...}`.
2. Communicate which new hypotheses were introduced by the cases-like tactic
   that generated the goal. For example, when performing induction on a
   `list α`, the `cons` case introduces two hypotheses corresponding to the two
   arguments of the `cons` constructor. `case` allows users to name these with
   `case cons : x xs {...}`. To perform this renaming, `case` needs to know
   which hypotheses to rename; this information is contained in the case tag for
   the `cons` goal.

## Module contents

This module defines

1. what a case tag is (see `case_tag`);
2. how to render a `case_tag` as a list of names (see `render`);
3. how to parse  a `case_tag` from a list of names (see `parse`);
4. how to match a `case_tag` with a sequence of names given by the user
   (see `match_tag`).),
   (⟨1, 0⟩, hey!)]),
 (none, [])]

-/

[Bryan Gin-ge Chen]

olean_doc_strings was formerly tested, but the test was removed in lean#216.

Oh, this is the test that @Yury G. Kudryashov mentioned earlier. Not sure what the best solution would have been.

[Bryan Gin-ge Chen]

I guess a good test would be to read the output of olean_doc_strings and then check each of the files / locations that appear to see if the doc strings actually exist there. This is beyond my capabilities though.

The issue as I understand it from my example above is that the module doc strings aren't being associated to the correct files. I'm not sure where to start with fixing olean_doc_strings.

[Mario Carneiro]

How do I silence the simp_nf linter warning in https://github.com/leanprover-community/mathlib/runs/683541688 ? The message doesn't give any hints as to which lemma is bad

[Mario Carneiro]

This idiom is broken in 3.13:

import algebra.ordered_ring

example {a b : ℕ} (h : b > 0) (w : a ≥ 1) : b ≤ a * b :=
(le_mul_iff_one_le_left h).mpr w

type mismatch at application
  le_mul_iff_one_le_left h
term
  h
has type
  b > 0
but is expected to have type
  0 < ?m_3

Which is too bad, because I use this a lot. If you use iff.mpr instead of (...).mpr or (...).2 then it works

[Mario Carneiro]

If you provide the type as in @le_mul_iff_one_le_left nat _ _ _ h then it works

[Mario Carneiro]

the fact that the theorem is stated with > is a red herring, it does the same thing with <

[Mario Carneiro]

I manually fixed a couple of instances of this in #2707, but the one above is apparently also causing library_search to fail to find this proof, which breaks one of the tests

[Bryan Gin-ge Chen]

Do you know which commit broke this?

[Mario Carneiro]

I imagine it was the speed up release (3.12?)

[Mario Carneiro]

I can make a test that works without any imports if you like

[Mario Carneiro]

test/lint.lean is also failing, and I don't understand the test enough to fix it. Something to do with detecting typeclass inference loops

[Bryan Gin-ge Chen]

Hmm, your example:

import algebra.ordered_ring

example {a b : ℕ} (h : b > 0) (w : a ≥ 1) : b ≤ a * b :=
(le_mul_iff_one_le_left h).mpr w

works with current mathlib master for me.

[Mario Carneiro]

Ah... nat isn't imported

[Mario Carneiro]

I'm pretty sure this is coming up in a real situation, but the library search test is broken for a more stupid reason

[Mario Carneiro]

Ok, try this:

import algebra.ordered_field

example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
iff.mp (mul_self_inj_of_nonneg _ (mul_nonneg _ _)) _ -- ok

example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
(mul_self_inj_of_nonneg _ (mul_nonneg _ _)).1 _ -- not ok

[Bryan Gin-ge Chen]

Hmm, I'm getting errors at all of the underscores in both:

empty.lean:4:31: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ 0 ≤ c
empty.lean:4:45: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ a ≥ 0
empty.lean:4:47: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ b ≥ 0
empty.lean:4:51: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ c * c = a * b * (a * b)
empty.lean:7:24: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ 0 ≤ c
empty.lean:7:38: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ a ≥ 0
empty.lean:7:40: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ b ≥ 0
empty.lean:7:46: error
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ c * c = a * b * (a * b)

[Mario Carneiro]

hm, maybe it's another instance priority mixup

[Bryan Gin-ge Chen]

Mario Carneiro said:

How do I silence the simp_nf linter warning in https://github.com/leanprover-community/mathlib/runs/683541688 ? The message doesn't give any hints as to which lemma is bad

I'm not really sure, but do we need to have the division_field versions of these lemmas if they are provable using their group_with_zero counterparts?

[Mario Carneiro]

Does have := (mul_self_inj_of_nonneg _ (mul_nonneg _ _)), work for you?

[Bryan Gin-ge Chen]

import algebra.ordered_field

example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
begin
have := (mul_self_inj_of_nonneg _ (mul_nonneg _ _)),
/-
empty.lean:7:0: error
tactic failed, there are unsolved goals
state:
9 goals
α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α,
this : ?m_3 * ?m_3 = ?m_4 * ?m_5 * (?m_4 * ?m_5) ↔ ?m_3 = ?m_4 * ?m_5
⊢ c = a * b

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ Type ?

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ linear_ordered_field ?m_1

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ ?m_1

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ ?m_1

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ ?m_1

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ 0 ≤ ?m_3

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ ?m_3 ≥ 0

α : Type ?,
_inst_1 : linear_ordered_field α,
a b c : α
⊢ ?m_3 ≥ 0
-/
end

[Mario Carneiro]

We should just delete the division_ring versions of the lemmas, but I was hoping to leave that until the next PR

[Bryan Gin-ge Chen]

You could just remove the @[simp] from them then.

[Mario Carneiro]

I get

type mismatch at application
  @mul_self_inj_of_nonneg.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 ?m_6 (@mul_nonneg.{?l_7} ?m_8 ?m_9 ?m_10 ?m_11 ?m_12 ?m_13)
term
  @mul_nonneg.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 ?m_6 ?m_7
has type
  @ge.{?l_1} ?m_2
    (@preorder.to_has_le.{?l_1} ?m_2
       (@partial_order.to_preorder.{?l_1} ?m_2
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_1} ?m_2
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_1} ?m_2 ?m_3))))
    (@has_mul.mul.{?l_1} ?m_2
       (@mul_zero_class.to_has_mul.{?l_1} ?m_2
          (@semiring.to_mul_zero_class.{?l_1} ?m_2 (@ordered_semiring.to_semiring.{?l_1} ?m_2 ?m_3)))
       ?m_4
       ?m_5)
    (@has_zero.zero.{?l_1} ?m_2
       (@mul_zero_class.to_has_zero.{?l_1} ?m_2
          (@semiring.to_mul_zero_class.{?l_1} ?m_2 (@ordered_semiring.to_semiring.{?l_1} ?m_2 ?m_3))))
but is expected to have type
  @has_le.le.{?l_1} ?m_2
    (@preorder.to_has_le.{?l_1} ?m_2
       (@partial_order.to_preorder.{?l_1} ?m_2
          (@ordered_add_comm_group.to_partial_order.{?l_1} ?m_2
             (@ordered_ring.to_ordered_add_comm_group.{?l_1} ?m_2
                (@linear_ordered_ring.to_ordered_ring.{?l_1} ?m_2
                   (@linear_ordered_field.to_linear_ordered_ring.{?l_1} ?m_2 ?m_3))))))
    (@has_zero.zero.{?l_1} ?m_2
       (@no_zero_divisors.to_has_zero.{?l_1} ?m_2
          (@integral_domain.to_no_zero_divisors.{?l_1} ?m_2
             (@field.to_integral_domain.{?l_1} ?m_2 (@linear_ordered_field.to_field.{?l_1} ?m_2 ?m_3)))))
    ?m_4

[Bryan Gin-ge Chen]

Prepare for pp.all spam:

import algebra.ordered_field

set_option pp.all true
example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
begin
have := (mul_self_inj_of_nonneg _ (mul_nonneg _ _)),
/-
empty.lean:8:0: error
tactic failed, there are unsolved goals
state:
9 goals
α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α,
this :
  iff
    (@eq.{?l_2+1} ?m_3
       (@has_mul.mul.{?l_2} ?m_3
          (@no_zero_divisors.to_has_mul.{?l_2} ?m_3
             (@domain.to_no_zero_divisors.{?l_2} ?m_3
                (@division_ring.to_domain.{?l_2} ?m_3
                   (@field.to_division_ring.{?l_2} ?m_3 (@linear_ordered_field.to_field.{?l_2} ?m_3 ?m_4)))))
          ?m_5
          ?m_5)
       (@has_mul.mul.{?l_2} ?m_3
          (@no_zero_divisors.to_has_mul.{?l_2} ?m_3
             (@domain.to_no_zero_divisors.{?l_2} ?m_3
                (@division_ring.to_domain.{?l_2} ?m_3
                   (@field.to_division_ring.{?l_2} ?m_3 (@linear_ordered_field.to_field.{?l_2} ?m_3 ?m_4)))))
          (@has_mul.mul.{?l_2} ?m_3
             (@mul_zero_class.to_has_mul.{?l_2} ?m_3
                (@semiring.to_mul_zero_class.{?l_2} ?m_3
                   (@ordered_semiring.to_semiring.{?l_2} ?m_3
                      (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                         (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                            (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4))))))
             ?m_6
             ?m_7)
          (@has_mul.mul.{?l_2} ?m_3
             (@mul_zero_class.to_has_mul.{?l_2} ?m_3
                (@semiring.to_mul_zero_class.{?l_2} ?m_3
                   (@ordered_semiring.to_semiring.{?l_2} ?m_3
                      (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                         (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                            (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4))))))
             ?m_6
             ?m_7)))
    (@eq.{?l_2+1} ?m_3 ?m_5
       (@has_mul.mul.{?l_2} ?m_3
          (@mul_zero_class.to_has_mul.{?l_2} ?m_3
             (@semiring.to_mul_zero_class.{?l_2} ?m_3
                (@ordered_semiring.to_semiring.{?l_2} ?m_3
                   (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                      (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                         (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4))))))
          ?m_6
          ?m_7))
⊢ @eq.{?l_1+1} α c
    (@has_mul.mul.{?l_1} α
       (@no_zero_divisors.to_has_mul.{?l_1} α
          (@domain.to_no_zero_divisors.{?l_1} α
             (@division_ring.to_domain.{?l_1} α
                (@field.to_division_ring.{?l_1} α (@linear_ordered_field.to_field.{?l_1} α _inst_1)))))
       a
       b)

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ Type ?l_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ linear_ordered_field.{?l_2} ?m_3

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ?m_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ?m_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ?m_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ @has_le.le.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid.{?l_2} ?m_3
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3
                   (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                      (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                         (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4))))))))
    (@has_zero.zero.{?l_2} ?m_3
       (@no_zero_divisors.to_has_zero.{?l_2} ?m_3
          (@domain.to_no_zero_divisors.{?l_2} ?m_3
             (@division_ring.to_domain.{?l_2} ?m_3
                (@field.to_division_ring.{?l_2} ?m_3 (@linear_ordered_field.to_field.{?l_2} ?m_3 ?m_4))))))
    ?m_5

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3
                (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                   (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                      (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4)))))))
    ?m_5
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3
             (@ordered_semiring.to_semiring.{?l_2} ?m_3
                (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                   (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                      (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4)))))))

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3
                (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                   (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                      (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4)))))))
    ?m_5
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3
             (@ordered_semiring.to_semiring.{?l_2} ?m_3
                (@ordered_ring.to_ordered_semiring.{?l_2} ?m_3
                   (@linear_ordered_ring.to_ordered_ring.{?l_2} ?m_3
                      (@linear_ordered_field.to_linear_ordered_ring.{?l_2} ?m_3 ?m_4)))))))
-/
end

[Mario Carneiro]

hm, could you send me one more test:

set_option pp.all true
example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
begin
  have := mul_nonneg _ _,
  have := mul_self_inj_of_nonneg _ (by {}),
end
-- solve1 tactic failed, focused goal has not been solved
-- state:
-- α : Type ?l_1,
-- _inst_1 : linear_ordered_field.{?l_1} α,
-- a b c : α,
-- this :
--   @ge.{?l_2} ?m_3
--     (@preorder.to_has_le.{?l_2} ?m_3
--        (@partial_order.to_preorder.{?l_2} ?m_3
--           (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
--              (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3 ?m_4))))
--     (@has_mul.mul.{?l_2} ?m_3
--        (@mul_zero_class.to_has_mul.{?l_2} ?m_3
--           (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4)))
--        ?m_5
--        ?m_6)
--     (@has_zero.zero.{?l_2} ?m_3
--        (@mul_zero_class.to_has_zero.{?l_2} ?m_3
--           (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4))))
-- ⊢ @has_le.le.{?l_7} ?m_8
--     (@preorder.to_has_le.{?l_7} ?m_8
--        (@partial_order.to_preorder.{?l_7} ?m_8
--           (@ordered_add_comm_group.to_partial_order.{?l_7} ?m_8
--              (@ordered_ring.to_ordered_add_comm_group.{?l_7} ?m_8
--                 (@linear_ordered_ring.to_ordered_ring.{?l_7} ?m_8
--                    (@linear_ordered_field.to_linear_ordered_ring.{?l_7} ?m_8 ?m_9))))))
--     (@has_zero.zero.{?l_7} ?m_8
--        (@no_zero_divisors.to_has_zero.{?l_7} ?m_8
--           (@integral_domain.to_no_zero_divisors.{?l_7} ?m_8
--              (@field.to_integral_domain.{?l_7} ?m_8 (@linear_ordered_field.to_field.{?l_7} ?m_8 ?m_9)))))
--     ?m_10

[Bryan Gin-ge Chen]

import algebra.ordered_field

set_option pp.all true
example {α} [linear_ordered_field α] (a b c : α) : c = a * b :=
begin
  have := mul_nonneg _ _,
  have := mul_self_inj_of_nonneg _ (by {}),
/-
empty.lean:7:40: error
solve1 tactic failed, focused goal has not been solved
state:
α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α,
this :
  @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3 ?m_4))))
    (@has_mul.mul.{?l_2} ?m_3
       (@mul_zero_class.to_has_mul.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4)))
       ?m_5
       ?m_6)
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4))))
⊢ @has_le.le.{?l_7} ?m_8
    (@preorder.to_has_le.{?l_7} ?m_8
       (@partial_order.to_preorder.{?l_7} ?m_8
          (@ordered_add_comm_monoid.to_partial_order.{?l_7} ?m_8
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid.{?l_7} ?m_8
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_7} ?m_8
                   (@ordered_ring.to_ordered_semiring.{?l_7} ?m_8
                      (@linear_ordered_ring.to_ordered_ring.{?l_7} ?m_8
                         (@linear_ordered_field.to_linear_ordered_ring.{?l_7} ?m_8 ?m_9))))))))
    (@has_zero.zero.{?l_7} ?m_8
       (@no_zero_divisors.to_has_zero.{?l_7} ?m_8
          (@domain.to_no_zero_divisors.{?l_7} ?m_8
             (@division_ring.to_domain.{?l_7} ?m_8
                (@field.to_division_ring.{?l_7} ?m_8 (@linear_ordered_field.to_field.{?l_7} ?m_8 ?m_9))))))
    ?m_10
state:
7 goals
α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α,
this :
  @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3 ?m_4))))
    (@has_mul.mul.{?l_2} ?m_3
       (@mul_zero_class.to_has_mul.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4)))
       ?m_5
       ?m_6)
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4))))
⊢ @eq.{?l_1+1} α c
    (@has_mul.mul.{?l_1} α
       (@no_zero_divisors.to_has_mul.{?l_1} α
          (@domain.to_no_zero_divisors.{?l_1} α
             (@division_ring.to_domain.{?l_1} α
                (@field.to_division_ring.{?l_1} α (@linear_ordered_field.to_field.{?l_1} α _inst_1)))))
       a
       b)

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ Type ?l_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ordered_semiring.{?l_2} ?m_3

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ?m_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ ?m_2

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3 ?m_4))))
    ?m_5
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4))))

α : Type ?l_1,
_inst_1 : linear_ordered_field.{?l_1} α,
a b c : α
⊢ @ge.{?l_2} ?m_3
    (@preorder.to_has_le.{?l_2} ?m_3
       (@partial_order.to_preorder.{?l_2} ?m_3
          (@ordered_cancel_add_comm_monoid.to_partial_order.{?l_2} ?m_3
             (@ordered_semiring.to_ordered_cancel_add_comm_monoid.{?l_2} ?m_3 ?m_4))))
    ?m_5
    (@has_zero.zero.{?l_2} ?m_3
       (@mul_zero_class.to_has_zero.{?l_2} ?m_3
          (@semiring.to_mul_zero_class.{?l_2} ?m_3 (@ordered_semiring.to_semiring.{?l_2} ?m_3 ?m_4))))
-/
end

[Mario Carneiro]

Hm, it appears that the typeclass solutions have indeed changed, but it's not clear to me how this unification problem is supposed to succeed in the first place

[Mario Carneiro]

I get it now. Here is the unification problem on master:

example (α : Type) :
  @has_le.le α (@preorder.to_has_le α
    (@partial_order.to_preorder α
      (@ordered_cancel_add_comm_monoid.to_partial_order α
        (@ordered_semiring.to_ordered_cancel_add_comm_monoid α (id _))))) =
  @has_le.le α (@preorder.to_has_le α
    (@partial_order.to_preorder α
      (@ordered_add_comm_monoid.to_partial_order α
        (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid α
          (@ordered_semiring.to_ordered_cancel_add_comm_monoid α
            (@ordered_ring.to_ordered_semiring α
              (@linear_ordered_ring.to_ordered_ring α
                (@linear_ordered_field.to_linear_ordered_ring α (id _))))))))) := rfl -- works

and here is the new version

example (α : Type) :
  @has_le.le α (@preorder.to_has_le α
    (@partial_order.to_preorder α
      (@ordered_cancel_add_comm_monoid.to_partial_order α
        (@ordered_semiring.to_ordered_cancel_add_comm_monoid α (id _))))) =
  @has_le.le α (@preorder.to_has_le α
    (@partial_order.to_preorder α
      (@ordered_add_comm_group.to_partial_order α
        (@ordered_ring.to_ordered_add_comm_group α
          (@linear_ordered_ring.to_ordered_ring α
            (@linear_ordered_field.to_linear_ordered_ring α (id _))))))) := rfl -- fails

The original one works because ordered_semiring is in the chain of instances from linear_ordered_field to has_le. In the new path it goes via ordered_ring -> ordered_add_comm_group -> ... and skips ordered_semiring. It's a bit disturbing that elaboration depends on which of many defeq paths is found by typeclass inference, and while I think it would be possible to recover the original path I think there are other examples that would break on master and don't break with the new ordering

[Bryan Gin-ge Chen]

Will things get better in Lean 4?

[Mario Carneiro]

this seems like a pretty messy elaboration order problem, so I wouldn't be surprised if the answer is no

[Mario Carneiro]

The fact that everything in sight is an old_structure_cmd is also a contributing factor, I think

[Mario Carneiro]

If these structures were neatly nested you would be guaranteed to have one fit in the other

[Mario Carneiro]

but on the other hand that doesn't reflect the reality of the situation - algebraic classes do not form a tree, there are diamonds and so instances that work by deconstructing the input into pieces and rebuilding a new structure are necessary

[Yury G. Kudryashov]

I removed the test because it tested that no files in core have module docstrings. Possibly a better approach would be to create another file, import it, and filter docstrings from this file only.

[Johan Commelin]

So... 3.13 created a big mess? But is everything cleaned up now?

[Johan Commelin]

@Mario Carneiro Do classify the problematic behaviour as a regression?

[Mario Carneiro]

I think it's revealing a dependence on the order of instances. The new order isn't better or worse, but it is different and that breaks some existing proofs

[Mario Carneiro]

I think #2707 is ready now

[Yury G. Kudryashov]

I removed some unneeded [to_additive] attributes.

[Yury G. Kudryashov]

to_additive automatically maps structure fields and projections. It needs ancestor attrs to deal with old_structure_cmd projections.

[Yury G. Kudryashov]

And it doesn't need to map has_mul.mk to has_add.mk because it maps prefixes, not full names.

[Mario Carneiro]

That's great. I don't recall when ancestor was added and exactly what its scope is.

[Mario Carneiro]

I think lean now has hooks for adding structures, so perhaps it might even be possible to create add_group itself using to_additive

[Yury G. Kudryashov]

When I was rewriting to_additive, ancestor was already here.

[Yury G. Kudryashov]

You mean adding structures with all mk/rec/whatever?

[Mario Carneiro]

I mean creating the structure input data, letting lean do the hard work of creating projections and all that

[Mario Carneiro]

I could be mistaken though. I know we added it for inductive but I forget if a hook for structure was also added

[Patrick Massot]

I think ancestor was introduced for the purpose of subtype_instance

[Gabriel Ebner]

Skimming over this thread:

• The doc string bug is still open, right? I'll get to it now.
• There was a simp_nf linter bug, a type class inference bug, and something else? If these are still issues, please file bugs / #mwe here.

[Bryan Gin-ge Chen]

I think the only bug is the doc string bug. The other things mentioned are just issues that came up with merging algebra together in #2707.

[Yury G. Kudryashov]

@Gabriel Ebner One more quesion: how do I copy an attribute like no_rsimp or ematch? tactic.copy_attribute doesn't work.

[Gabriel Ebner]

I think you need to use user_attribute for this. Look at mk_hinst_lemma_attr_set how the ematch attribute is defined.

[Sebastien Gouezel]

I also found an issue with typeclass inference, unrelated to the move to 3.13 though. Issue filed at https://github.com/leanprover-community/lean/issues/244

[Sebastien Gouezel]

Discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197786186

[Gabriel Ebner]

lean#249, are there any other high priority fixes we should include in 3.13.2?

[Johan Commelin]

I'm not aware of any

[Sebastien Gouezel]

Neither am I.

[Bryan Gin-ge Chen]

Thanks for the quick fix, Gabriel!

[Bryan Gin-ge Chen]

The docs should hopefully be fixed in 15-20 minutes.

Edit: The module doc strings are back! https://leanprover-community.github.io/mathlib_docs/algebra/group_with_zero.html

[Kevin Buzzard]

Leo said:

Yes, the Apache license used in Lean allows anybody to copy files from Lean to other projects if they keep the copyright notice. I am not unhappy or happy with the idea of moving Lean3 files to mathlib.

[Bryan Gin-ge Chen]

Mario Carneiro said:

Oh, I just realized that one of the areas I was most looking forward to refactoring as a result of the move, the stuff on order structures, was not included as part of the big move. Have we looked at giving the same treatment to the preorder, partial_order, linear_order classes in core?

Is this just a matter of removing init.algebra.order? Should init.algebra.classes be cleaned up somehow too?

[Mario Carneiro]

If nothing in core breaks, yes

[Mario Carneiro]

It is likely though that some order theorems will be used over nat and int, and these need specialized versions or alternate proofs