Zulip Chat Archive

Stream: new members

Topic: how to prove this?


Joseph O (May 01 2022 at 02:17):

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 (May 01 2022 at 04:17):

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

Bolton Bailey (May 01 2022 at 05:09):

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 (May 01 2022 at 08:53):

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 (May 01 2022 at 08:55):

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

Joseph O (May 01 2022 at 14:01):

Can anyone tell me why this doesnt work?

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

Joseph O (May 01 2022 at 14:01):

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

Notification Bot (May 01 2022 at 14:03):

Joseph O has marked this topic as unresolved.

Joseph O (May 01 2022 at 14:03):

(f : set α → α)

Joseph O (May 01 2022 at 14:14):

Even adding type signatures didnt help

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

Eric Wieser (May 01 2022 at 14:18):

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

Eric Wieser (May 01 2022 at 14:18):

The thing to the left of | is a variable name

Ruben Van de Velde (May 01 2022 at 14:19):

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

Eric Wieser (May 01 2022 at 14:21):

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 (May 01 2022 at 14:33):

^ this

Eric Wieser (May 01 2022 at 14:34):

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

Joseph O (May 01 2022 at 14:35):

Why? This is what I want I think

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

Joseph O (May 01 2022 at 14:37):

Well actually not really

Joseph O (May 01 2022 at 14:37):

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

Joseph O (May 01 2022 at 14:38):

seems like its counting x : set α as elements

Eric Wieser (May 01 2022 at 14:38):

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

Joseph O (May 01 2022 at 14:40):

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 (May 01 2022 at 14:44):

Idea on how to do this?

Ruben Van de Velde (May 01 2022 at 14:45):

Do you have an English proof you can paste?

Eric Wieser (May 01 2022 at 14:48):

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 (May 01 2022 at 14:48):

Your translation should include an exists symbol

Joseph O (May 01 2022 at 14:50):

Like this?

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

Eric Wieser (May 01 2022 at 14:51):

You've not include the "set of" bit

Eric Wieser (May 01 2022 at 14:51):

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

Eric Wieser (May 01 2022 at 14:52):

You also should be writing B := not B :

Joseph O (May 01 2022 at 14:53):

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 (May 01 2022 at 14:53):

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

Joseph O (May 01 2022 at 14:54):

I see

Joseph O (May 01 2022 at 14:55):

So its this

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

Eric Wieser (May 01 2022 at 14:55):

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

Joseph O (May 01 2022 at 14:57):

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 (May 01 2022 at 14:58):

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 (May 01 2022 at 14:58):

I was trying to follow the definition of injective functions

Joseph O (May 01 2022 at 14:59):

doc#function.injective

Eric Wieser (May 01 2022 at 15:00):

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

Riccardo Brasca (May 01 2022 at 15:03):

@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 (May 01 2022 at 15:36):

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 (May 01 2022 at 15:46):

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

Kyle Miller (May 01 2022 at 16:33):

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 (May 01 2022 at 16:38):

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 (May 01 2022 at 16:39):

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

Kyle Miller (May 01 2022 at 16:45):

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

Joseph O (May 01 2022 at 22:56):

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 (May 01 2022 at 23:14):

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 (May 01 2022 at 23:52):

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

Joseph O (May 02 2022 at 13:29):

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 (May 02 2022 at 13:30):

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

Eric Wieser (May 02 2022 at 14:01):

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

Joseph O (May 02 2022 at 14:05):

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 (May 02 2022 at 14:15):

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

Joseph O (May 02 2022 at 14:25):

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 (May 02 2022 at 14:27):

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 (May 02 2022 at 16:52):

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 (May 02 2022 at 16:52):

But for some reason applying h doesnt really work

Joseph O (May 02 2022 at 16:53):

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

Joseph O (May 02 2022 at 16:55):

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

Joseph O (May 02 2022 at 16:55):

Maybe I shouldnt do a contradiction

Joseph O (May 02 2022 at 16:57):

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 (May 02 2022 at 17:06):

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

Joseph O (May 02 2022 at 17:07):

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

Yaël Dillies (May 02 2022 at 17:08):

What is the next step of the proof in words?

Joseph O (May 02 2022 at 17:14):

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 (May 02 2022 at 17:27):

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

Mario Carneiro (May 02 2022 at 17:45):

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 (May 02 2022 at 17:47):

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 (May 02 2022 at 19:05):

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 (May 02 2022 at 19:06):

Yeah they should be very similar

Michael Jam (Oct 24 2022 at 13:56):

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 (Oct 24 2022 at 14:15):

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 (Oct 24 2022 at 18:50):

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 (Oct 24 2022 at 18:57):

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 (Oct 24 2022 at 18:58):

Can you do it with s/Empty/Nat?

Mario Carneiro (Oct 24 2022 at 19:04):

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 (Oct 24 2022 at 19:05):

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

Reid Barton (Oct 24 2022 at 19:10):

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 (Oct 24 2022 at 19:10):

or a custom inductive family

Mario Carneiro (Oct 24 2022 at 19:19):

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 (Oct 24 2022 at 19:20):

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 (Oct 24 2022 at 22:54):

Help please lean3 how to prove

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

Kevin Buzzard (Oct 24 2022 at 22:55):

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

Kevin Buzzard (Oct 24 2022 at 22:56):

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

Moahu Cheng (Oct 24 2022 at 23:00):

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

Matt Diamond (Oct 24 2022 at 23:17):

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

Matt Diamond (Oct 24 2022 at 23:26):

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

Arien Malec (Oct 25 2022 at 02:40):

two other hints:

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

Matt Diamond (Oct 25 2022 at 02:55):

and tactic#by_cases!

Kevin Buzzard (Oct 25 2022 at 05:25):

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 (Oct 25 2022 at 10:08):

@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 (Oct 25 2022 at 10:27):

@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 (Oct 25 2022 at 10:28):

and we can even drop the DecidableEq I assumption

Kevin Buzzard (Oct 25 2022 at 10:28):

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 (Oct 25 2022 at 11:13):

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


Last updated: Dec 20 2023 at 11:08 UTC