# Zulip Chat Archive

## Stream: general

### Topic: preparing for lean-3.13.0

#### Johan Commelin (May 16 2020 at 14:41):

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 (May 16 2020 at 14:42):

```
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 (May 16 2020 at 14:44):

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

#### Johan Commelin (May 16 2020 at 14:44):

I can replace the `rw`

with `erw`

, and after that `refl`

closes the goal. But I'd rather understand what went wrong...

#### Reid Barton (May 16 2020 at 14:45):

My guess would be that the goal after `dsimp`

changed somehow

#### Johan Commelin (May 16 2020 at 14:45):

Probably, yes

#### Johan Commelin (May 16 2020 at 14:45):

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

#### Reid Barton (May 16 2020 at 14:46):

Not easily at the moment

#### Johan Commelin (May 16 2020 at 14:46):

```
⊢ 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 (May 16 2020 at 14:46):

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

#### Johan Commelin (May 16 2020 at 14:46):

So yes, `dsimp`

changed.

#### Johan Commelin (May 16 2020 at 14:48):

@Gabriel Ebner Is this expected behaviour? Is `dsimp`

supposed to behave differently?

#### Reid Barton (May 16 2020 at 14:50):

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

```
set_option trace.simplify.rewrite true
```

#### Reid Barton (May 16 2020 at 14:50):

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

#### Gabriel Ebner (May 16 2020 at 15:08):

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

#### Johan Commelin (May 16 2020 at 18:03):

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

#### Gabriel Ebner (May 16 2020 at 18:03):

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

PR.

#### Johan Commelin (May 16 2020 at 18:04):

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 (May 16 2020 at 18:04):

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

#### Gabriel Ebner (May 16 2020 at 18:05):

Yes!

#### Johan Commelin (May 16 2020 at 18:18):

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

#### Johan Commelin (May 16 2020 at 18:18):

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

#### Gabriel Ebner (May 16 2020 at 18:23):

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 (May 16 2020 at 18:28):

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

#### Johan Commelin (May 16 2020 at 18:43):

Hooray! This branch compiles :tada:

#### Johan Commelin (May 16 2020 at 18:59):

What's left is sorting out the copyright stuff.

#### Johan Commelin (May 16 2020 at 18:59):

I'll leave that to others

#### Kevin Buzzard (May 16 2020 at 19:09):

I emailed Leo but didn't hear back yet

#### Bryan Gin-ge Chen (May 16 2020 at 19:20):

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

#### Johan Commelin (May 16 2020 at 19:38):

@Bryan Gin-ge Chen Thanks!

#### Bryan Gin-ge Chen (May 16 2020 at 22:02):

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 (May 16 2020 at 22:10):

`int.int.sub_self`

?

#### Mario Carneiro (May 16 2020 at 22:10):

also `int.int.eq_zero_or_eq_zero_of_mul_eq_zero`

#### Mario Carneiro (May 16 2020 at 22:10):

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

#### Mario Carneiro (May 16 2020 at 22:14):

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 (May 16 2020 at 22:15):

and probably lint cleanups should be delayed until then

#### Bryan Gin-ge Chen (May 16 2020 at 22:15):

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 (May 16 2020 at 22:16):

It's mentioned by name in the `mk_protected`

call

#### Mario Carneiro (May 16 2020 at 22:16):

it's in core

#### Bryan Gin-ge Chen (May 16 2020 at 22:19):

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

.

#### Bryan Gin-ge Chen (May 16 2020 at 22:22):

Should I release 3.13.1 with those fixed?

#### Bryan Gin-ge Chen (May 16 2020 at 22:27):

PR: lean#245

#### Mario Carneiro (May 16 2020 at 22:27):

what about the protected definitions?

#### Bryan Gin-ge Chen (May 16 2020 at 22:28):

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

#### Mario Carneiro (May 16 2020 at 22:29):

I do

#### Mario Carneiro (May 16 2020 at 22:29):

Johan has conveniently already made a list

#### Bryan Gin-ge Chen (May 16 2020 at 22:29):

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

#### Mario Carneiro (May 16 2020 at 22:30):

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

)

#### Bryan Gin-ge Chen (May 17 2020 at 00:30):

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

