cardinality of powerset

Stream: maths

[Milan Tiji]

Hi my name is Milan and I am a computer science student learning Lean and trying to write a proof on the cardinality of the powerset. Right now I am doing the proof for no surjection between X and the powerset. I have had some trouble using 'match' .

have u2 : ∃ x, x ∈ A ∧ f x = y,
match u2 with (x0, u3, u4) :=

So I tried defining u2 and matching it with the other variable names so that x0 matches with ∃ x, u3 matches with x ∈ A and u4 matches with f x = y. It gives me the error 'Can't synthesize placeholder' on the match and u2. Can anyone give me some assistance on how to go about this please. Thank you!

[Kyle Miller]

It would be helpful if you could provide a #mwe that shows the error -- that way we can paste it into Lean and more easily give suggestions.

[Reid Barton]

The parentheses should definitely be angle brackets, though.

[Yury G. Kudryashov]

Also, you should properly use #backticks

[Milan]

Kyle Miller said:

It would be helpful if you could provide a #mwe that shows the error -- that way we can paste it into Lean and more easily give suggestions.

section
variables {U V: Type}

def powerset (A : set U) : set (set U) := {B : set U | B ⊆ A}
def surjective (f : U → V)(A : set U)(B : set V) : Prop := ∀ y, y ∈ B → ∃ x, x ∈ A ∧ f x = y

theorem no_surjection : ∀ f : U → set U, ∀ A : set U, ¬ surjective f A (powerset A) :=
begin

assume f,
assume A,
assume (h : surjective f A (powerset A)),
show false,

let y := {z ∈ A | ¬ (z ∈ f z)},
have u1 : y ∈ (powerset A),
from h y u1,
have u2 : ∃ x, x ∈ A ∧ f x = y,

match u2 with ⟨x0, u3, u4⟩ :=

end

This is not the entire code but I got rid of some things and hopefully this is enough to help understand what's going on and what I am doing.

[Kevin Buzzard]

You should fix your first error before you start worrying about your last error. If you comment out the match you'll see an error earlier in your script.

[Milan]

That's interesting because I don't actually get an error

[Kevin Buzzard]

you do if you comment out the match (or at least I do) -- you can't prove u1 using u1 because it's not there yet. Maybe comment out the have u2 too? After that error Lean is totally confused and can't be trusted.

[Milan]

I have tried commenting out both and I don't seem to get any error still.

[Kevin Buzzard]

On the other hand, I'm sure you believe that you can't prove a new theorem called u1 using a fact called u1 which has not been defined up until this point -- that would be circular reasoning.

[Kevin Buzzard]

u1.png
That's what I see. Note the red underline under u1 and the error on the right

[Milan]

Okay, I see the error on your one. So I will have to define it first?

[Kevin Buzzard]

I think your first error is actually even earlier. I don't think that your definition of y is valid lean syntax. Edit: Hmm -- apparently it is? I didn't know that! Ignore me.

[Milan]

I will try amend the first error before the other but I will have to look into it more. I am still perplexed as to why the error does not show up on my system. Thank you.

[Kevin Buzzard]

Try restarting VS Code.

[Kevin Buzzard]

If you still have no error, post a screenshot like I did and I'll see if I can spot any funny business. Open the file explorer by clicking on the "two pieces of paper" icon on the top left in VS Code. You are using VS Code, right?

[Milan]

Okay will do, I have it installed on VS code.

[Milan]

Screenshot-2022-02-01-at-23.08.34.png

I don't seem to be getting the same errors as you but now it is showing an error on the no_surjection. But when I comment out the match line it gets rid of all errors.

[Kevin Buzzard]

let y := {z ∈ A | ¬ (z ∈ f z)},
have hy : y = {z : U | z ∈ A ∧ ¬ (z ∈ f z) },
  refl,

Your definition of y is definitionally equal to that.

[Kevin Buzzard]

There is no match tactic, Lean is totally confused by that point. Can I see what happens when you comment out match?

[Milan]

Actually, you are correct. I have managed to find the error with u1.

[Milan]

Thank you very much, I will work on fixing the u1 error now.

[Patrick Johnson]

If you import tactic you will gain access to docs#tactic.interactive.set, which you can use instead of let if you want explicit hypothesis, and docs#tactic.interactive.rcases, which you can use instead of match. Note that your definition of powerset is docs#set.powerset and surjective is docs#set.surj_on.

[Milan]

Hi, I can't understand why my code gives me an error on the from powerset A as it says the term has a invalid type ascription. I was trying to define u1 although Lean does not understand it and so I am unsure how to go about this. Could anyone help me please solve this error? Here is #mwe of my code.

section
variables {U V: Type}

def powerset (A : set U) : set (set U) := {B : set U | B ⊆ A}
def surjective (f : U → V)(A : set U)(B : set V) : Prop := ∀ y, y ∈ B → ∃ x, x ∈ A ∧ f x = y
def injection (f : U → V)(A : set U) : Prop := ∀ x1 x2, x1 ∈ A ∧ x2 ∈ A → f x1 = f x2 → x1 = x2

theorem no_surjection : ∀ f : U → set U, ∀ A : set U, ¬ surjective f A (powerset A) :=

begin
assume f,
assume A,
assume (h : surjective f A (powerset A)),
show false,

let y := {z ∈ A | ¬ (z ∈ f z)},
have u1 : y ∈ (powerset A),
  from powerset A,
have u2 : ∃ x, x ∈ A ∧ f x = y,
  from h y u1,

end
end

[Yaël Dillies]

You're trying to provide powerset A as a term of type y ∈ (powerset A). How should that make sense?

