Zulip Chat Archive

Stream: maths

Topic: law of excluded middle in set membership


view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 06:43):

import data.set.basic
example {x:α} {s: set α}: x  s  x  s :=
begin
  exact classical.em (x  s),
end

Can we prove it without classical.em in lean?

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 07:10):

I think it's equivalent. Given an arbitrary proposition P you can make the set of natural numbers such that P holds and then asking if 37 is in or not is just asking if P is true or false

view this post on Zulip Mario Carneiro (Oct 17 2020 at 07:17):

example : ( (α : Type) (X : set α) x, x  X  x  X)   p, p  ¬ p :=
λ H p, H unit {x | p} (), λ H α X x, H (x  X)⟩

view this post on Zulip Mario Carneiro (Oct 17 2020 at 07:22):

oh oops, here's a better version

example : ( (α : Type) (X : set α) x, x  X  x  X)   p, p  ¬ p :=
λ H p, H  {x | p} 37, λ H α X x, H (x  X)⟩

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 07:55):

That means: intuitionistic logic can't prove x ∈ s ∨ x ∉ s?

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 07:56):

Because sets are functions taking values in Prop not bool

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 07:56):

I use classical.em in this theorem. But I hope that the proof of theorem union_diff_cancel does not rely on the law of excluded middle.

universe variables u
variables {α : Type u}
theorem union_diff_cancel {s t : set α} (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_union_eq, set.mem_diff, set.subset_def] at *,
  split,
  {
    rintro (h₁|h₁,h₂⟩),
    {
      have := h _ h₁,
      assumption,
    },
    {
      assumption,
    }
  },
  {
    intro h₁,
    have := classical.em (x  s), -- TODO: remove classical.em
    cases this,
    {
      left,
      assumption,
    },
    {
      right,
      split,
      assumption,
      assumption,
    }
  }
end

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 07:56):

Set unit = Prop

view this post on Zulip Kenny Lau (Oct 17 2020 at 07:57):

unfortunately it does

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 07:58):

If alpha is unit, s is P and t is Q you can just directly work out the logic statement that this is equivalent to

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 07:59):

P implies Q is your hypothesis and the conclusion is P or (Q and not P) implies Q

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:00):

So your question is simply whether this is true constructively

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:01):

And so maybe this is ok

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:01):

The general case will reduce to this using functional or set extensionality

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:02):

Oh no crap

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:03):

It's P or (Q and not P) is equivalent to Q

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:03):

So you're in trouble

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 08:04):

So you're not ok as Kenny says

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:07):

You're ok if you assume the set s is given by a decidable predicate:

theorem union_diff_cancel {s t : set α} [p : decidable_pred s] (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_diff, set.mem_union_eq],
  split,
  { rintros (xel | xel, xnel⟩),
    exact h xel,
    exact xel, },
  { intro xel,
    -- by_cases x ∈ s, -- but expanded out using the instance just to show there's no classical.em sneaking in
    rcases p x with (h₁ | h₂),
    { right, exact xel, h₁⟩, },
    { left, exact h₂, }, },
end

Using by_cases like usual:

theorem union_diff_cancel {s t : set α} [decidable_pred s] (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_diff, set.mem_union_eq],
  split,
  { rintros (xel | xel, xnel⟩),
    exact h xel,
    exact xel, },
  { intro xel,
    by_cases x  s,
    { left, exact h, },
    { right, exact xel, h⟩, }, },
end

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:14):

Referencing what Kevin said,

Kevin Buzzard said:

Because sets are functions taking values in Prop not bool

what decidable_pred gives you is a way to, essentially, turn the Prop-valued set membership function into a bool-valued one. However, this restricts which sets you're allowed to use this theorem with.

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:21):

Thank you very much.

But remove [decidable_pred s] in second example also works. Is by_cases introduce em?

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:33):

yes

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:33):

well, it will use a decidable instance if it can

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:35):

So, if I want to force it only use a decidable instance, I should write the first style, rcases p x with (h₁ | h₂).

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:36):

I'm a bit confused... it looks like the proofs that the tactics generate are exactly the same whether or not that decidable_pred is there.

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:40):

Oh, never mind. I didn't set it to pp.all. Without the decidable_pred, it uses classical.prop_decidable instead.

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:42):

@ZHAO Jinxiang I'm not sure what you should do -- I only wrote that because it came to mind. I usually use classical reasoning within proofs myself.

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:42):

What's pp.all?

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:44):

First, I was using the command #print union_diff_cancel to get Lean to print the proof term. Then I remembered to add set_option pp.all true before this to get it to show the full form of the term -- all implicit arguments become visible

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:45):

It turns out set_option pp.implicit true is enough to see the difference, and it's easier to read than pp.all

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:45):

I am trying to translate a math book to lean, I want to derive all theorems from axioms as much as possible.

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:46):

To be perfectly frank, lean isn't the best tool for proofs in a restricted logic, unless that logic is intuitionistic logic

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:47):