#### Bryan Gin-ge Chen (May 17 2020 at 00:48):

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 (May 17 2020 at 01:09):

What's the purpose of `int.mul_sub`

and `int.sub_mul`

? Can I delete them?

#### Bryan Gin-ge Chen (May 17 2020 at 01:09):

@Mario Carneiro

#### Mario Carneiro (May 17 2020 at 01:11):

they are aliases

#### Mario Carneiro (May 17 2020 at 01:11):

I think `int.mul_sub_left_distrib`

should just be renamed to `int.mul_sub`

#### Mario Carneiro (May 17 2020 at 01:12):

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

#### Bryan Gin-ge Chen (May 17 2020 at 01:13):

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

s.

#### Ryan Lahfa (May 17 2020 at 01:32):

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 (May 17 2020 at 01:46):

I just added a comment there.

#### Mario Carneiro (May 17 2020 at 02:20):

they are `def`

s because you can skip the type if you do that

#### Mario Carneiro (May 17 2020 at 02:20):

mathlib has `alias`

for this sort of thing

#### Bryan Gin-ge Chen (May 17 2020 at 02:22):

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 (May 17 2020 at 03:06):

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 (May 17 2020 at 03:06):

Great, I'll move forward then.

#### Bryan Gin-ge Chen (May 17 2020 at 04:15):

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

#### Johan Commelin (May 17 2020 at 05:22):

Thanks! Sorry for the double namespace issue.

#### Bryan Gin-ge Chen (May 17 2020 at 05:26):

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

#### Mario Carneiro (May 17 2020 at 05:47):

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 (May 17 2020 at 05:49):

MWE:

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

#### Yury G. Kudryashov (May 17 2020 at 05:50):

Why does it pick the wrong instance for coercion of `ring_hom`

to function?

#### Yury G. Kudryashov (May 17 2020 at 05:51):

Somehow it prefers the transitive instance to the explicit `has_coe_to_fun`

.

#### Mario Carneiro (May 17 2020 at 05:51):

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

#### Mario Carneiro (May 17 2020 at 05:51):

are you getting the transitive instance?

#### Alex J. Best (May 17 2020 at 05:52):

Works for me in mathlib from 5 days ago

#### Yury G. Kudryashov (May 17 2020 at 05:52):

In current `master`

: no

#### Mario Carneiro (May 17 2020 at 05:53):

where is the has_coe_to_fun instance?

#### Yury G. Kudryashov (May 17 2020 at 05:53):

In `algebra.ring`

#### Yury G. Kudryashov (May 17 2020 at 05:54):

#### Yury G. Kudryashov (May 17 2020 at 05:55):

Your MWE works for me in the 3.13 branch

#### Mario Carneiro (May 17 2020 at 05:55):

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

#### Mario Carneiro (May 17 2020 at 05:56):

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

#### Mario Carneiro (May 17 2020 at 06:01):

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 (May 17 2020 at 06:05):

Note that #2707 build fails somewhere in `_init`

.

#### Yury G. Kudryashov (May 17 2020 at 06:06):

I think that `has_coe_to_fun`

instance in `master`

has default priority, not 100.

#### Yury G. Kudryashov (May 17 2020 at 06:07):

BTW, it would be nice if Lean generated the `ancestor`

information for `old_structure_cmd`

classes.

#### Mario Carneiro (May 17 2020 at 06:10):

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

#### Yury G. Kudryashov (May 17 2020 at 06:16):

I think that

`has_coe_to_fun`

instance in master has default priority, not 100.

:up:

#### Mario Carneiro (May 17 2020 at 06:23):

brilliant, that did it

#### Mario Carneiro (May 17 2020 at 06:24):

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 (May 17 2020 at 06:24):

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

#### Yury G. Kudryashov (May 17 2020 at 06:25):

Currently `@[ancestor]`

attributes are used, e.g., by `to_additive`

to map functions like `group.to_monoid`

.

#### Bryan Gin-ge Chen (May 17 2020 at 06:34):

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 (May 17 2020 at 06:36):

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

#### Yury G. Kudryashov (May 17 2020 at 06:36):

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

#### Yury G. Kudryashov (May 17 2020 at 06:37):

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

#### Yury G. Kudryashov (May 17 2020 at 06:37):

(and I added one module docstring)

