Basic cardinality calculation

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

How would I prove that {n:ℕ | n=5}.to_finset.card = 1 ? From the mathlib docs it didn't seem obvious what the definition of .card is

[Pedro Minicz]

simp does the job:

example : {n : ℕ | n = 5}.to_finset.card = 1 :=
begin
  simp
end

[Heather Macbeth]

By the way, did you know you can do {5} rather than {n : ℕ | n = 5}?

[Pedro Minicz]

By the way, you can use squeeze_simp to see what lemmas simp used to solve the goal:

example : {n : ℕ | n = 5}.to_finset.card = 1 :=
begin
  --squeeze_simp,
  simp only [set.card_singleton, set.set_of_eq_eq_singleton, set.to_finset_card]
end

[Pedro Minicz]

Heather Macbeth said:

By the way, did you know you can do {5} rather than {n : ℕ | n = 5}?

Indeed, simp was using set_of_eq_eq_singleton {a : α} : {n | n = a} = {a} to turn {n : ℕ | n = 5} into {5}, as lemmas about singleton sets are defined using that notation.

[Bjørn Kjos-Hanssen]

OK thanks... simp does that but how about {n:ℕ | n=5 ∨ n=6}.to_finset.card = 2

[Heather Macbeth]

Maybe docs#finset.card_eq_succ? (Not a library I know well, though.)

[Pedro Minicz]

{n : ℕ | n = 5 ∨ n = 6}.to_finset won't work. If you see the definition of set.to_finset the issue becomes clear:

#check set.to_finset -- set.to_finset : Π (s : set ?M_1) [_inst_1 : fintype ↥s], finset ?M_1

set.to_finset needs an instance of fintype ↥s which cannot be inferred in this case.

[Pedro Minicz]

In the first case the instance could be inferred because {n : ℕ | n = 5} = {5} and there is an instance for fintype ↥{x}.

[Pedro Minicz]

You could provide the instance:

instance : fintype ↥{n : ℕ | n = 5 ∨ n = 6} :=
sorry

but using a different notation is better (because Lean can then infer things):

example : ({5, 6} : set ℕ).to_finset.card = 2 :=
sorry

[Pedro Minicz]

{5, 6} = {n : ℕ | n = 5 ∨ n = 6 ∨ false} = {n : ℕ | n = 5 ∨ n = 6}

[Pedro Minicz]

example : ({5, 6} : set ℕ).to_finset.card = 2 :=
begin
  simp,
  refl
end

[Pedro Minicz]

Again, I'd recommend using squeeze_simp and see which lemmas where used. In VSCode you can press F12 to jump to the definition.

[Bjørn Kjos-Hanssen]

That reduced the goal to {6}.to_finset.val.card + 1 = 2 it seems... so now if I prove {6]}.to_finset.val.card = 1 we may be getting somewhere

[Pedro Minicz]

This is true by reflexivity. {6}.to_finset.val.card reduces to 1.

[Pedro Minicz]

I removed change _ = 1 + 1, as it wasn't necessary. Then the goal becomes {6}.to_finset.val.card + 1 = 2 and again, {6}.to_finset.val.card + 1 reduces to 2. They are literally the same term!

[Bjørn Kjos-Hanssen]

Ah okay, this worked... example : ({5, 6} : set ℕ).to_finset.card = 2 :=begin refl end Thanks @Pedro Minicz and @Heather Macbeth

[Heather Macbeth]

Also -- example : ({5, 6} : set ℕ).to_finset.card = 2 := rfl :smiley:

[Bjørn Kjos-Hanssen]

I'd been wondering about the difference between refl and rfl... Also, this is a bit shorter: example : ({5, 6} : finset ℕ).card = 2 := rfl

[Heather Macbeth]

refl is a tactic and rfl is a lemma, if you are in the mood for this kind of abstract nonsense.

[Heather Macbeth]

So exact rfl is the same as refl

[Heather Macbeth]

and by refl or begin refl end are the same as rfl

[Heather Macbeth]

(modulo some subtleties that other people will probably jump in to explain!)

[Kevin Buzzard]

refl (the tactic) is slightly stronger than rfl (the term) because rfl will only prove goals of the form A = A, whereas refl will close any goal of the form R A A if R is a binary relation such that there's a proof of "for all x, R x x" which has been tagged with the refl tag (tactics can look through the library for lemmas and tags, term mode proofs can't). In practice most of the time refl is used to prove A = A (at least for me) but occasionally I use it to prove x <= x or P <-> P

[Kevin Buzzard]

def R (a b : ℕ) : Prop := true

@[refl] lemma R.refl : ∀ a, R a a := λ a, trivial

example : R 37 37 :=
begin
  refl
end

[Kevin Buzzard]

or even

def R (a b : ℕ) : Prop := sorry

@[refl] lemma R.refl : ∀ a, R a a := sorry

example : R 37 37 :=
begin
  refl
end

[Kyle Miller]

Are the following instances already in mathlib?

instance emptyc.fintype (α : Type*) : fintype ({} : set α) :=
⟨∅, by simp⟩

instance insert.fintype (α : Type*) [decidable_eq α] (x : α) (s : set α) [fintype s] : fintype ↥(insert x s) :=
begin
  fsplit,
  let emb : s ↪ ↥(insert x s) :=
  { to_fun := λ ⟨a, h⟩, ⟨a, set.mem_insert_of_mem x h⟩,
    inj' := λ ⟨a,ha⟩ ⟨b,hb⟩ h, by simpa [insert.fintype._match_1] using h },
  have h : x ∈ insert x s := set.mem_insert x s,
  exact {⟨x, h⟩} ∪ finset.map emb finset.univ,
  rintro ⟨y, hy⟩,
  simp only [set.mem_insert_iff] at hy,
  rcases hy with ⟨rfl, _⟩,
  simp,
  simp [insert.fintype._match_1, hy_1],
end

[Kyle Miller]

This makes it so the following can find a fintype instance:

example : ({1,2,3} : set ℕ).to_finset.card = 3 :=
begin
  sorry,
end

[Bryan Gin-ge Chen]

Yeah, they're both in data.set.finite as src#set.fintype_empty and src#set.fintype_insert:

import data.set.finite
example : ({1,2,3} : set ℕ).to_finset.card = 3 := rfl

(I found them by going to docs#fintype, expanding the "Instances" and scrolling down to set.*.)

[Bjørn Kjos-Hanssen]

It seems that rfl (and begin refl end) can do some arithmetic too! For instance:

example : 2+2=4 :=
rfl

[Kenny Lau]

I might be wrong, but rfl is a special term, as in it is specially interpreted by the parser / elaborator.

[Kenny Lau]

as seen from the fact that if you write rfl for something that are not defeq, you get a special error message.

[Mario Carneiro]

For the most part it's just a term, but theorems of the form theorem foo : A = B := rfl (where the rhs can only be the literal token rfl) are used to mark definitional simp lemmas. It's a little restrictive but I think the idea is to substitute for some computation foo : A ~> B that doesn't otherwise have syntax in lean

[Bjørn Kjos-Hanssen]

(deleted)