Finsets and fintypes

Stream: new members

[Donald Sebastian Leung]

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

[Reid Barton]

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.

[Jalex Stark]

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

[Kenny Lau]

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

[Jalex Stark]

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?)

[Kenny Lau]

yes; no

[Kevin Buzzard]

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...)

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Jalex Stark]

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)

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Reid Barton]

Hopefully tactics will get faster in Lean 4 as well

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

everything being their entire body of formalized math

[Kevin Buzzard]

Metamath is also Pollack-consistent, I learnt today

[Jalex Stark]

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?"

[Reid Barton]

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?

[Kevin Buzzard]

ooh

[Kevin Buzzard]

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

[Kevin Buzzard]

Boy that's a lot of errors

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

So by exact already incurs 1/3 the cost

[Reid Barton]

and you have three tactics :thinking:

[Reid Barton]

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:

[Reid Barton]

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