Lean 3.12.0

Stream: general

[Gabriel Ebner]

As every week, I'm proud to release the latest version of the Lean community fork, Lean 3.12.0. Thanks to @Yury G. Kudryashov, @Johan Commelin, @Mario Carneiro, @Jannis Limperg! Here is the changelog:

Features:

- tactic combinators with informative results (lean#212)
- has_singleton is a new typeclass (lean#217)
- Add instances for has_repr name, has_repr case_tag, and has_to_format case_tag (lean#230)

Changes:

- library/init/function: use dot notation, add some docstrings (lean#216)
- tactic.all_goals is now called tactic.all_goals', etc. (lean#212)
- norm_num is removed (lean#224)
- Parse {a,b,c} as right associative (lean#153)
- Refactor case tags (lean#228)
- Enable pp.generalized_field_notation by default (lean#227)

[Johan Commelin]

Are there plans for bumping mathlib?

[Gabriel Ebner]

I'm currently on the segfault with lean#234

[Johan Commelin]

I'm not saying you should do it. Many people contributed to this release. Many others could also help with moving mathlib onto it.

[Johan Commelin]

Before I mess up again... what is a good branch name?

[Johan Commelin]

I could of course go for jmc-bump-to-3-12-0, but I want something a bit more professional (-;

[Johan Commelin]

#2681 is the start of a draft PR

[Jannis Limperg]

I've added commits that fix all breakage due to my Lean PRs.

[Yury G. Kudryashov]

I'll fix logic/function

[Yury G. Kudryashov]

Unless someone else is already on it

[Johan Commelin]

@Yury G. Kudryashov Please go ahead. I tried a global replace, but borked it.

[Johan Commelin]

@Yury G. Kudryashov Doesn't it need more changes in the rest of mathlib?

[Yury G. Kudryashov]

Yes, it does.

[Johan Commelin]

Can we do a smart global search replace?

[Johan Commelin]

I did things in the wrong order, and ended up replacing substrings that shouldn't have been replaced.

[Yury G. Kudryashov]

No, I want to use dot notation.

[Johan Commelin]

Aha, so it's going to be a lot of work.

[Johan Commelin]

I thought we could do that in a follow-up PR.

[Yury G. Kudryashov]

I'm looking for editable grep mode for Emacs.

[Johan Commelin]

Sorry, can't help you there. Maybe Reid can?

[Yury G. Kudryashov]

OK, let's postpone this to another PR. I'll try to make sed do the job.

[Johan Commelin]

Thanks for pushing @Yury G. Kudryashov

[Johan Commelin]

Next up is

mathlib/src/data/set/basic.lean:584:62: error: type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  {a} = {a}

[Johan Commelin]

I guess this is now because of the has_singleton stuff.

[Reid Barton]

oh boy

[Johan Commelin]

What is the best way forward?

[Johan Commelin]

theorem singleton_def (a : α) : ({a} : set α) = insert a ∅ := rfl

[Johan Commelin]

Are we going to rename such things in this PR?

[Johan Commelin]

I guess it should become singleton_eq_insert_empty_right?

[Johan Commelin]

I would like to keep this PR as small as possible, I think. And then clean up/massage in later PRs

[Johan Commelin]

I've fixed data/set/basic

[Johan Commelin]

@Yury G. Kudryashov I still get errors related to injective/surjective

[Johan Commelin]

In data.equiv.basic

[Yury G. Kudryashov]

I'm pushing one or two renames at a time.

[Yury G. Kudryashov]

singleton_def is now (insert_singleton_eq a).symm

[Yury G. Kudryashov]

Where insert_singleton_eq comes from is_lawful_singleton instance.

[Yury G. Kudryashov]

And mem_singleton_iff is now iff.rfl

[Johan Commelin]

Ok... is that better than what I did? Or does it not matter?

[Johan Commelin]

Dinner now... I'll be back later.

[Yury G. Kudryashov]

I answered before looking at your diff

[Yury G. Kudryashov]

No need to use ext

[Yury G. Kudryashov]

In finset I'm going to reuse finset.singleton for has_singleton.

[Johan Commelin]

@Yury G. Kudryashov What's the status here?

[Johan Commelin]

Something I can help with?

[Yury G. Kudryashov]

I'm working on finset. You can choose some other file.

[Johan Commelin]

@Mario Carneiro

tactic/ring.lean:106:9: warning: failed to generate bytecode for 'eval_horner'
code generation failed, VM does not have code for 'tactic.norm_num'
tactic/ring.lean:143:9: error: equation compiler failed to generate bytecode for 'eval_add._main'
nested exception message:
code generation failed, VM does not have code for 'tactic.norm_num'
tactic/ring.lean:205:9: error: equation compiler failed to generate bytecode for 'eval_neg._main'
nested exception message:
code generation failed, VM does not have code for 'tactic.norm_num'

Is this good or bad news?

[Mario Carneiro]

that's fine, tactic.ring was calling tactic.norm_num to evaluate some additions and multiplications, they just need to be redirected to the norm_num calls

[Johan Commelin]

Is this something that a human sed like me can do?

[Johan Commelin]

I guess the mere fact that tactic.norm_num still exists means that I didn't do a good job in my PR to core.

[Johan Commelin]

But it's hidden in some file about simp.

[Gabriel Ebner]

@Johan Commelin Please do not clean square rooms in a circular way: https://github.com/leanprover-community/lean/blob/aa5e30d24fefd13fb5b272522b9c08f9c5491d18/library/init/meta/simp_tactic.lean#L456

[Gabriel Ebner]

But don't worry. It's not dangerous. It will just throw an error when you call it. But it should be removed.

[Johan Commelin]

@Gabriel Ebner Yup, I also just found it.

[Johan Commelin]

Anyway, how should I fix this? What does

redirected to the norm_num calls

mean?

[Rob Lewis]

I think you can replace calls to tactic.norm_num with calls to norm_num.derive'? Or maybe derive.

[Rob Lewis]

derive' seems right.

[Johan Commelin]

Thx, let me try

[Johan Commelin]

Hmmmz, doesn't seem to help. Same error message.

[Mario Carneiro]

I'll prep a PR shortly for this. You (I) can call the internal norm_num functions and avoid some of the dispatching

[Mario Carneiro]

it also allows us to cache instances across multiple norm_num invocations in the same ring call, which we couldn't do before, so a possible performance improvement

[Johan Commelin]

For eval_neg it did help to tag on .derive'

[Rob Lewis]

Oh yeah, ignore me, I'm working on a version of mathlib like two commits before the norm_num update.

[Johan Commelin]

Is the problem that eval_add is passing on a pair, and norm_num.derive' expects a single number?

[Johan Commelin]

@Rob Lewis Ooh, it did fix 1 error (-;

[Mario Carneiro]

What's the problem with the drop in replacement of derive'?

[Mario Carneiro]

that should also work

[Johan Commelin]

I really don't understand the error:

equation compiler failed to generate bytecode for 'eval_add._main'
nested exception message:
code generation failed, VM does not have code for 'tactic.norm_num'

[Johan Commelin]

I don't see any reference to tactic.norm_num anymore

[Johan Commelin]

/me stupid

[Johan Commelin]

I missed an error higher up in the file

[Johan Commelin]

It's all fixed now. Thanks Rob and Mario!

[Johan Commelin]

Hmm, but ring is now failing in tactic.omega.eq_elim on:

tactic failed, there are unsolved goals
state:
v : ℕ → ℤ,
b : ℤ,
as : list ℤ,
n : ℕ,
h1 : 0 < get n as,
h2 : 0 = term.val v (b, as),
a_n : ℤ := get n as,
m : ℤ := a_n + 1,
h3 : m ≠ 0
⊢ (-(a_n * sgm v b as n) + sym_sym m b + coeffs.val_except n v (list.map (sym_sym m) as)) * m =
    (sym_sym m b + (coeffs.val_except n v (list.map (sym_sym m) as) - a_n * sgm v b as n)) * m

[Johan Commelin]

It's really weird, it's something that ring should easily solve.

[Johan Commelin]

Ugly fix: https://github.com/leanprover-community/mathlib/pull/2681/commits/87e05736402caefbb7febac7983992a29616c04d

[Johan Commelin]

It seems that (all?) other errors are about singleton stuff. How's that going @Yury G. Kudryashov ?

[Yury G. Kudryashov]

Almost there.

[Yury G. Kudryashov]

Fixed multiset and finset files.

[Yury G. Kudryashov]

A new inconvenience: (({a} : finset α) : set α) is no longer defeq {a}

[Bhavik Mehta]

Oof I wonder if this is gonna kill my combinatorics project... We shall see! (At least I was warned by basically everyone that this would happen)

[Yury G. Kudryashov]

I can't make a ∈ ({b} : finset α) defeq a = b because it comes from lists.

[Johan Commelin]

@Bhavik Mehta you mean

(({a} : finset α) : set α) is no longer defeq {a}
? Are you using sets that much? I thought it would all be finset...

[Bhavik Mehta]

I mean all the set and finset changes

[Johan Commelin]

Yury fixed all of mathlib in ~ 2hours

[Yury G. Kudryashov]

No, I've just fixed finset.lean

[Johan Commelin]

Oooooh..... :no_mouth:

[Yury G. Kudryashov]

This included removing finset.singleton

[Bhavik Mehta]

that's gonna hurt me

[Yury G. Kudryashov]

You just use ({a} : finset α) instead

[Yury G. Kudryashov]

ring fails in quadratic_discriminant

[Bhavik Mehta]

oh fair enough shouldn't be too bad then

[Yury G. Kudryashov]

You should PR your partial progress.

[Bryan Gin-ge Chen]

Exactly, if you'd PR'd it to mathlib then Yury would be fixing your code right now too :joy:

[Chris Hughes]

Isn't fold op [a] defeq to a now on lists. I thought there was a change at some point. So if mem was defined using fold then the defeq might work.

[Bhavik Mehta]

Yeah I know this is my fault

[Bhavik Mehta]

my real hope is that this makes singleton finsets easier to use so that some of my less pleasant proofs can actually be improved

[Yury G. Kudryashov]

But this will break a ∈ b::s defeq a = b ∨ a ∈ s.

[Johan Commelin]

I think ring is simply broken.

[Johan Commelin]

I fixed the errors in tactic/ring but I think I "broke" it at the same time.

[Johan Commelin]

@Mario Carneiro I can't fix this, I fear.

[Yury G. Kudryashov]

I fixed a few more files. Waiting for a fixed tactic/ring.

[Johan Commelin]

@Mario Carneiro Could you please take a look at ring?

[Mario Carneiro]

I'm working on it as we speak

[Johan Commelin]

Awesome

[Johan Commelin]

So I guess we should merge #2685 (new norm_num in ring) before the bump to 3.12.0

[Johan Commelin]

It's really great to see all those finset.singleton x be replaced by {x}.

[Johan Commelin]

@Mario Carneiro Do you think it makes sense to merge your PR into this bump PR already?

[Johan Commelin]

Still keep them as separate PRs, of course

[Johan Commelin]

Really, my question is: Is your PR now stable, or do you still expect a lot of changes?

[Mario Carneiro]

If it compiles I'm happy with it

[Johan Commelin]

@Yury G. Kudryashov I've merged Mario's ring fixes. Just so you know.

[Yury G. Kudryashov]

@Mario Carneiro Please have a look at this docstring

[Johan Commelin]

@Yury G. Kudryashov Oops, didn't realise you were still working on this branch

[Johan Commelin]

I just pushed some stuff

[Johan Commelin]

I'm afraid we can't really parallelise this...

[Johan Commelin]

Or maybe I will just build, and ignore the first 20 errors.

[Yury G. Kudryashov]

Or maybe I'll go eat something and work on a paper for a few hours.

[Johan Commelin]

I pushed a bit. Now it's time to break my fast.

[Yury G. Kudryashov]

Pushed determinant.

[Johan Commelin]

@Yury G. Kudryashov Are you working on this again?

[Yury G. Kudryashov]

I'll fix fractional_ideal, then make another break.

[Johan Commelin]

Ok, good

[Johan Commelin]

I pushed a fix to topology/instances/ennreal

[Yury G. Kudryashov]

Pushed ring_theory/polynomial, fixed ring_theory/adjoin locally

[Johan Commelin]

@Yury G. Kudryashov Could you look at https://github.com/leanprover-community/mathlib/pull/2681/commits/5d1e279722120258238737ca5f95edacb4a6104b

[Johan Commelin]

I don't like it

[Johan Commelin]

@Yury G. Kudryashov I've merged ring_faster again. And pushed.

[Yury G. Kudryashov]

Pushed

[Yury G. Kudryashov]

Opening borel_space

[Johan Commelin]

That's about the last thing with errors, I think

[Johan Commelin]

And something in geometry/manifold/real_instances. After that, maybe we're done :slight_smile:

[Yury G. Kudryashov]

A side effect of the singleton change: we can't do rintro rfl on (H : a ∈ {b}). We can do rintro (rfl|H) but it unfolds b.

[Johan Commelin]

Yup, I noticed this... but I think it's minor compared to all the wins that we got.

[Johan Commelin]

Hooray, Yury pushed. Are we done?

[Yury G. Kudryashov]

No

[Johan Commelin]

Oho... :sad:

[Johan Commelin]

I see... measure_theory/integration. Are you on it @Yury G. Kudryashov ? I can also do it

[Yury G. Kudryashov]

Done.

[Yury G. Kudryashov]

leanpkg build succeeded.

[Johan Commelin]

I've undrafted the PR

[Johan Commelin]

But it depends on the norm_num PR

[Yury G. Kudryashov]

Waiting for lint

[Mario Carneiro]

Yury G. Kudryashov said:

A side effect of the singleton change: we can't do rintro rfl on (H : a ∈ {b}). We can do rintro (rfl|H) but it unfolds b.

Does rintro <> work? I usually try this when rfl doesn't work

[Johan Commelin]

I think #2681 is ready

[Gabriel Ebner]

There is a merge conflict in ring.

[Johan Commelin]

Fixed