What's new in mathlib

Stream: general

[Johan Commelin]

There is a thread in the #maths stream: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/What's.20new.20in.20Lean.20maths.3F
It is a place to announce recent merges to mathlib that have clear mathematical relevance.

[Johan Commelin]

I propose to announce other general contributions in this thread.

[Johan Commelin]

There is now a choice tactic that will help with applying the axiom of choice: https://github.com/leanprover/mathlib/blob/c2df6b1f3f62575649dbe128a2c5fc9e2de26ffb/docs/tactics.md#choice
Kudos to @Patrick Massot :tada:

[Johannes Hölzl]

I changed the syntax to

choose a b h using show ∀ (y : Y), ∃ (a : A) (b : B), f a b = y, ...

Also it allows a arbitrary prefix of quantifiers and existentials.

[Mario Carneiro]

Does that include higher than Pi^2 complexity?

[Mario Carneiro]

i.e. after the first choose you might end up with a hypothesis that is again of the form AE and repeat

[Mario Carneiro]

(I'm not sure how applicable this is, but it would be nice to say we have full skolemization)

[Kevin Buzzard]

"Mathlib: aiming for full skolemization". I think this should be our catch phrase.

[Johannes Hölzl]

It should handle quantifiers again. But problem is that it doesn't handle conjunctions currently.

example (h : ∀n m : ℕ, ∃i, ∀n:ℕ, ∃j, m = n + i ∨ m + j = n) : true :=
begin
  choose i j h using h,
  guard_hyp i := ℕ → ℕ → ℕ,
  guard_hyp j := ℕ → ℕ → ℕ → ℕ,
  guard_hyp h := ∀ (n m n_1 : ℕ), m = n_1 + i n m ∨ m + j n m n_1 = n_1,
  trivial
end

[Johannes Hölzl]

also, since it doesn't use axiom_of_choice but classical.some it can be used in Type and not only in Prop.

[Patrick Massot]

Oh, I just noticed https://github.com/leanprover/mathlib/pull/383#issuecomment-426571007 it means I don't need set_option pp.beta true in my demo file anymore

[Johan Commelin]

:bell: We have a new pair of tactics: tfae_have and tfae_finish. The help with proving "the following are equivalent".
Take a look at https://github.com/leanprover/mathlib/blob/b7d314f3f2f4b18a491b359aaeb889b5c83640bc/data/list/basic.lean#L3890 and at https://github.com/leanprover/mathlib/blob/b7d314f3f2f4b18a491b359aaeb889b5c83640bc/docs/tactics.md#tfae

[Johan Commelin]

There have been valiant efforts by the community to improve the installation experience: https://github.com/leanprover/mathlib/commit/4dbe0cdfaee201cc15cd2a74fbe8731f8bd4642a

[Johan Commelin]

In this context I think it is worth pointing once more to Kevin's page: https://xenaproject.wordpress.com/installing-lean-and-mathlib/ which also links to two fantastic installation walkthrough videos by Scott.

[Scott Morrison]

New in Lean itself: the patches to deal with spaces in Windows user names have landed, https://github.com/leanprover/lean-nightly/releases.

[Scott Morrison]

In mathlib, my fin_cases tactic was merged. Sorry I haven't been paying attention to mathlib much recently; perhaps someone else can give some updates on recent merges?

[Kenny Lau]

cd /c/lean
git pull
cd build/release
ninja clean-olean
ninja

:P

[Scott Morrison]

?

[Kenny Lau]

that's how to manually update lean

[Keeley Hoek]

but kenny, this means you are yet to bask in the glorious elan way

[Keeley Hoek]

:D

[Kenny Lau]

maybe elan is yet to work for windows

[Keeley Hoek]

nah it even has a windows binary and everything!

[Keeley Hoek]

there is even scope for like a windows installer, but someone will have to be bothered to repair it

[Kenny Lau]

[...]
Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation


error: toolchain 'stable' is not installed
info: caused by: not a directory: 'C:\Users\Kenny Lau\.elan\toolchains\stable'

Press the Enter key to continue.

[Keeley Hoek]

I think the old space in the name strikes again

[Kenny Lau]

I think the correct name is stable-x86_64-pc-windows-msvc not stable

[Keeley Hoek]

Is that because there was a folder created in ...\toolchains\ which is called that? How did you get that name?
My understanding of the elan toolchain code is that stable is a special keyword, along with nightly. In my testing I tend to get the error error: toolchain 'stable' is not installed when elan is failing silently because of something.
I suppose I should stop talking about this in this thread... :o

[Reid Barton]

Gonna be a lot of stuff this week.

[Kenny Lau]

oh man

[Johan Commelin]

Keeley's PR's for extending conv mode with ring and erw have been merged.

[Keeley Hoek]

Woah, the pull-request list fits onto one page now!

[Kenny Lau]

https://math.stackexchange.com/q/2987631/328173

[Johan Commelin]

We just got elide: https://github.com/leanprover/mathlib/blob/ebf3008ba84fec5363334fa77a947f43bd71a965/docs/tactics.md#elideunelide
Thanks Mario!

[Kenny Lau]

interesting...

[Johan Commelin]

#489 is merged. This adds a new command #where. Kudos to @Keeley Hoek :tada:
If you insert #where in a file, Lean will print a message explaining what your current namespace is, and which variables are in use.

[Keeley Hoek]

Mario needs a medal (or at least a high-five) for the insane response time after I fixed up his suggestions

[Johan Commelin]

34 merged PRs in the past week!
https://github.com/leanprover/mathlib/pulse

[Mario Carneiro]

and I'm sure there are more open PRs now than when I started :P

[Kevin Buzzard]

https://xkcd.com/2086/

[Patrick Massot]

and I'm sure there are more open PRs now than when I started :P

You did ask for many small PR everywhere there could be one big...

[Reid Barton]

I think most of the remaining PRs are fairly large though

[Patrick Massot]

Simon wrote a bunch of long expected hole commands https://github.com/leanprover/mathlib/commit/84d1c450111d4c576c7aefd3a7901c4aa07d0b6f!

[Sebastian Ullrich]

Nice

[Simon Hudon]

I hope you guys enjoy it! There's a lot of room for improvement. Please let me know what the pain points are.

[Scott Morrison]

There's a new tactic suggest, that I'd encourage everyone to try out. Like library_search, it attempts to find a useful lemma from the imported library to close the current goal. It prints a list of everything (up to some cutoff) that it finds, even if they don't completely close the goal. Thus you'll sometimes see results of the form exact ..., but also refine ... with underscores for new goals.

(This is joint work with a student Lucas Allen at the ANU.)

Bug reports, or suggestions for improvements in its behaviour, very welcome. There's still a lot of low-hanging fruit in this direction.

[Scott Morrison]

interval_cases has landed in mathlib. It's good for situations where you know n < 3, and just want to be given the cases n = 0, n=1, and n=2 to deal with separately.

Just call it as interval_cases n, and it will automatically look for appropriate bounds.

[Scott Morrison]

It currently works with a variable in nat, int, or pnat: it's not so hard to add support for others, so please let me know if there are specific other types that would be useful to you.

[Mario Carneiro]

is this the evolution of fin_cases?

[Scott Morrison]

Yes, under the hood it is just assembling the pieces into a new hypotheses n \mem set.Ico a b, and then calling fin_cases on that.

[Scott Morrison]

So as long as there is a fintype (set.Ico a b) instance available for a type, this has a chance of working. It needs some lattice-type instances in order to combine multiple bounds if they appear, and to automatically find lower bounds for e.g. nat.

[Scott Morrison]

fin_cases is still there, as before.

[Sebastien Gouezel]

The inverse function theorem #2228 has been merged. Thanks @Yury G. Kudryashov !

[Johan Commelin]

Mathlib is almost a grown up now!

[Kevin Buzzard]

Kenny still refers to Lean as a first year undergraduate

[Johan Commelin]

Hmmm... and most of those aren't grown up :oops:

[Yury G. Kudryashov]

Let me revive this topic with the Divergence thm for a Henstock-style integral, see docs#box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at

[Yury G. Kudryashov]

A version for the Bochner integral #9811 is awaiting review.