help dealing with quantifiers in example

Stream: new members

[Mason McBride]

To the best of my ability, I translated Joel David Hampkin's tweet into lean. There are a lot of quantifies on both sides of a proposition. I'm trying to prove it but I don't know how to deal with them in an organized way. I remember I can use cases on them because use only works on the goal. Any help would be kind.

Logic puzzle challenge. Express the following assertion in plainer language: ∃y (x≠y and y≠z) → ∀x∃y (x≠y and y≠z)

- Joel David Hamkins (@JDHamkins)

import data.real.basic

variables (x y z : ℝ)

example : (∃y : ℝ, x≠y ∧ y≠z) → (∀x : ℝ, ∃y : ℝ, x≠y ∧ y≠z) :=
begin
  sorry,
  /-
  # Option 1
  simp, (this gives me a (∀ x_1 : ℝ), which idk what that means)
  # Option 2
  by_contradiction,
  push_neg at h,
  -/
end

[Mario Carneiro]

you don't really need real for this... use variable {A : Type*} instead to avoid the gratuitous imports

[Ruben Van de Velde]

Is the goal to express the assertion or prove it?

[Mario Carneiro]

I think it is true

[Mason McBride]

prove it

[Mario Carneiro]

(this gives me a (∀ x_1 : ℝ), which idk what that means)

there is more stuff after the quantifier, it continues on several lines

[Mason McBride]

Here's how close I got:

example : (∃y : ℝ, x≠y ∧ y≠z) → (∀x : ℝ, ∃y : ℝ, x≠y ∧ y≠z) :=
begin
  simp,
  intros y x_ne_y y_ne_z x',
  use y,
  split,
  { sorry, /- I don't have x'≠y -/},
  exact y_ne_z,
end

[Mason McBride]

Thanks mario ill refactor rn

[Mario Carneiro]

I would start the proof like this:

import tactic

example {α : Type*} (x z : α) :
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
begin
  rintro ⟨y, xy, yz⟩ w,
  by_cases wy : w = y,
  { subst w,
    sorry },
  { exact ⟨_ , wy, yz⟩ }
end

[Mario Carneiro]

the next part is probably cases on whether some variables are equal to some others

[Alex J. Best]

Joel says on his twitter that he doesn't intend any universal quantification of x and z, which it seems like you are doing here.

[Mario Carneiro]

I don't think there is any untoward quantification here

[Mario Carneiro]

x and z are free variables (y is unused)

[Mario Carneiro]

oh interesting, this sorry doesn't look provable

example {α : Type*} (x z : α) :
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
begin
  rintro ⟨y, xy, yz⟩ w,
  by_cases wy : w = y,
  { subst w,
    by_cases xz : x = z,
    { subst z, sorry },
    { exact ⟨_, xy.symm, xz⟩ } },
  { exact ⟨_ , wy, yz⟩ }
end

[Alex J. Best]

Well when we write

variables (x z : ℝ)

example : (∃y : ℝ, x≠y ∧ y≠z) → (∀x : ℝ, ∃y : ℝ, x≠y ∧ y≠z) := ...

we universally quantify over x and z, I guess I'm saying the expression of the original logical statement is

example : ℝ → ℝ → Prop := λ x z, (∃y : ℝ, x≠y ∧ y≠z) → (∀x : ℝ, ∃y : ℝ, x≠y ∧ y≠z)

which it doesn't make sense to "prove it", necessarily.

[Mario Carneiro]

Normally, proving a statement with free variables is equivalent to proving its universal closure

[Alex J. Best]

Right, I'm pointing out that just doing that you might not be getting something provable

[Mario Carneiro]

well if the statement's universal closure is not provable it is a stretch to say the original statement is

[Mario Carneiro]

even if there are some more hypotheses about x and z that apply it would still be the universal closure of that that is being asserted

[Alex J. Best]

Yes precisely, the original question on twitter is simply to interpret the sentence, not to prove it

[Mario Carneiro]

a lot of logicians just define provability to only apply to (closed) sentences to avoid this confusion

[Mason McBride]

what If I want to prove it

[Mario Carneiro]

or disprove it...?

[Mason McBride]

yeah either one

[Alex J. Best]

You should decide which it is before embarking on the proof though!

[Mario Carneiro]

Blindly applying simp in problems like this usually doesn't get you far. You usually have to do some structural reasoning here using things like cases and use

