## Stream: Is there code for X?

### Topic: Subset of finset is finset

#### Robert Maxton (Oct 31 2020 at 05:32):

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 (Oct 31 2020 at 05:53):

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 (Oct 31 2020 at 05:56):

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

#### Robert Maxton (Oct 31 2020 at 05:57):

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

#### Bryan Gin-ge Chen (Oct 31 2020 at 06:11):

(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 (Oct 31 2020 at 06:12):

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 (Oct 31 2020 at 06:22):

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 (Oct 31 2020 at 12:24):

"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 (Oct 31 2020 at 13:48):

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 (Oct 31 2020 at 13:49):

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 (Oct 31 2020 at 13:50):

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

#### Johan Commelin (Oct 31 2020 at 13:50):

Can't Doron Zeilberger do that?

#### Johan Commelin (Oct 31 2020 at 13:50):

Or is this out of scope of A = B?

Not even Doron.

#### Kevin Buzzard (Oct 31 2020 at 13:50):

He can only do finite sums.

Hmmm, I see

#### Johan Commelin (Oct 31 2020 at 13:51):

I never really looked into that stuff carefully

#### Kevin Buzzard (Oct 31 2020 at 13:52):

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

#### Robert Maxton (Oct 31 2020 at 13:55):

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 (Oct 31 2020 at 13:58):

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 (Oct 31 2020 at 13:59):

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 (Oct 31 2020 at 14:01):

... 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 (Oct 31 2020 at 14:01):

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

#### Kevin Buzzard (Oct 31 2020 at 14:01):

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 (Oct 31 2020 at 14:01):

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

#### Robert Maxton (Oct 31 2020 at 14:02):

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 (Oct 31 2020 at 14:03):

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

#### Kevin Buzzard (Oct 31 2020 at 14:03):

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

#### Yury G. Kudryashov (Oct 31 2020 at 14:03):

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 (Oct 31 2020 at 14:04):

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 (Oct 31 2020 at 14:05):

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

#### Kevin Buzzard (Oct 31 2020 at 14:07):

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 (Oct 31 2020 at 14:07):

@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 (Oct 31 2020 at 14:12):

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

#### Adam Topaz (Oct 31 2020 at 14:16):

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 (Oct 31 2020 at 16:43):

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

Last updated: May 07 2021 at 19:12 UTC