Subset of finset is finset

Stream: Is there code for X?

[Robert Maxton]

I might just be blind, but I can't seem to find an existing theorem that proves that a subset of a finset is itself a finset. (I'm also having trouble proving it myself in Lean, so suggestions in that direction would also be valuable.)

[Bryan Gin-ge Chen]

finset.has_subset is defined as a relation between two finsets:

import data.finset.basic
variables (α : Type*) (s t : finset α)
#check ((⊆) : finset α → finset α → Prop)

That is, you can't even state that s is a subset of t unless s and t are both finsets of the same type.

Can you say a little more about what you're trying to prove?

[Robert Maxton]

"Let s, t be sets s.t. s \subseteq t. Then fintype s \to fintype t."

[Robert Maxton]

... Also, how do you type fancy characters in Zulip?

[Bryan Gin-ge Chen]

(I have VS Code open and I copied and pasted the code into Zulip).

This might be a bit surprising, but the informal statement "Let s, t be sets s.t. s \subseteq t" doesn't fit well with how we formalize sets in Lean. You could either formalize the sets s and t as two different types, and then you could talk about fintype s and fintype t, but then there isn't a definition of "subset" between two arbitrary types. You could, however, provide an injective function from s to t, and then docs#fintype.of_injective says that you can get an instance of fintype s from fintype t:

import data.fintype.basic

noncomputable example (s t : Type*) (f : s → t) (hf : function.injective f) [fintype t] :
  fintype s :=
fintype.of_injective f hf

Alternatively, you could formalize s and t as two terms of type set α for some other type α, and then it makes good sense to talk about s ⊆ t and s.finite and t.finite, but this is closer to the following instead: "Let s, t be two subsets of some universal set α". If you're OK with this, then the theorem you're looking for is docs#set.finite.subset:

import data.set.finite

example (α : Type*) (s t : set α) (h : s ⊆ t) (ht : t.finite) :
  s.finite :=
ht.subset h

[Bryan Gin-ge Chen]

Note that fintypes, finsets and finite sets are all different things in Lean, there's some (very brief) discussion on this page on the community website.

[Robert Maxton]

Hmm... On general principles I kind of want to avoid using noncomputable if I don't have to, though I suppose it's not super important. I think the latter will do in my case; I'll go find out!

[Reid Barton]

"A subset of a finite set is finite" isn't true constructively for the usual notion of finite set. It needs to be decidable whether each element of the latter set is contained in the former set.

[Robert Maxton]

Huh. But, can't you argue that since the cardinality of a subset is bounded above by the cardinality of the original set, if the original set is finite then the subset must be as well? It isn't a "constructive proof" in the sense that it tells you what the actual members of the subset are, but I didn't think that constructive-logic forbade 'proving existence without giving an example' in general... (not that constructivist logic is my specialty or anything)

[Kevin Buzzard]

you can't compute the cardinality of a finite set. What's the cardinality of $\{\sum_{n=1}^{\infty}\frac{1}{n^2}, \pi^2/6\}$?

[Kevin Buzzard]

You'll need to figure out if the infinite sum equals $\pi^2/6$ and there's no algorithm for that

[Johan Commelin]

Can't Doron Zeilberger do that?

[Johan Commelin]

Or is this out of scope of A = B?

[Kevin Buzzard]

Not even Doron.

[Kevin Buzzard]

He can only do finite sums.

[Johan Commelin]

Hmmm, I see

[Johan Commelin]

I never really looked into that stuff carefully

[Kevin Buzzard]

If you don't like the example, there are more to choose from here.

[Robert Maxton]

Well, okay. That saves me some bother, since it basically proves the thing I want to do can't be done without noncomputable lol. Thanks!

[Yury G. Kudryashov]

If you have s ⊆ t, fintype t, and ∀ x, decidable (x ∈ s), then you can get fintype s without noncomputable, see docs#set.fintype_subset.

[Robert Maxton]

Yeah, but I'm trying to prove that an arbitrary subset of a finite group is finite, so I don't think that I can assume ∀ x, decidable (x ∈ s)...

[Robert Maxton]

... though actually, in my specific case, maybe it is decidable. Hm. It's not quite arbitrary -- I'm trying to prove that the conjugacy classes in specific are finite (and furthermore there's finitely many of them), so I can prove the class equation. And there is a perfectly decidable way to check that.

[Robert Maxton]

Okay, I'll poke at it some more then.

[Kevin Buzzard]

I assume that all the time when I'm doing normal mathematics. I write open_locale classical at the top of my file and bingo, everything is decidable. If you're doing classical mathematics then this is taken as read.

[Yury G. Kudryashov]

You have two choices: (a) use docs#set.finite and docs#set.finite_of_fintype; (b) add [decidable ...] assumptions to your theorems.

[Robert Maxton]

I guess that begs the question -- how careful are we about avoiding noncomputable results in library code? I get the impression we'd prefer to avoid it whenever possible, but how hard are we trying?

[Kevin Buzzard]

oh you've got the wrong end of the stick entirely. We are very happy to work classically in mathlib.

[Kevin Buzzard]

It's the reason we have so much mathematics in there.

[Yury G. Kudryashov]

If you want to use (b), then note that in mathlib we only add [decidable ..] assumptions if they're required to state the theorem, not to prove it.

[Kevin Buzzard]

Polynomials used to be computable, which made them good for computations, but people found them hard to use, so now they're noncomputable, and easier to work with when it comes to proofs.

[Robert Maxton]

Psht. Alright then, I won't worry about it too much if I can't make this work without noncomputable

[Kevin Buzzard]

The Gonthier et al proof of the odd order theorem was done completely constructively, as I understand it; but in practice there is only so far you can do with constructive mathematics, and it's not even clear to me that you can get particularly far into an undergraduate maths degree without jumping through innumerable hoops. In mathlib we treat mathematics the way working mathematicians treat it and work classically the moment we run into issues like this.

[Yury G. Kudryashov]

@Kevin Buzzard Sometimes adding [decidable] assumptions to lemmas make them more useful in classical context because otherwise sometimes you get different [decidable] instances in LHS and RHS.

[Robert Maxton]

Somewhat unrelatedly, is there a way to make Lean generate new goals for unfulfilled type class witnesses, instead of just complaining?

[Adam Topaz]

we have all these fooI tactics. One of them might do what you want. At the very least you can do, for example

...
have : group G, by sorry,
letI := this,
...

[Yury G. Kudryashov]

Another trick: refine @my_thm _ (id _).