Zulip Chat Archive

Stream: general

Topic: preparing for lean-3.13.0


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

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

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

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

view this post on Zulip Reid Barton (May 16 2020 at 14:45):

My guess would be that the goal after dsimp changed somehow

view this post on Zulip Johan Commelin (May 16 2020 at 14:45):

Probably, yes

view this post on Zulip Johan Commelin (May 16 2020 at 14:45):

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

view this post on Zulip Reid Barton (May 16 2020 at 14:46):

Not easily at the moment

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

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

view this post on Zulip Johan Commelin (May 16 2020 at 14:46):

So yes, dsimp changed.

view this post on Zulip Johan Commelin (May 16 2020 at 14:48):

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

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

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

view this post on Zulip Gabriel Ebner (May 16 2020 at 15:08):

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

view this post on Zulip Johan Commelin (May 16 2020 at 18:03):

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

view this post on Zulip Gabriel Ebner (May 16 2020 at 18:03):

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

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

view this post on Zulip Johan Commelin (May 16 2020 at 18:04):

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

view this post on Zulip Gabriel Ebner (May 16 2020 at 18:05):

Yes!

view this post on Zulip Johan Commelin (May 16 2020 at 18:18):

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

view this post on Zulip Johan Commelin (May 16 2020 at 18:18):

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

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

view this post on Zulip Johan Commelin (May 16 2020 at 18:28):

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

view this post on Zulip Johan Commelin (May 16 2020 at 18:43):

Hooray! This branch compiles :tada:

view this post on Zulip Johan Commelin (May 16 2020 at 18:59):

What's left is sorting out the copyright stuff.

view this post on Zulip Johan Commelin (May 16 2020 at 18:59):

I'll leave that to others

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:09):

I emailed Leo but didn't hear back yet

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

view this post on Zulip Johan Commelin (May 16 2020 at 19:38):

@Bryan Gin-ge Chen Thanks!

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

view this post on Zulip Mario Carneiro (May 16 2020 at 22:10):

int.int.sub_self?

view this post on Zulip Mario Carneiro (May 16 2020 at 22:10):

also int.int.eq_zero_or_eq_zero_of_mul_eq_zero

view this post on Zulip Mario Carneiro (May 16 2020 at 22:10):

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

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

view this post on Zulip Mario Carneiro (May 16 2020 at 22:15):

and probably lint cleanups should be delayed until then

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

view this post on Zulip Mario Carneiro (May 16 2020 at 22:16):

It's mentioned by name in the mk_protected call

view this post on Zulip Mario Carneiro (May 16 2020 at 22:16):

it's in core

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 22:19):

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

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 22:22):

Should I release 3.13.1 with those fixed?

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 22:27):

PR: lean#245

view this post on Zulip Mario Carneiro (May 16 2020 at 22:27):

what about the protected definitions?

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 22:28):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 22:29):

I do

view this post on Zulip Mario Carneiro (May 16 2020 at 22:29):

Johan has conveniently already made a list

view this post on Zulip Bryan Gin-ge Chen (May 16 2020 at 22:29):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 22:30):

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 00:30):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 01:09):

@Mario Carneiro

view this post on Zulip Mario Carneiro (May 17 2020 at 01:11):

they are aliases

view this post on Zulip Mario Carneiro (May 17 2020 at 01:11):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 01:12):

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 01:13):

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 01:46):

I just added a comment there.

view this post on Zulip Mario Carneiro (May 17 2020 at 02:20):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 02:20):

mathlib has alias for this sort of thing

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 03:06):

Great, I'll move forward then.

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 04:15):

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

view this post on Zulip Johan Commelin (May 17 2020 at 05:22):

Thanks! Sorry for the double namespace issue.

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

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

view this post on Zulip Mario Carneiro (May 17 2020 at 05:49):

MWE:

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:50):

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:51):

Somehow it prefers the transitive instance to the explicit has_coe_to_fun.

view this post on Zulip Mario Carneiro (May 17 2020 at 05:51):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 05:51):

are you getting the transitive instance?

view this post on Zulip Alex J. Best (May 17 2020 at 05:52):

