finset.card errors

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

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

[Sebastien Gouezel]

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

[ROCKY KAMEN-RUBIO]

Sebastien Gouezel said:

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

Oh that makes sense. Thanks!

[ROCKY KAMEN-RUBIO]

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]

You need decidable equality on M to work with finsets

[Kevin Buzzard]

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

[ROCKY KAMEN-RUBIO]

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]

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

[Kevin Buzzard]

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]

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]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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

[ROCKY KAMEN-RUBIO]

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]

finset.card_insert should exist

[Jalex Stark]

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]

The cardinality could be 1

[Jalex Stark]

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]

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]

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]

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.

[Kevin Buzzard]

#3137

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

#3137

Cool!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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!