# Zulip Chat Archive

## Stream: maths

### Topic: Cantor golf

#### Kevin Buzzard (Dec 12 2018 at 16:42):

1) Is there a very short proof of this in Lean / mathlib?

example (X : Type) (x : X) (f : X → set X) (H : x ∈ f x ↔ x ∉ f x) : false := sorry

2) Can anyone golf the mathlib proof of Cantor's Diagonal Argument (using only imports in mathlib):

theorem cantor_surjective {α} (f : α → α → Prop) : ¬ function.surjective f | h := let ⟨D, e⟩ := h (λ a, ¬ f a a) in (iff_not_self (f D D)).1 $ iff_of_eq (congr_fun e D)

#### Rob Lewis (Dec 12 2018 at 16:44):

For 1), `by tauto!`

It shouldn't need classical logic but `by tauto`

fails.

#### Kevin Buzzard (Dec 12 2018 at 16:44):

My answer to (1):

example (X : Type) (x : X) (f : X → set X) (H : x ∈ f x ↔ x ∉ f x) : false := begin revert H, generalize : x ∈ f x = p, cc end

I'm sure something much better will exist.

#### Kevin Buzzard (Dec 12 2018 at 16:44):

...and indeed it existed before I even posted! Many thanks Rob!

#### Kevin Buzzard (Dec 12 2018 at 16:54):

Why my code no work?

import tactic.interactive open function theorem no_bijection_to_power_set' (X : Type) (f : X → set X) : bijective f → false := λ ⟨Hi, Hs⟩, -- unexpected occurrence of recursive function error begin cases Hs {x : X | x ∉ f x} with x Hx, have Hconclusion_so_far : x ∈ f x ↔ x ∈ _ := by rw [Hx], have Hlogical_nonsense : (x ∈ f x) ↔ ¬ (x ∈ f x) := Hconclusion_so_far, tauto! end

#### Kevin Buzzard (Dec 12 2018 at 16:58):

Changing `tauto!`

to `sorry`

fixes the error. Is it a combination of the equation compiler and the tactic? Why is this happening?

#### Kevin Buzzard (Dec 12 2018 at 16:59):

import tactic.interactive open function theorem no_bijection_to_power_set' (X : Type) (f : X → set X) : bijective f → false := λ Hb, let ⟨Hi,Hs⟩ := Hb in -- unexpected occurrence of recursive function begin cases Hs {x : X | x ∉ f x} with x Hx, have Hconclusion_so_far : x ∈ f x ↔ x ∈ _ := by rw [Hx], have Hlogical_nonsense : (x ∈ f x) ↔ ¬ (x ∈ f x) := Hconclusion_so_far, tauto! end

Also doesn't work.

#### Reid Barton (Dec 12 2018 at 16:59):

For some reason using lambda with pattern matching like this makes a hypothesis (I think it's called `_fun_match`

) which I guess represents some kind of recursion

#### Reid Barton (Dec 12 2018 at 17:00):

if you use a tactic which tries to apply everything like `tauto`

, it'll try to apply `_fun_match`

and then you get this error

#### Reid Barton (Dec 12 2018 at 17:01):

Same with let but I think the hypothesis name is different

#### Reid Barton (Dec 12 2018 at 17:01):

You could use `begin rintros \<Hi,Hs\>, cases ...`

#### Kevin Buzzard (Dec 12 2018 at 17:32):

I was trying to get out of tactic mode, on this occasion.

#### Kevin Buzzard (Dec 12 2018 at 17:35):

Here's the game. I have a version of Cantor's theorem in Lean, spelt out so that mathematicians with epsilon Lean experience can still understand it:

-- Cantor's theorem in Lean import tactic.interactive open function /- Theorem: If X is any type, then there is no bijective function f from X to the power set of X. -/ theorem no_bijection_to_power_set (X : Type) : ∀ f : X → set X, ¬ (bijective f) := begin -- Let f be a function from X to the power set of X intro f, -- Assume, for a contradiction, that f is bijective intro Hf, -- f is bijective, so it's surjective. cases Hf with Hi Hs, -- it's also injective, but I don't even care clear Hi, -- Let S be the usual cunning set let S : set X := {x : X | x ∉ f x}, -- What does surjectivity of f say when applied to S? have HCantor := Hs S, -- It tells us that there's x in X with f x = S! cases HCantor with x Hx, -- That means x is in f x if and only if x has is in S. have Hconclusion_so_far : x ∈ f x ↔ x ∈ S := by rw [Hx], -- but this means (x ∈ f x) ↔ ¬ (x ∈ f x) have Hlogical_nonsense : (x ∈ f x) ↔ ¬ (x ∈ f x) := Hconclusion_so_far, -- automation can now take over. tauto!, end

and I was trying to compress it into a term mode function.

I also have the mathlib proof

import tactic.interactive theorem cantor_surjective {α} (f : α → α → Prop) : ¬ function.surjective f | h := let ⟨D, e⟩ := h (λ a, ¬ f a a) in (iff_not_self (f D D)).1 $ iff_of_eq (congr_fun e D)

and I was attempting to expand this into a tactic mode proof. I could just use rcases, as you say.

#### Rob Lewis (Dec 12 2018 at 18:14):

You can use `simpa using Hlogical_nonsense`

to avoid the weird `tauto`

behavior, but I guess it doesn't look quite as good when you have to name the hypothesis.

Last updated: May 14 2021 at 20:13 UTC