[Kevin Buzzard]

from powerset A,

After the word from you need to write a proof of the theorem that y ∈ powerset A. But powerset A is not a proof of this statement, it's just a random type.

[Patrick Johnson]

You need a proof of y ∈ powerset A

have u1 : y ∈ powerset A := λ _, and.left,

[Milan]

Thank you that has worked now

[Milan]

Hi again, my last problem was fixed however now my code has completely broke which hasn't happened before.

section
variables {U V: Type}

def powerset (A : set U) : set (set U) := {B : set U | B ⊆ A}
def surjective (f : U → V)(A : set U)(B : set V) : Prop := ∀ y, y ∈ B → ∃ x, x ∈ A ∧ f x = y
def injection (f : U → V)(A : set U) : Prop := ∀ x1 x2, x1 ∈ A ∧ x2 ∈ A → f x1 = f x2 → x1 = x2

theorem no_surjection : ∀ f : U → set U, ∀ A : set U, ¬ surjective f A (powerset A) :=

begin
assume f,
assume A,
assume (h : surjective f A (powerset A)),
show false,

let y := {z ∈ A | ¬ (z ∈ f z)},
have u1 : y ∈ (powerset A) := λ _, and.left,
have u2 : ∃ x, x ∈ A ∧ f x = y,
  from h y u1,

match u2 with ⟨x0, u3, u4⟩ :=
Let y = {z in A | z ¬ ∈ f(z)} by h there exists x ∈ A such that f(x) = y

end
end

I uncommented the match to fix the earlier error with the powerset definition however now I get multiple errors including where it says theorem no_surjection saying equation compiler failed . This didn't happen previously and I'm unsure how this has occurred. Any help will be much appreciated, thank you.

[Kevin Buzzard]

match is not a tactic in Lean 3. If you're not using mathlib you can do cases on u2, and if you are then you can do rcases.

[Reid Barton]

Also Let y = {z in A | z ¬ ∈ f(z)} by h there exists x ∈ A such that f(x) = y is not valid Lean syntax, as you probably know

[Milan]

Reid Barton said:

Also Let y = {z in A | z ¬ ∈ f(z)} by h there exists x ∈ A such that f(x) = y is not valid Lean syntax, as you probably know

Haha apologies, that should not have been there.

[Milan]

Hi, so basically I am facing another problem with my proof. I am struggling to write the proof by contradiction segment of my theorem and I have come across an error saying focused goal has not been solved for the middle begin and end.

section
variables {U V: Type}

def powerset (A : set U) : set (set U) := {B : set U | B ⊆ A}
def surjective (f : U → V)(A : set U)(B : set V) : Prop := ∀ y, y ∈ B → ∃ x, x ∈ A ∧ f x = y

theorem no_surjection : ∀ f : U → set U, ∀ A : set U, ¬ surjective f A (powerset A) :=

begin
assume f,
assume A,
assume (h : surjective f A (powerset A)),
show false,

let y := {z ∈ A | ¬ (z ∈ f z)},
have u1 : y ∈ (powerset A) := λ _, and.left,
have u2 : ∃ x, x ∈ A ∧ f x = y,
  from h y u1,

cases u2 with x0 u3,
  cases u3 with u30 u31,
  let claim1: ¬ x0 ∈ y :=
      begin assume v1 : x0 ∈ y, show false,
          begin
              have u5: ¬ x0 ∈ f x0, from v1.right,
              have u6: ¬ x0 ∈ y, from eq.rec u5 u31,
              have false, from u6 v1,
          end,
  let claim2: ¬ x0 ∈ f x0 := eq.rec claim1 u31,
  let claim3: x0 ∈ y := constructor, exact u30, exact claim2,
      end

end
end

I feel like I am going about this the wrong way. Would it be better to use classical reasoning and use the by_contradiction inference to solve the contradiction part? Also, I was wondering if the eq equality relation is the same as using an = symbol? Thank you.

[Reid Barton]

The proof looks okay math-wise but you have begin/end in the wrong places

[Reid Barton]

And let claim3: x0 ∈ y := constructor, cannot be correct

[Reid Barton]

You should try to avoid ever having errors (aside from goals that are unsolved). If Lean gives you an error then fix it--don't keep typing more stuff.

[Yaël Dillies]

Yes, eq = (=).

[Milan]

How do I fix this begin/end issue as this is how I believed it had to be done by looking through the Lean manual

[Kyle Miller]

What have false, from u6 v1, is doing is creating a new hypothesis named false that is a proof of false. The current goal is false, so you can just do exact u6 v1.

[Kyle Miller]

Your proof might be more conventionally structured like this:

theorem no_surjection : ∀ f : U → set U, ∀ A : set U, ¬ surjective f A (powerset A) :=
begin
  intros f A h,

  let y := {z ∈ A | ¬ (z ∈ f z)},
  have u1 : y ∈ (powerset A) := λ _, and.left,
  have u2 : ∃ x, x ∈ A ∧ f x = y := h y u1,

  cases u2 with x0 u3,
  cases u3 with u30 u31,
  have claim1 : ¬ x0 ∈ y,
  { assume v1 : x0 ∈ y,
    have u5: ¬ x0 ∈ f x0 := v1.right,
    rw [u31] at u5,
    exact u5 v1, },
  have claim2 : ¬ x0 ∈ f x0,
  { sorry, },
  have claim3 : x0 ∈ y,
  { sorry, },
  exact claim1 claim3,
end

Curly braces are a synonym for begin ... end in a tactic block. I replaced the parts that didn't work with sorry (claim2 doesn't seem to be used though).

[Milan]

Thank you