the majority of mathlib use is predicated on full classical logic

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:47):

Is there any reason you don't take classical.em as an axiom then?

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:47):

I would imagine that Tao's Analysis 1 is written for classical logic

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:48):

Yes.

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:48):

so then there are no problems

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:48):

just use mathlib normally

view this post on Zulip ZHAO Jinxiang (Oct 17 2020 at 08:48):

Ok, I'll use classical logic. :joy:

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:49):

Also, have you looked at the proof of classical.em? It follows from other axioms.

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:49):

If you get too close to the foundations you will notice that the axioms don't match up 1-1 to a logic textbook, but the full theories are roughly equivalent

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:50):

like there is no axiom for "and elimination" in lean, it falls out of a much more general axiom schema for inductive types

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:50):

Both of the proofs of union_diff_cancel depend on the two axioms classical.em follows from, if I'm not mistaken.

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:51):

union_diff_cancel is equivalent to EM

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:51):

Sure, what I mean is that the proof terms explicitly have the propext and funext (but as set.ext)

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:52):

so if that's true, there's no point avoiding classical.em

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:52):

well the biggie is classical.choice

view this post on Zulip Mario Carneiro (Oct 17 2020 at 08:53):

also funext isn't an axiom in lean

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:57):

(I know that funext comes from quotient types and I was using "axiom" loosely, but I did forget classical.prop_decidable used classical.choice in those last comments.)

view this post on Zulip Kyle Miller (Oct 17 2020 at 08:58):

is it possible to make by_cases use classical.em when possible? (assuming anyone cared about classical.choice in their proofs?)

view this post on Zulip Bryan Gin-ge Chen (Oct 17 2020 at 09:02):

Wasn't that added in lean#409?

view this post on Zulip Kyle Miller (Oct 17 2020 at 09:05):

It looks like it uses classical.prop_decidable as a fallback, which is implemented with classical.choice.

view this post on Zulip Kyle Miller (Oct 17 2020 at 09:07):

I'm ok with choice, so this isn't a serious question in any way. But if anyone isn't ok with it, it seems like for Prop goals by_cases could use classical.em instead.

view this post on Zulip Bryan Gin-ge Chen (Oct 17 2020 at 09:07):

Oh, sorry, I see what you mean now.

view this post on Zulip ZHAO Jinxiang (Oct 18 2020 at 15:58):

Kyle Miller said:

You're ok if you assume the set s is given by a decidable predicate:

theorem union_diff_cancel {s t : set α} [p : decidable_pred s] (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_diff, set.mem_union_eq],
  split,
  { rintros (xel | xel, xnel⟩),
    exact h xel,
    exact xel, },
  { intro xel,
    -- by_cases x ∈ s, -- but expanded out using the instance just to show there's no classical.em sneaking in
    rcases p x with (h₁ | h₂),
    { right, exact xel, h₁⟩, },
    { left, exact h₂, }, },
end

Using by_cases like usual:

theorem union_diff_cancel {s t : set α} [decidable_pred s] (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_diff, set.mem_union_eq],
  split,
  { rintros (xel | xel, xnel⟩),
    exact h xel,
    exact xel, },
  { intro xel,
    by_cases x  s,
    { left, exact h, },
    { right, exact xel, h⟩, }, },
end

What's the difference with t x and x ∈ t?

view this post on Zulip Kevin Buzzard (Oct 18 2020 at 15:58):

They are definitionally, but not syntactically, equal.

view this post on Zulip ZHAO Jinxiang (Oct 18 2020 at 15:59):

Can we change it syntactically?

view this post on Zulip Bhavik Mehta (Oct 18 2020 at 15:59):

rw set.mem_def I think

view this post on Zulip ZHAO Jinxiang (Oct 18 2020 at 16:07):

theorem union_diff_cancel {s t : set α} [p : decidable_pred s] (h : s  t) : s  (t \ s) = t :=
begin
  ext x,
  simp only [set.mem_diff, set.mem_union_eq],
  split,
  { rintros (xel | xel, xnel⟩),
    exact h xel,
    exact xel, },
  { intro xel,
    rcases p x with (h₁ | h₂),
    {
      rewrite <-set.mem_def at h₁,  -- rewrite tactic failed, did not find instance of the pattern in the target expression
      right, exact xel, h₁⟩, },
    { left, exact h₂, }, },
end

view this post on Zulip Kevin Buzzard (Oct 18 2020 at 22:56):

rewrite ← @set.mem_def _ x s at h₁, works. Lean needs some hints for some reason

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:09):

ZHAO Jinxiang said:

What's the difference with t x and x ∈ t?

x ∈ t is defined to be t x, and should always be favored. It is a bad habit to break the abstraction barrier of sets. The phrase decidable_pred s also breaks the abstraction barrier, and should be replaced by decidable_pred (∈ s).

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 23:41):

There is an instance [decidable_pred s] : decidable_pred (∈s), so at least this doesn't create diamonds.


Last updated: May 10 2021 at 07:15 UTC