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

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?

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: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

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?

PR: lean#245

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

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

I do

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?

@Mario Carneiro

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 defs.

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 defs 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


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

here

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

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)

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 (α →+* β) (α →+ β) :=

@[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 -/

#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
/-
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?

@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
/-
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):

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
(@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
(@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_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_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_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
--     (@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
--                 (@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
(@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_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
(@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
?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
?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 α
@has_le.le α (@preorder.to_has_le α
(@partial_order.to_preorder α
(@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 α
@has_le.le α (@preorder.to_has_le α
(@partial_order.to_preorder α
(@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 structures, 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 structures 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):

• 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

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

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