Zulip Chat Archive

Stream: Is there code for X?

Topic: Basic cardinality calculation


view this post on Zulip 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

view this post on Zulip Pedro Minicz (Oct 10 2020 at 21:42):

simp does the job:

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

view this post on Zulip Heather Macbeth (Oct 10 2020 at 21:43):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Oct 10 2020 at 21:50):

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

view this post on Zulip 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.

view this post on Zulip 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}.

view this post on Zulip 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

view this post on Zulip Pedro Minicz (Oct 10 2020 at 21:55):

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

view this post on Zulip Pedro Minicz (Oct 10 2020 at 21:57):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pedro Minicz (Oct 10 2020 at 21:59):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Oct 10 2020 at 22:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Oct 10 2020 at 22:39):

So exact rfl is the same as refl

view this post on Zulip Heather Macbeth (Oct 10 2020 at 22:39):

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

view this post on Zulip Heather Macbeth (Oct 10 2020 at 22:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.*.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Oct 16 2020 at 20:14):

(deleted)


Last updated: May 19 2021 at 02:10 UTC