#### Bryan Gin-ge Chen (May 17 2020 at 06:38):

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

#### Bryan Gin-ge Chen (May 17 2020 at 06:42):

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 (May 17 2020 at 06:43):

@Simon Hudon ?

#### Yury G. Kudryashov (May 17 2020 at 06:46):

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 (May 17 2020 at 06:46):

If yes, then it needs versions of `sub`

lemmas for `int`

.

#### Bryan Gin-ge Chen (May 17 2020 at 06:49):

Adding `attribute [mono] int.sub_le_sub`

didn't help, unfortunately.

#### Bryan Gin-ge Chen (May 17 2020 at 06:59):

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 (May 17 2020 at 07:04):

Specifically: should I also add `nat.sub`

?

#### Yury G. Kudryashov (May 17 2020 at 07:08):

I think that the answer is no because `int.sub`

is `a + -b`

while `nat.sub`

is an inductive definition.

#### Bryan Gin-ge Chen (May 17 2020 at 07:12):

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 (May 17 2020 at 07:15):

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

#### Mario Carneiro (May 17 2020 at 07:15):

that is, it should not `unfold has_sub.sub`

but rather `simp only [sub_eq_add_neg]`

#### Bryan Gin-ge Chen (May 17 2020 at 07:20):

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 (May 17 2020 at 07:21):

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

#### Bryan Gin-ge Chen (May 17 2020 at 07:24):

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

#### Yury G. Kudryashov (May 17 2020 at 07:25):

In the first case I think that `simp only`

performs some computations even if you don't ask it for this.

#### Yury G. Kudryashov (May 17 2020 at 07:26):

So this `simp only [sub_eq_add_neg]`

solves the goal.

#### Gabriel Ebner (May 17 2020 at 10:42):

`simp`

will try `refl`

and `trivial`

afterwards, this might be the case here.

#### Bryan Gin-ge Chen (May 17 2020 at 15:29):

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

#### Sebastien Gouezel (May 17 2020 at 15:44):

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

#### Sebastien Gouezel (May 17 2020 at 15:45):

And will merging #2697 break #2707?

#### Sebastien Gouezel (May 17 2020 at 15:46):

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 (May 17 2020 at 15:48):

OK, let's go then.

#### Mario Carneiro (May 17 2020 at 20:13):

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 (May 17 2020 at 20:18):

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

#### Bryan Gin-ge Chen (May 17 2020 at 20:18):

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

, right?

#### Patrick Massot (May 17 2020 at 20:19):

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

#### Mario Carneiro (May 17 2020 at 20:20):

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

#### Kevin Buzzard (May 17 2020 at 20:29):

I didn't hear back from Leo

#### Kevin Buzzard (May 17 2020 at 20:29):

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

#### Patrick Massot (May 17 2020 at 20:30):

There is no license issue, this is a politeness issue

#### Mario Carneiro (May 17 2020 at 20:35):

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

#### Mario Carneiro (May 17 2020 at 20:35):

plus lean 3 is still there on `leanprover/lean`

where it has always been

#### Bryan Gin-ge Chen (May 17 2020 at 21:38):

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 (May 17 2020 at 21:40):

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

#### Bryan Gin-ge Chen (May 17 2020 at 22:30):

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 (May 17 2020 at 22:34):

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 (May 17 2020 at 22:46):

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 (May 17 2020 at 22:54):

`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 (May 17 2020 at 23:01):

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 (May 18 2020 at 00:00):

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 (May 18 2020 at 00:12):

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 (May 18 2020 at 00:13):

If you provide the type as in `@le_mul_iff_one_le_left nat _ _ _ h`

then it works

#### Mario Carneiro (May 18 2020 at 00:14):

the fact that the theorem is stated with `>`

is a red herring, it does the same thing with `<`

#### Mario Carneiro (May 18 2020 at 00:15):

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 (May 18 2020 at 00:20):

Do you know which commit broke this?

#### Mario Carneiro (May 18 2020 at 00:20):

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

#### Mario Carneiro (May 18 2020 at 00:21):

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

#### Mario Carneiro (May 18 2020 at 00:23):

`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 (May 18 2020 at 00:24):

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 (May 18 2020 at 00:27):

Ah... nat isn't imported

