## Stream: general

### Topic: What's new in mathlib

#### Johan Commelin (Oct 02 2018 at 14:08):

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 (Oct 02 2018 at 14:08):

I propose to announce other general contributions in this thread.

#### Johan Commelin (Oct 03 2018 at 07:29):

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

#### Johannes Hölzl (Oct 03 2018 at 09:32):

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 (Oct 03 2018 at 09:34):

Does that include higher than Pi^2 complexity?

#### Mario Carneiro (Oct 03 2018 at 09:35):

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

#### Mario Carneiro (Oct 03 2018 at 09:35):

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

#### Kevin Buzzard (Oct 03 2018 at 09:39):

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

#### Johannes Hölzl (Oct 03 2018 at 09:49):

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 (Oct 03 2018 at 09:50):

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 (Oct 03 2018 at 13:47):

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 (Oct 04 2018 at 13:11):

: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 (Oct 15 2018 at 16:47):

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

#### Johan Commelin (Oct 15 2018 at 16:50):

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 (Nov 01 2018 at 09:13):

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 (Nov 01 2018 at 09:13):

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 (Nov 01 2018 at 09:18):

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


:P

?

#### Kenny Lau (Nov 01 2018 at 09:19):

that's how to manually update lean

#### Keeley Hoek (Nov 01 2018 at 09:20):

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

:D

#### Kenny Lau (Nov 01 2018 at 09:21):

maybe elan is yet to work for windows

#### Keeley Hoek (Nov 01 2018 at 09:21):

nah it even has a windows binary and everything!

#### Keeley Hoek (Nov 01 2018 at 09:22):

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

#### Kenny Lau (Nov 01 2018 at 09:34):

[...]
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 (Nov 01 2018 at 09:35):

I think the old space in the name strikes again

#### Kenny Lau (Nov 01 2018 at 09:38):

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

#### Keeley Hoek (Nov 01 2018 at 09:50):

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.

#### Reid Barton (Nov 05 2018 at 14:57):

Gonna be a lot of stuff this week.

oh man

#### Johan Commelin (Nov 05 2018 at 19:25):

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

#### Keeley Hoek (Nov 06 2018 at 02:41):

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

#### Kenny Lau (Nov 06 2018 at 20:20):

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

#### Johan Commelin (Dec 17 2018 at 17:54):

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

interesting...

#### Johan Commelin (Dec 20 2018 at 08:51):

#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 (Dec 20 2018 at 08:53):

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

#### Johan Commelin (Dec 22 2018 at 17:13):

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

#### Mario Carneiro (Dec 22 2018 at 17:15):

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

#### Kevin Buzzard (Dec 22 2018 at 17:40):

https://xkcd.com/2086/

#### Patrick Massot (Dec 22 2018 at 18:14):

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 (Dec 22 2018 at 18:21):

I think most of the remaining PRs are fairly large though

#### Patrick Massot (Jan 27 2019 at 11:38):

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

Nice

#### Simon Hudon (Jan 27 2019 at 17:24):

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 (Oct 22 2019 at 10:06):

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 (Mar 03 2020 at 23:46):

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 (Mar 03 2020 at 23:47):

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 (Mar 04 2020 at 00:54):

is this the evolution of fin_cases?

#### Scott Morrison (Mar 04 2020 at 03:47):

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 (Mar 04 2020 at 03:49):

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 (Mar 04 2020 at 03:49):

fin_cases is still there, as before.

#### Sebastien Gouezel (Apr 29 2020 at 07:32):

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

#### Johan Commelin (Apr 29 2020 at 07:48):

Mathlib is almost a grown up now!

#### Kevin Buzzard (Apr 29 2020 at 08:01):

Kenny still refers to Lean as a first year undergraduate

#### Johan Commelin (Apr 29 2020 at 08:02):

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

Last updated: May 11 2021 at 23:11 UTC