## Stream: Is there code for X?

### Topic: Basic cardinality calculation

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 21:38):

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 (Oct 10 2020 at 21:42):

simp does the job:

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


#### Heather Macbeth (Oct 10 2020 at 21:43):

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

#### Pedro Minicz (Oct 10 2020 at 21:43):

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 (Oct 10 2020 at 21:45):

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 (Oct 10 2020 at 21:45):

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

#### Heather Macbeth (Oct 10 2020 at 21:50):

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

#### Pedro Minicz (Oct 10 2020 at 21:50):

{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 (Oct 10 2020 at 21:51):

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

#### Pedro Minicz (Oct 10 2020 at 21:55):

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 (Oct 10 2020 at 21:55):

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

#### Pedro Minicz (Oct 10 2020 at 21:57):

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


#### Pedro Minicz (Oct 10 2020 at 21:58):

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 (Oct 10 2020 at 21:59):

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 (Oct 10 2020 at 21:59):

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

#### Pedro Minicz (Oct 10 2020 at 22:00):

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 (Oct 10 2020 at 22:05):

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

#### Heather Macbeth (Oct 10 2020 at 22:10):

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

#### Bjørn Kjos-Hanssen (Oct 10 2020 at 22:38):

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 (Oct 10 2020 at 22:38):

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

#### Heather Macbeth (Oct 10 2020 at 22:39):

So exact rfl is the same as refl

#### Heather Macbeth (Oct 10 2020 at 22:39):

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

#### Heather Macbeth (Oct 10 2020 at 22:40):

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

#### Kevin Buzzard (Oct 10 2020 at 22:47):

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 (Oct 10 2020 at 22:50):

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 (Oct 10 2020 at 22:52):

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 (Oct 10 2020 at 23:18):

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 (Oct 10 2020 at 23:24):

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 (Oct 11 2020 at 00:25):

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 (Oct 11 2020 at 02:16):

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

example : 2+2=4 :=
rfl


#### Kenny Lau (Oct 11 2020 at 04:27):

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

#### Kenny Lau (Oct 11 2020 at 04:28):

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

#### Mario Carneiro (Oct 11 2020 at 05:30):

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 (Oct 16 2020 at 20:14):

(deleted)

Last updated: May 19 2021 at 02:10 UTC