#### Mario Carneiro (May 18 2020 at 00:27):

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 (May 18 2020 at 00:32):

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 (May 18 2020 at 00:37):

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 (May 18 2020 at 00:44):

hm, maybe it's another instance priority mixup

#### Bryan Gin-ge Chen (May 18 2020 at 00:45):

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 (May 18 2020 at 00:46):

Does `have := (mul_self_inj_of_nonneg _ (mul_nonneg _ _)),`

work for you?

#### Bryan Gin-ge Chen (May 18 2020 at 00:47):

```
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 (May 18 2020 at 00:47):

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 (May 18 2020 at 00:48):

You could just remove the `@[simp]`

from them then.

#### Mario Carneiro (May 18 2020 at 00:48):

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 (May 18 2020 at 00:50):

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 (May 18 2020 at 00:55):

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 (May 18 2020 at 01:03):

```
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 (May 18 2020 at 01:11):

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 (May 18 2020 at 01:24):

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 (May 18 2020 at 01:26):

Will things get better in Lean 4?

#### Mario Carneiro (May 18 2020 at 01:27):

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

#### Mario Carneiro (May 18 2020 at 01:28):

The fact that everything in sight is an `old_structure_cmd`

is also a contributing factor, I think

#### Mario Carneiro (May 18 2020 at 01:28):

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

#### Mario Carneiro (May 18 2020 at 01:30):

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 (May 18 2020 at 01:30):

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 (May 18 2020 at 05:31):

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

#### Johan Commelin (May 18 2020 at 05:32):

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

#### Mario Carneiro (May 18 2020 at 05:45):

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 (May 18 2020 at 05:46):

I think #2707 is ready now

#### Yury G. Kudryashov (May 18 2020 at 06:26):

I removed some unneeded `[to_additive]`

attributes.

#### Yury G. Kudryashov (May 18 2020 at 06:27):

`to_additive`

automatically maps structure fields and projections. It needs `ancestor`

attrs to deal with `old_structure_cmd`

projections.

#### Yury G. Kudryashov (May 18 2020 at 06:27):

And it doesn't need to map `has_mul.mk`

to `has_add.mk`

because it maps prefixes, not full names.

#### Mario Carneiro (May 18 2020 at 06:29):

That's great. I don't recall when `ancestor`

was added and exactly what its scope is.

#### Mario Carneiro (May 18 2020 at 06:30):

I think lean now has hooks for adding `structure`

s, so perhaps it might even be possible to create `add_group`

itself using `to_additive`

#### Yury G. Kudryashov (May 18 2020 at 06:30):

When I was rewriting `to_additive`

, `ancestor`

was already here.

#### Yury G. Kudryashov (May 18 2020 at 06:31):

You mean adding `structure`

s with all `mk`

/`rec`

/whatever?

#### Mario Carneiro (May 18 2020 at 06:31):

I mean creating the `structure`

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

#### Mario Carneiro (May 18 2020 at 06:32):

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 (May 18 2020 at 07:45):

I think `ancestor`

was introduced for the purpose of `subtype_instance`

#### Gabriel Ebner (May 18 2020 at 08:26):

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 (May 18 2020 at 08:27):

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 (May 18 2020 at 08:31):

@Gabriel Ebner One more quesion: how do I copy an attribute like `no_rsimp`

or `ematch`

? `tactic.copy_attribute`

doesn't work.

#### Gabriel Ebner (May 18 2020 at 08:35):

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 (May 18 2020 at 08:44):

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 (May 18 2020 at 08:47):

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

#### Gabriel Ebner (May 18 2020 at 09:32):

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

#### Johan Commelin (May 18 2020 at 09:42):

I'm not aware of any

#### Sebastien Gouezel (May 18 2020 at 09:48):

Neither am I.

#### Bryan Gin-ge Chen (May 18 2020 at 14:34):

Thanks for the quick fix, Gabriel!

#### Bryan Gin-ge Chen (May 18 2020 at 14:35):

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 (May 18 2020 at 14:53):

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 (May 24 2020 at 08:22):

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 (May 24 2020 at 08:58):

If nothing in core breaks, yes

#### Mario Carneiro (May 24 2020 at 08:59):

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

Last updated: May 09 2021 at 18:17 UTC