Works for me in mathlib from 5 days ago

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:52):

In current master: no

view this post on Zulip Mario Carneiro (May 17 2020 at 05:53):

where is the has_coe_to_fun instance?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:53):

In algebra.ring

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:54):

here

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:55):

Your MWE works for me in the 3.13 branch

view this post on Zulip Mario Carneiro (May 17 2020 at 05:55):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 05:56):

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

view this post on Zulip 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*} { : semiring α} { : semiring β} : has_coe_to_fun (α →+* β) :=
⟨_, ring_hom.to_fun

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

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

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:05):

Note that #2707 build fails somewhere in _init.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:06):

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

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

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

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

view this post on Zulip Mario Carneiro (May 17 2020 at 06:23):

brilliant, that did it

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

view this post on Zulip Mario Carneiro (May 17 2020 at 06:24):

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

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

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:36):

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:36):

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

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:37):

(and I added one module docstring)

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 06:38):

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 06:43):

@Simon Hudon ?

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 06:46):

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 06:49):

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 07:04):

Specifically: should I also add nat.sub?

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

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

view this post on Zulip Mario Carneiro (May 17 2020 at 07:15):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 07:21):

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

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

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 07:26):

So this simp only [sub_eq_add_neg] solves the goal.

view this post on Zulip Gabriel Ebner (May 17 2020 at 10:42):

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 15:29):

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

view this post on Zulip Sebastien Gouezel (May 17 2020 at 15:44):

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

view this post on Zulip Sebastien Gouezel (May 17 2020 at 15:45):

And will merging #2697 break #2707?

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 15:48):

OK, let's go then.

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

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

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

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

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 20:29):

I didn't hear back from Leo

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

view this post on Zulip Patrick Massot (May 17 2020 at 20:30):

There is no license issue, this is a politeness issue

view this post on Zulip Mario Carneiro (May 17 2020 at 20:35):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 20:35):

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

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

view this post on Zulip Rob Lewis (May 17 2020 at 21:40):

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

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

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

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

-/

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

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

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

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

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

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

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

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 00:20):

Do you know which commit broke this?

view this post on Zulip Mario Carneiro (May 18 2020 at 00:20):

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

view this post on Zulip Mario Carneiro (May 18 2020 at 00:21):

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

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

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

view this post on Zulip Mario Carneiro (May 18 2020 at 00:27):

Ah... nat isn't imported

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

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

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

view this post on Zulip Mario Carneiro (May 18 2020 at 00:44):

hm, maybe it's another instance priority mixup

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

view this post on Zulip Mario Carneiro (May 18 2020 at 00:46):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 00:48):

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

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

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

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

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

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

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

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 01:26):

Will things get better in Lean 4?

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

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

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

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

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

view this post on Zulip Johan Commelin (May 18 2020 at 05:31):

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

view this post on Zulip Johan Commelin (May 18 2020 at 05:32):

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

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

view this post on Zulip Mario Carneiro (May 18 2020 at 05:46):

I think #2707 is ready now

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 06:26):

I removed some unneeded [to_additive] attributes.

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

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

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

view this post on Zulip Mario Carneiro (May 18 2020 at 06:30):

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

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 06:30):

When I was rewriting to_additive, ancestor was already here.

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 06:31):

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

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

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

view this post on Zulip Patrick Massot (May 18 2020 at 07:45):

I think ancestor was introduced for the purpose of subtype_instance

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

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

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

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

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

view this post on Zulip Sebastien Gouezel (May 18 2020 at 08:47):

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

view this post on Zulip Gabriel Ebner (May 18 2020 at 09:32):

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

view this post on Zulip Johan Commelin (May 18 2020 at 09:42):

I'm not aware of any

view this post on Zulip Sebastien Gouezel (May 18 2020 at 09:48):

Neither am I.

view this post on Zulip Bryan Gin-ge Chen (May 18 2020 at 14:34):

Thanks for the quick fix, Gabriel!

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

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

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

view this post on Zulip Mario Carneiro (May 24 2020 at 08:58):

If nothing in core breaks, yes

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