[Mario Carneiro]

and in particular by_cases on variables being equal is important in this one

[Mario Carneiro]

and subst when they are equal to get rid of the extra variables

[Mason McBride]

Mario Carneiro said:

oh interesting, this sorry doesn't look provable

example {α : Type*} (x z : α) :
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
begin
  rintro ⟨y, xy, yz⟩ w,
  by_cases wy : w = y,
  { subst w,
    by_cases xz : x = z,
    { subst z, sorry },
    { exact ⟨_, xy.symm, xz⟩ } },
  { exact ⟨_ , wy, yz⟩ }
end

is this sorry not provable because you can't use anything for y_1 that would satisfy the goal?

[Mason McBride]

Thanks for the tips Mario I've been stepping through your snippets and I'm getting to see how subst and by_cases work

[Mario Carneiro]

yeah, the only thing you know is that x and y aren't equal, and you need to come up with something that isn't x or y (there might not even be any such thing)

[Mario Carneiro]

in fact, you can just plug and chug it for bool to disprove it

example : ¬ ∀ {α : Type*} (x z : α),
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
have ¬ ∀ (x z : bool), (∃y : bool, x≠y ∧ y≠z) → (∀x : bool, ∃y : bool, x≠y ∧ y≠z),
  by dec_trivial,
λ H, this H

[Mario Carneiro]

this works because quantifiers over bool can be brute forced, so we can just evaluate the whole statement as a claim about bool

[Alex J. Best]

You can also just do this if you know the counterexample

example : ¬ ∀ {α : Type*} (x z : α),
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
λ H, by simpa using H tt tt

[Mario Carneiro]

here's a more explicit proof

example : ¬ ∀ {α : Type*} (x z : α),
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
begin
  intro H,
  obtain ⟨_|_, h1, h2⟩ := @H bool tt tt ⟨ff, ne.symm bool.ff_ne_tt, bool.ff_ne_tt⟩ ff,
  { exact h1 rfl },
  { exact h2 rfl },
end

[Mario Carneiro]

or by { intro H, have := @H bool, revert this, dec_trivial } which is more similar to alex's version

[Mario Carneiro]

even λ H, by simpa using @H bool works

[Mario Carneiro]

I guess this is because there are also simp lemmas which effectively brute-force bool quantifiers

[Mason McBride]

nice these are cool, what's @H

[Mario Carneiro]

@ before an identifier makes all of the implicit quantifiers act like they were explicit. In this case, the quantifier on alpha

[Mario Carneiro]

because we want to pass bool to that quantifier without specifying later things

[Mario Carneiro]

normally the type argument would be implied by later things (like alex's version, which uses H tt tt and since tt : bool it infers that alpha is bool)

[Mario Carneiro]

if you just used H alone, it would get instantiated to an unknown type and then the simp lemmas and things for bool quantifiers wouldn't trigger since it has no idea that bool is involved

[Yaël Dillies]

I read this sentence as "ℝ has at least three elements".

[Martin C. Martin]

Yaël Dillies said:

I read this sentence as "ℝ has at least three elements".

If there is only one element, then the premise is always false, so the implication is always true.

[Yaël Dillies]

Oh right, then I guess it is "ℝ doesn't have exactly two elements".

[Martin C. Martin]

The consequent says "there are at least 3 elements." For the antecedent, if x = z, it says "there are at least two elements," otherwise, it says "there are at least 3 elements."

So, if x=z, the full implication says "doesn't have exactly two elements." Otherwise, it's a tautology. I think. :)

[Mario Carneiro]

I like that, that description is way better than the things people were saying on twitter. "If there are exactly two elements, then x != z."

[Mason McBride]

I'm just putting this here for me

example : ¬ ∀ {α : Type*} (x z : α),
  (∃y : α, x≠y ∧ y≠z) → (∀x : α, ∃y : α, x≠y ∧ y≠z) :=
begin
  intro H,
  have y_ne_ff_and_tt :=
  begin
    exact @H bool tt tt ⟨ff, ne.symm bool.ff_ne_tt, bool.ff_ne_tt⟩ ff,
  end,
  rcases y_ne_ff_and_tt with ⟨_|_, h1, h2⟩,
  { apply h1,
    exact rfl, },
  { apply h2,
    exact rfl, },
end