Zulip Chat Archive

Stream: general

Topic: What's new in mathlib


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

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:08):

I propose to announce other general contributions in this thread.

view this post on Zulip 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
Kudos to @Patrick Massot :tada:

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

view this post on Zulip Mario Carneiro (Oct 03 2018 at 09:34):

Does that include higher than Pi^2 complexity?

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

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

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 09:39):

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

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

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

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

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

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

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

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

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:18):

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

:P

view this post on Zulip Scott Morrison (Nov 01 2018 at 09:19):

?

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:19):

that's how to manually update lean

view this post on Zulip Keeley Hoek (Nov 01 2018 at 09:20):

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

view this post on Zulip Keeley Hoek (Nov 01 2018 at 09:20):

:D

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:21):

maybe elan is yet to work for windows

view this post on Zulip Keeley Hoek (Nov 01 2018 at 09:21):

nah it even has a windows binary and everything!

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

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

view this post on Zulip Keeley Hoek (Nov 01 2018 at 09:35):

I think the old space in the name strikes again

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:38):

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

view this post on Zulip 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.
I suppose I should stop talking about this in this thread... :o

view this post on Zulip Reid Barton (Nov 05 2018 at 14:57):

Gonna be a lot of stuff this week.

view this post on Zulip Kenny Lau (Nov 05 2018 at 15:13):

oh man

view this post on Zulip Johan Commelin (Nov 05 2018 at 19:25):

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

view this post on Zulip Keeley Hoek (Nov 06 2018 at 02:41):

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

view this post on Zulip Kenny Lau (Nov 06 2018 at 20:20):

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

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 18:00):

interesting...

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

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

view this post on Zulip Johan Commelin (Dec 22 2018 at 17:13):

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

view this post on Zulip Mario Carneiro (Dec 22 2018 at 17:15):

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

view this post on Zulip Kevin Buzzard (Dec 22 2018 at 17:40):

https://xkcd.com/2086/

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

view this post on Zulip Reid Barton (Dec 22 2018 at 18:21):

I think most of the remaining PRs are fairly large though

view this post on Zulip Patrick Massot (Jan 27 2019 at 11:38):

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

view this post on Zulip Sebastian Ullrich (Jan 27 2019 at 11:39):

Nice

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 04 2020 at 00:54):

is this the evolution of fin_cases?

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

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

view this post on Zulip Scott Morrison (Mar 04 2020 at 03:49):

fin_cases is still there, as before.

view this post on Zulip Sebastien Gouezel (Apr 29 2020 at 07:32):

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

view this post on Zulip Johan Commelin (Apr 29 2020 at 07:48):

Mathlib is almost a grown up now!

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:01):

Kenny still refers to Lean as a first year undergraduate

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