## Stream: new members

### Topic: finset.card errors

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 20:29):

I'm confused by the error messages I get from the following examples. Namely invalid field notation, type is not of the form (C ...) on the .card.

import geometry.euclidean
import data.finset

def x : finset ℕ := {1,2,3}
example : x.card ≥ 3 :=
begin
exact le_refl 3,
end

example : {1,2,3}.card ≥ 3 := sorry

variables (M : Type) [metric_space M] (y1 y2 y3 : M)

example : {y1, y2, y3}.card ≥ 3 := sorry

def y : finset M := {y1, y2, y3}

example : y.card ≥ 3 := sorry


#### Sebastien Gouezel (Jun 19 2020 at 20:32):

example : ({1,2,3} : finset ℕ).card ≥ 3 := sorry


#### Sebastien Gouezel (Jun 19 2020 at 20:32):

Lean can not guess that you are working with a finset.

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 20:37):

Sebastien Gouezel said:

Lean can not guess that you are working with a finset.

Oh that makes sense. Thanks!

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 20:44):

Ok with that modification I'm able to resolve the second example but the last two still aren't working for me. I'm confused why card seems to like the size of a nat finset is obvious but not for a finset using elements of a metric space.

import geometry.euclidean
import data.finset

def x : finset ℕ := {1,2,3}
example : x.card ≥ 3 :=
begin
exact le_refl 3,
end

example : ({1,2,3} : finset ℕ).card ≥ 3 :=
begin
exact le_refl 3,
end

variables (M : Type) [metric_space M] (y1 y2 y3 : M)

example : ({y1, y2, y3} : finset M).card ≥ 3 := begin
exact le_refl 3,
end

def y : finset M := {y1, y2, y3}

example : y.card ≥ 3 := sorry


#### Kevin Buzzard (Jun 19 2020 at 20:45):

You need decidable equality on M to work with finsets

#### Kevin Buzzard (Jun 19 2020 at 20:46):

you can't insert constructively unless you have an algorithm for working out whether the new element is already in

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 20:59):

Kevin Buzzard said:

you can't insert constructively unless you have an algorithm for working out whether the new element is already in

How would I assert decidable equality on M and build an algorithm for appending new elements to a finset? This is in the context of euclidean geoemtry, so I don't think either of those would be an issue.

#### Kevin Buzzard (Jun 19 2020 at 20:59):

Either [decidable_eq M] everywhere, or open_locale classical at the top.

#### Kevin Buzzard (Jun 19 2020 at 21:00):

It's completely daft that this fails; the set is obviously finite, you won't be able to work out its size but that shouldn't stop you making it.

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 21:07):

Kevin Buzzard said:

It's completely daft that this fails; the set is obviously finite, you won't be able to work out its size but that shouldn't stop you making it.

I'm getting the same errors with open_locale classical and with [decidable_eq M].

I was trying to prove some geometry theorems and wanted a way to pass a certain number of points without having to specify an order. Finsets seemed like a good choice because they provided an easy way to enforce the condition of the points being distinct. Maybe this isn't worth it though if finsets don't have this kind of machinery built in yet.

#### Jalex Stark (Jun 19 2020 at 21:10):

you don't have hypotheses that that the y are distinct anywhere, so your last examples just aren't true

#### Jalex Stark (Jun 19 2020 at 21:16):

This works

import data.finset

noncomputable theory
open_locale classical

example
{α : Type*} {y1 y2 y3 : α}
(h12 : y1 ≠ y2) (h13 : y1 ≠ y3) (h23 : y2 ≠ y3) :
({y1, y2, y3} : finset α).card = 3 :=
begin
rw finset.card_insert_of_not_mem,
swap, { simp; cc },
rw finset.card_insert_of_not_mem, { simp },
simpa,
end


#### Jalex Stark (Jun 19 2020 at 21:17):

finish can do it, though it's a touch slow

#### Jalex Stark (Jun 19 2020 at 21:30):

here's "the right proof" for the case where you don't know they're equal

import data.finset
import tactic

noncomputable theory
open_locale classical

example {α : Type*} {y1 y2 y3 : α} :
({y1, y2, y3} : finset α).card ≤ 3 :=
begin
have : list.to_finset [y1, y2, y3] = ({y1, y2, y3} : finset α) := by simp,
rw ← this,
apply list.to_finset_card_le,
end


#### Jalex Stark (Jun 19 2020 at 21:32):

here it is for the case where you know they're distinct

example {α : Type*} {y1 y2 y3 : α}
(h12 : y1 ≠ y2) (h13 : y1 ≠ y3) (h23 : y2 ≠ y3) :
({y1, y2, y3} : finset α).card = 3 :=
begin
have : list.to_finset [y1, y2, y3] = ({y1, y2, y3} : finset α) := by simp,
rw ← this,
apply list.to_finset_card_of_nodup,
simp; cc
end


#### ROCKY KAMEN-RUBIO (Jun 21 2020 at 03:18):

That makes sense. The way finset is implemented is pretty unintuitive to me but this has helped a lot.

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 14:56):

