how to prove this?

Stream: new members

[Joseph O]

How can I prove this goal?

α: Type
f: set α → α
B: set α := {x : α | x ∉ range f}
h: function.injective f
ξ: α
fx: f B = ξ
⊢ ξ ∈ B ↔ f B ∉ B

here is the proof so far:

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : α | x ∉ range f},
  by_contradiction,
  have : ∃ (ξ : α), f B = ξ,
  { exact exists_eq', },
  { rcases this with ⟨ξ, fx⟩,
    have : ξ ∈ B ↔ f B ∉ B,
    { sorry, },
    { rw fx at this,
      exact not_p_iff_not_p _ this, }}
end

the proof of this goal should go in the sorry
thanks in advance

[Bolton Bailey]

It's a bit easier on us if you include imports in the code section to make it an #mwe

[Bolton Bailey]

It's not clear to me that there's a simple way of doing this from here. Presumably you want to use the injectivity in some way. So you need some statement of the form f A = f B for which A is not B. But B here won't necessarily work for that: You could imagine the function f on set nat that maps finite sets to their cardinality, and infinite sets to 17. In that case every nat is in the range, so B would be the empty set. But now you can't find a collision because B is the only thing that f maps to 0.

[Eric Wieser]

Are you following a Maths proof that you already know here? It seems unlikely to me that the have... exists_eq' ... cases this is an accurate translation, as it's entirely vacuous mathematically

[Eric Wieser]

You can replace those three lines with set ξ := f B with hx

[Joseph O]

Can anyone tell me why this doesnt work?

set B := {f(x) | f(x) ∉ x ∧ x ⊆ α},

[Joseph O]

invalid '{' expression, ',', '}', '..', `//` or `|` expected

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

(f : set α → α)

[Joseph O]

Even adding type signatures didnt help

set B := {(f (x : set α)) : α| (f x) ∉ x ∧ x ⊆ α},

[Eric Wieser]

You're not allowed to put expressions to the left of | in a set literal

[Eric Wieser]

The thing to the left of | is a variable name

[Ruben Van de Velde]

I'm not sure what the expression is supposed to mean, which makes it hard to figure out what to tell lean

[Eric Wieser]

I would guess the intent is "the set of y such that there exists an x satisfying f x = y and (rest of the conditions)"

[Joseph O]

^ this

[Eric Wieser]

Well then you need to write it out like that, complete with spelling out the exists

[Joseph O]

Why? This is what I want I think

set B := {x : set α | (f x) ∉ x},

[Joseph O]

Well actually not really

[Joseph O]

Its of type set (set a), but I want it to be of type set a

[Joseph O]

seems like its counting x : set α as elements

[Eric Wieser]

Yes, because when you write {x : A | p x}, that means "I am giving you a set of As"

[Joseph O]

I need x to be some set a, and B to be a set of as where each element is not in x

[Joseph O]

Idea on how to do this?

[Ruben Van de Velde]

Do you have an English proof you can paste?

[Eric Wieser]

Joseph O said:

Idea on how to do this?

Yes, try translating this into lean, since you said it was what you meant

Eric Wieser said:

I would guess the intent is "the set of y such that there exists an x satisfying f x = y and (rest of the conditions)"

[Eric Wieser]

Your translation should include an exists symbol

[Joseph O]

Like this?

have B : ∃ y : α, ∃ x : set α, f x = y,

[Eric Wieser]

You've not include the "set of" bit

[Eric Wieser]

"the set of y: α such that ..." is spelt {y : α| ... }

[Eric Wieser]

You also should be writing B := not B :

[Joseph O]

Eric Wieser said:

"the set of y: α such that ..." is spelt {y : α| ... }

But then I can't do the x : set a part

[Eric Wieser]

Yes you can, put the ∃ x : set α inside the ...

[Joseph O]

I see

[Joseph O]

So its this

set B := {y : α | ∃ x : set α, f x = y},

[Eric Wieser]

You wanted to add ∧ (f x) ∉ x too though, right?

[Joseph O]

So far, is the math here right?

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {y : α | ∃ x : set α, f x = y ∧ f x ∉ x},
  by_contradiction,
  have : ∃ ξ : set α, ∃ τ : set α, f ξ = f τ,
  { sorry, },
  { sorry, }
end

[Eric Wieser]

The have looks like nonsense, it's obviously true (pick ξ = τ = empty) and isn't going to help with the rest of the proof

[Joseph O]

I was trying to follow the definition of injective functions

[Joseph O]

doc#function.injective

[Eric Wieser]

You should go back to your pen and paper proof and check you've translated it accurately

[Riccardo Brasca]

@Joseph O it is very very difficult to formalize some math if you haven't already understood it perfectly. Formalization, even if it is of course useful, tends to add problems rather than solving them. In particular you should first of all write a very detailed pen and paper proof.

[Alex J. Best]

Eric Wieser said:

You're not allowed to put expressions to the left of | in a set literal

Since lean#402 there is a very important special case where this is allowed though. But I don't think this is completely general

[Eric Wieser]

I remembered seeing that but had totally forgotten you needed the parens for it to work

[Kyle Miller]

It's in the file of "all the things that start with {" https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp (see parse_set_replacement)

[Kyle Miller]

Here's a way to write Joseph's set from earlier: { (f x) | (x : set α) (h : f x ∉ x) }. You can put any binders you want after the |.

[Kyle Miller]

That gets interpreted as {_x : α | ∃ (x : set α) (h : f x ∉ x), f x = _x}

[Kyle Miller]

I guess you can also use union notation to build that kind of set. ⋃ (x : set α) (h : f x ∉ x), {f x}

[Joseph O]

how would the mathematical proof for the sorry go?

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction,
  have : ∃ (ξ : α), f B' = ξ,
  { exact exists_eq'},
  { rcases this with ⟨ξ, fx⟩,
    have : f(B') ∈ B' ↔ f(B') ∉ B',
    { sorry, },
    { rw fx at this,
      exact not_p_iff_not_p _ this, } }
end

the goal is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
ξ: α
fx: f B' = ξ
⊢ f B' ∈ B' ↔ f B' ∉ B'

[Eric Wieser]

Didn't you ask exactly that question at the top of the thread? I feel like we're going in circles a bit here...

[Joseph O]

Hmm you are right, except my proof is now different. Let me go take a look again,

[Joseph O]

Eric Wieser said:

Are you following a Maths proof that you already know here? It seems unlikely to me that the have... exists_eq' ... cases this is an accurate translation, as it's entirely vacuous mathematically

Though that is how the proof went for surjective functions

[Joseph O]

But I am going to try set ξ := f B' with hx,

[Eric Wieser]

What do you mean by "how the proof went"? Which proof? Your own proof, or one you're following?

[Joseph O]

Oh sorry, so here was the proof for surjective functions

theorem cantor_surjective {α : Type} (f : α → set α) :
  ¬function.surjective f :=
begin
  set B := {x : α | x ∉ f x},
  by_contradiction,
  have : ∃ (ξ : α), f ξ = B,
  { exact h B, },
  { rcases this with ⟨ξ, fx⟩,
    have : ξ ∈ B ↔ ξ ∉ f(ξ),
    { exact mem_set_of, },
    { rw fx at this,
      exact not_p_iff_not_p _ this, }}
end

[Joseph O]

Someone told me the proof for injective functions should be very similar

[Joseph O]

Following @Eric Wieser 's suggestion in the second reply,

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction,
  set ξ := f B' with hx,
end

and this gives a goal of

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
ξ: α := f B'
hx: ξ = f B'
⊢ false

which I dont know if it makes things any better?

[Eric Wieser]

The lean code is at least short. But it sounds like your problem is that you don't know the maths proof? To make any progress there, you need to come up with something (an equality of two α terms of the form f _ = f _) to apply h to.

[Joseph O]

Eric Wieser said:

The lean code is at least short. But it sounds like your problem is that you don't know the maths proof? To make any progress there, you need to come up with something (an equality of two α terms of the form f _ = f _) to apply h to.

Does this look fine?

have : ∃ (τ : set α), f τ = ξ,

[Joseph O]

But for some reason applying h doesnt really work

[Joseph O]

I get two goals. The first one I was able to close off with exact Exists.intro B' rfl,,

[Joseph O]

The reason applying h doesnt work is because the goal is to result in false

[Joseph O]

Maybe I shouldnt do a contradiction

[Joseph O]

Here is the error and goal I get:

invalid apply tactic, failed to unify
  false
with
  ?m_1 = ?m_2
state:
α : Type,
f : set α → α,
B : set (set α) := {x : set α | f x ∉ x},
B' : set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B},
h : function.injective f,
ξ : α := f B',
hx : ξ = f B',
this : ∃ (τ : set α), f τ = ξ
⊢ false

[Yaël Dillies]

You did not make progress. You already knew that there was some \tau such that f \tau = \xi. Just take B'.

[Joseph O]

What do you mean by "just take B'"?

[Yaël Dillies]

What is the next step of the proof in words?

[Joseph O]

We have an equality of f τ = f B', and since h says that f is injective, if we apply it, we get a proof that τ = B'.

[Yaël Dillies]

Great! But you picked \tau = B' in the first place, so you did not learn anything.

[Mario Carneiro]

By the way, while the proof of cantor_surjective in mathlib is the classic one, I had not seen the proof of cantor_injective before and it was based on a proof on nLab

[Mario Carneiro]

I don't think it is easy to come up with that proof on your own (the classic proof uses inv_surj and the axiom of choice and is probably easier to guess)

[Yaël Dillies]

Hmm... I personally tried them for fun a while back and figured that both proofs were pretty similar (I only knew the surjective one and came up with the injective version myself).

[Joseph O]

Yeah they should be very similar

[Michael Jam]

I'm stuck trying to prove the following fact in lean 4:

open Classical in
example
(c : Prop)
(h : c)
(e : if c then Unit else Empty)
: e = if_pos h ▸ () :=
sorry

What's a simple way to prove this? I tried using simp and cases everywhere, but it doesn't seem to help.
Any suggestions are welcome.

[Michael Jam]

open Classical is only there so that I don't need an extra Decidable assumption.
This example came up while proving the basic laws of a discrete category.

[Kevin Buzzard]

Why would you want to forcibly insert a noncomputable decidability instance into the theorem statement rather than letting typeclass inference find its own? In Lean 3 the rule of thumb is that if the statement doesn't compile without decidability assumptions, put them in the statement; if the proof needs them, use classical assumptions. This makes lemmas maximally applicable.

As for your question, I feel like it would be easier if we had more tactics, for example convert or split_ifs. But neither of these have been ported yet :-( Can I ask for more details about how you got into this mess?

[Mario Carneiro]

open Classical in
example
(c : Prop)
(h : c)
(e : if c then Unit else Empty)
: e = if_pos h ▸ () :=
  have : Subsingleton (if c then Unit else Empty) := by
    split <;> infer_instance
  Subsingleton.elim _ _

[Kevin Buzzard]

Can you do it with s/Empty/Nat?

[Mario Carneiro]

open Classical in
example
(c : Prop)
(h : c)
(e : if c then Unit else Nat)
: e = if_pos h ▸ () := by
  generalize if_pos h = h'; revert e h'
  rw [if_pos h]; simp

[Kevin Buzzard]

Aah nice; this is somehow the "proper" proof.

[Reid Barton]

Probably you should not use if c then Unit else Nat in the first place, but rather whatever the Lean 4 spelling of plift is

[Reid Barton]

or a custom inductive family

[Mario Carneiro]

Oh, by a quirk it seems this works too:

open Classical in
theorem T
(c : Prop)
(h : c)
(e : if c then Unit else Nat)
: e = if_pos h ▸ () :=
  have : Subsingleton (if c then Unit else Nat) := by
    split <;> infer_instance
  Subsingleton.elim _ _

[Mario Carneiro]

It looks like split got confused and applied h to simplify the if in both cases, so both calls to infer_instance are proving Subsingleton Unit!

[Moahu Cheng]

Help please lean3 how to prove

theorem notPiffnotP : ¬ (P ↔ ¬ P) :=
begin
  sorry,
end

[Kevin Buzzard]

Is this homework? It comes up a lot :-)

[Kevin Buzzard]

Try the hint tactic; it might find other tactics which can solve it

[Moahu Cheng]

hint does not work :-\
it does not give me anything

[Matt Diamond]

keep in mind that ¬X in Lean means X → false

[Matt Diamond]

also you might need to import tactic.hint for hint to work

[Arien Malec]

two other hints:

1. intro h is always a good thing to try
2. understand what classical.em does

[Matt Diamond]

and tactic#by_cases!

[Kevin Buzzard]

The usual context for this question is that the student has been told to prove it constructively, which is tricky but possible. I was expecting hint to suggest tauto! which should nail it classically

[Michael Jam]

@Kevin Buzzard To give you some details, I was just making a small category library in my lean 4 playground. To make something into a diagram, I want to view a Type as a discrete category.
So the code looks like this in isolation.

namespace Category
class Hom.{u,v} (C : Type u) where
  hom : C → C → Type v
export Hom (hom)
scoped infix:10 " ⟶ " => hom

class Data (C) extends Hom C where
  comp {X Y Z : C} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
  id (X : C) : X ⟶ X
export Data (comp id)
scoped infix:80 " ≫ " => comp
scoped notation "𝟙" => id
end Category

open Category in
class Category (C) extends Data C where
  id_comp {X Y : C} : ∀ (f : X ⟶ Y), 𝟙 X ≫ f = f
  comp_id {X Y : C} : ∀ (f : X ⟶ Y), f ≫ 𝟙 Y = f
  assoc {X Y Z W : C} : ∀ (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W),
    (f ≫ g) ≫ h = f ≫ (g ≫ h)

def Empty.elim : Empty → C := fun h => nomatch h

inductive TUnit.{u} {α : Sort u} (a : α) : Type where
| unit : TUnit a

def Category.discreteCategoryOf (I) [DecidableEq I] : Category I := {
  hom := λ X Y => if X = Y then TUnit X else Empty
  comp := λ {X Y Z} (f : ite ..) (g : ite ..) =>
    show ite .. from
    have h1 : X = Y := if h : X = Y then h else (if_neg h ▸ f).elim
    have h2 : Y = Z := if h : Y = Z then h else (if_neg h ▸ g).elim
    if_pos (h1.trans h2) ▸ ⟨⟩
  id := λ X => show ite .. from if_pos rfl ▸ ⟨⟩
  id_comp := λ {X Y} (f : ite ..) =>
    if h : X = Y then by
      show if_pos h ▸ ⟨⟩ = f
      generalize if_pos h = h'; revert f h'; rw [if_pos h]
      simp
    else (if_neg h ▸ f).elim
  comp_id := λ {X Y} (f : ite ..) =>
    if h : X = Y then by
      show if_pos h ▸ ⟨⟩ = f
      generalize if_pos h = h'; revert f h'; rw [if_pos h]
      simp
    else (if_neg h ▸ f).elim
  assoc := λ {X Y Z W} f g h => rfl
}

Those proofs are probably dumb and automatable.
Many thanks to @Mario Carneiro for your generalize,revert,rw trick. I often get stuck in those kind of situations.

[Mario Carneiro]

@Michael Jam Here's what Reid was alluding to by saying you shouldn't use if c then Unit else Empty: You can express that much more nicely by using PLift c, and since it's an inductive type everything is nice by pattern matching:

def Category.discreteCategoryOf (I) : Category I where
  hom X Y := PLift (X = Y)
  comp | ⟨h1⟩, ⟨h2⟩ => ⟨h1.trans h2⟩
  id _ := ⟨rfl⟩
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

[Mario Carneiro]

and we can even drop the DecidableEq I assumption

[Kevin Buzzard]

Your definition of the morphisms is going to be super-hard to work with (as you just saw). Use plift (X = Y) (or whatever the Lean 4 equivalent is). In Lean 3 it's

/-- Universe lifting operation from Sort to Type -/
structure plift (α : Sort u) : Type u :=
up :: (down : α)

(edit: Mario got there first!)

[Michael Jam]

Right thanks, this is much simpler. I could even get rid of PLift by allowing Sort valued arrows as in lean 3's category library