Zulip Chat Archive

Stream: maths

Topic: Cantor golf


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

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:44):

For 1), by tauto!It shouldn't need classical logic but by tauto fails.

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

view this post on Zulip Kevin Buzzard (Dec 12 2018 at 16:44):

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

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

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

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

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

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

view this post on Zulip Reid Barton (Dec 12 2018 at 17:01):

Same with let but I think the hypothesis name is different

view this post on Zulip Reid Barton (Dec 12 2018 at 17:01):

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

view this post on Zulip Kevin Buzzard (Dec 12 2018 at 17:32):

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

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

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