Ok what if I have a finset {y1, y2, y3} and a proof h : y1 = y3. How could I use that to show {y1, y2, y3}.card = 2? It seems like there's no finset.card_insert_of_mem along with finset.card_insert_of_not_mem

#### Johan Commelin (Jun 22 2020 at 14:57):

finset.card_insert should exist

#### Jalex Stark (Jun 22 2020 at 15:06):

ROCKY KAMEN-RUBIO said:

Ok what if I have a finset {y1, y2, y3} and a proof h : y1 = y3. How could I use that to show {y1, y2, y3}.card = 2? It seems like there's no finset.card_insert_of_mem along with finset.card_insert_of_not_mem

Your statement is very close to a #mwe. If you wrap your question in an example and add the appropriate imports, you'll get more useful answers more quickly.

#### Kevin Buzzard (Jun 22 2020 at 15:07):

The cardinality could be 1

#### Jalex Stark (Jun 22 2020 at 15:10):

it's easier to notice your theorem is false after you formalize the statement. (probably the theorem you want is to replace = with \le)

#### Kevin Buzzard (Jun 22 2020 at 15:19):

import data.finset

namespace finset

lemma finset.card_insert_of_mem {α : Type*} [_inst_1 : decidable_eq α] {a : α} {s : finset α}
(h : a ∈ s) : (insert a s).card = s.card := by rw insert_eq_of_mem h

end finset


#### Kenny Lau (Jun 22 2020 at 15:21):

we have been so familiarized with indeterminates (like x y z in polynomials) that we automatically assume y1 y2 y3 are distinct

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 15:23):

Kevin Buzzard said:

The cardinality could be 1

Jalex Stark said:

it's easier to notice your theorem is false after you formalize the statement. (probably the theorem you want is to replace = with \le)

Yes! Thanks for catching that. Either that the finset is \le 2, or that it is 2 and we're given a proof that y1 \ne y2.

#3137

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 15:26):

Kevin Buzzard said:

#3137

Cool!

#### Kevin Buzzard (Jun 22 2020 at 15:30):

Note that it follows trivially from the stronger statement that if a \in s then insert a s = s, which is insert_eq_of_mem.

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 16:44):

How often do these get built? I'll just use insert_eq_of_mem for now and get back periodically.

#### Kevin Buzzard (Jun 22 2020 at 17:27):

You can watch the PR. Assuming it's uncontroversial, it might well be merged today, and then if you do leanproject up you'll have access to it. Just wait for the green "open" thing to change to a purple "merged"

#### Kevin Buzzard (Jun 22 2020 at 17:31):

some PR's can take weeks or months, if they're complicated, or half-ready and then the person working on them has to stop to work on other things. For a PR like this, there are two possibilities -- either it gets shooed through, or I'm told that the lemma shouldn't be in the library because it's a trivial consequence of a stronger lemma which is already there, namely insert_eq_of_mem.

If you want to be a pro, then you can just use it now. I pushed to the card-insert-of-mem branch of mathlib, so you can just checkout that branch, use leanproject up to get the olean files (they have been made, because it says "all checks have passed" on the PR page) and then you have it. But then you have to be careful to sort things out again properly when it gets merged into master (and of course if it doesn't get merged then you will have to unravel everything).

#### ROCKY KAMEN-RUBIO (Jun 22 2020 at 18:26):

Kevin Buzzard said:

some PR's can take weeks or months, if they're complicated, or half-ready and then the person working on them has to stop to work on other things. For a PR like this, there are two possibilities -- either it gets shooed through, or I'm told that the lemma shouldn't be in the library because it's a trivial consequence of a stronger lemma which is already there, namely insert_eq_of_mem.

If you want to be a pro, then you can just use it now. I pushed to the card-insert-of-mem branch of mathlib, so you can just checkout that branch, use leanproject up to get the olean files (they have been made, because it says "all checks have passed" on the PR page) and then you have it. But then you have to be careful to sort things out again properly when it gets merged into master (and of course if it doesn't get merged then you will have to unravel everything).

Cool! This is insightful. I think I'll just wait and update mathlib; I think changing my mathlib dependencies is ultimately going to be more difficult than refactoring my code with the update.

#### Patrick Massot (Jun 22 2020 at 18:41):

The magic command that Kevin wanted to mention is leanproject get mathlib:card-insert-of-mem

#### Kevin Buzzard (Jun 22 2020 at 18:42):

As usual, there is a problem with my two-line PR ;-)

#### Kevin Buzzard (Jun 22 2020 at 23:16):

Ok @ROCKY KAMEN-RUBIO if you type leanproject up you can use the lemma now without switching branches or doing any other git weirdness

#### ROCKY KAMEN-RUBIO (Jun 23 2020 at 19:46):

Kevin Buzzard said:

Ok ROCKY KAMEN-RUBIO if you type leanproject up you can use the lemma now without switching branches or doing any other git weirdness

Amazing, thank you!

Last updated: May 12 2021 at 05:19 UTC