Zulip Chat Archive

Stream: new members

Topic: Finsets and fintypes


view this post on Zulip Donald Sebastian Leung (Apr 29 2020 at 04:29):

Is there a mathlib lemma that says if I can construct a finset α with cardinality n then fintype.card α ≥ n?

view this post on Zulip Reid Barton (Apr 29 2020 at 04:30):

I doubt it, but I am sure there are lemmas that say things like every finset is a subset of finset.univ and finset.card preserves order and finset.univ.card equals fintype.card.

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:05):

example
{α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n)
:  fintype.card α  n := begin
rw  hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:06):

example {α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n) :  fintype.card α  n :=
hX  finset.card_le_of_subset $ finset.subset_univ X

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:08):

just to check my understanding, your proof is more-or-less a mechanical translation of my tactic script into a single term? (do you think it runs noticeably faster?)

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:08):

yes; no

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 14:42):

I think that there is some overhead for entering tactic mode and some more overhead by using the rewrite command; I've noticed slowdown in scripts which use a lot of rewrites. I would be interested to know how much faster term mode is; in some sense the best argument for writing stuff in term mode is that it's faster (because it's also less readable, harder to debug, harder to write...)

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:16):

I created files which were just 10,000 copies of the term proof and the tactic proof:

import data.fintype.basic

example {α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n) :  fintype.card α  n :=
hX  finset.card_le_of_subset $ finset.subset_univ X
example {α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n) :  fintype.card α  n :=
hX  finset.card_le_of_subset $ finset.subset_univ X
example {α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n) :  fintype.card α  n :=
hX  finset.card_le_of_subset $ finset.subset_univ X
...

and

import data.fintype.basic

example
{α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n)
:  fintype.card α  n := begin
rw  hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end
example
{α : Type*} {X : finset α} {n : } [fintype α] (hX : finset.card X = n)
:  fintype.card α  n := begin
rw  hX,
apply finset.card_le_of_subset,
refine finset.subset_univ X,
end
...

and here are the timings:

buzzard@bob:~/lean-projects/xena/src/term_v_tactic$ date; lean --make tactic10000.lean; date
Wed 29 Apr 16:13:54 BST 2020
Wed 29 Apr 16:14:58 BST 2020
buzzard@bob:~/lean-projects/xena/src/term_v_tactic$ date; lean --make term10000.lean; date
Wed 29 Apr 16:15:05 BST 2020
Wed 29 Apr 16:15:11 BST 2020
buzzard@bob:~/lean-projects/xena/src/term_v_tactic$

The tactic proof took over a minute and the term proof took 6 seconds.

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:18):

The profiler also seems to indicate that the term mode proof is much faster; the tactic proof takes well over a millisecond and the tactic proof well under.

view this post on Zulip Reid Barton (Apr 29 2020 at 15:24):

surely it's worth a thousand milliseconds to not use that awful triangle, though

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:26):

I suspect it's the triangle which is saving the time; rewrite is hard work, it's a lot more than eq.subst, that's why the triangle is so awful. We should just celebrate the miracle that it actually works in this situation

view this post on Zulip Reid Barton (Apr 29 2020 at 15:27):

I agree except actually I have no idea whether these claims about timing are true. eq.subst has to work out the motive too.

view this post on Zulip Jalex Stark (Apr 29 2020 at 15:28):

Reid Barton said:

surely it's worth a thousand milliseconds to not use that awful triangle, though

compile-time optimization at any cost (just a humorous image)

view this post on Zulip Andrew Ashworth (Apr 29 2020 at 15:34):

this reminds me that we need the leftwards-pointing triangle notation for eq.substr

view this post on Zulip Andrew Ashworth (Apr 29 2020 at 15:36):

but looking forward to Lean 4, I think there's a lot of scope for making term mode a nicer environment to do proofs in... people in Agda generally are happy with programming and proving with holes. In a way I think this would be a good way to produce "fast" proofs that are reasonably easy to write

view this post on Zulip Reid Barton (Apr 29 2020 at 15:41):

Hopefully tactics will get faster in Lean 4 as well

view this post on Zulip Andrew Ashworth (Apr 29 2020 at 15:44):

Me too, but there's no getting around the fact that tactics are generally very powerful pieces of compile-time automation, and that represents work the computer has to do

view this post on Zulip Andrew Ashworth (Apr 29 2020 at 15:45):

Say what you want about Metamath, but I am impressed they manage to type-check everything in just a few seconds

view this post on Zulip Andrew Ashworth (Apr 29 2020 at 15:45):

everything being their entire body of formalized math

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:52):

Metamath is also Pollack-consistent, I learnt today

view this post on Zulip Jalex Stark (Apr 29 2020 at 15:53):

Isn't "people with Agda generally are happy with programming and proving with holes" partially explained by "agda users are more computer sciencey than mathy?"

view this post on Zulip Reid Barton (Apr 29 2020 at 15:53):

I guess I'm still not sure where the time is actually going. Is it expensive to write begin ... end? (Kevin, maybe try wrapping the term mode proofs in by exact?) Is rw intrinsically doing a lot more work than the stupid triangle, such that if the stupid triangle became a smart triangle, it would also be expensive? Or is it because parts of rw are written in Lean? Is the tactic state access of apply and refine slow? Surely these latter tactics do not do significantly more than just building the corresponding terms in term mode?

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:56):

ooh

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:56):

I just remembered that $ doesn't work in tactic mode.

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:56):

Boy that's a lot of errors

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:57):

Somehow after exact you can't use $. I never understood why not. You seem to be able to use everything else.

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:58):

$ date; lean --make byexactterm10000.lean; date
Wed 29 Apr 16:58:00 BST 2020
Wed 29 Apr 16:58:20 BST 2020

view this post on Zulip Reid Barton (Apr 29 2020 at 16:02):

So by exact already incurs 1/3 the cost

view this post on Zulip Reid Barton (Apr 29 2020 at 16:02):

and you have three tactics :thinking:

view this post on Zulip Reid Barton (May 03 2020 at 10:52):

Donald Sebastian Leung said:

Is there a mathlib lemma that says if I can construct a finset α with cardinality n then fintype.card α ≥ n?

Also I just found out why you asked this :upside_down:

view this post on Zulip Reid Barton (May 03 2020 at 10:52):

I think a more naturally-phrased form of this lemma would be good for mathlib


Last updated: May 12 2021 at 22:15 UTC