law of excluded middle in set membership

Stream: maths

[ZHAO Jinxiang]

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?

[Kevin Buzzard]

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

[Mario Carneiro]

example : (∀ (α : Type) (X : set α) x, x ∈ X ∨ x ∉ X) ↔ ∀ p, p ∨ ¬ p :=
⟨λ H p, H unit {x | p} (), λ H α X x, H (x ∈ X)⟩

[Mario Carneiro]

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)⟩

[ZHAO Jinxiang]

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

[Kevin Buzzard]

Because sets are functions taking values in Prop not bool

[ZHAO Jinxiang]

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

[Kevin Buzzard]

Set unit = Prop

[Kenny Lau]

unfortunately it does

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

So your question is simply whether this is true constructively

[Kevin Buzzard]

And so maybe this is ok

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh no crap

[Kevin Buzzard]

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

[Kevin Buzzard]

So you're in trouble

[Kevin Buzzard]

So you're not ok as Kenny says

[Kyle Miller]

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

[Kyle Miller]

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.

[ZHAO Jinxiang]

Thank you very much.

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

[Mario Carneiro]

yes

[Mario Carneiro]

well, it will use a decidable instance if it can

[ZHAO Jinxiang]

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

[Kyle Miller]

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.

[Kyle Miller]

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

[Kyle Miller]

@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.

[ZHAO Jinxiang]

What's pp.all?

[Kyle Miller]

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

[Kyle Miller]

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

[ZHAO Jinxiang]

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

[Mario Carneiro]

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

[Mario Carneiro]

the majority of mathlib use is predicated on full classical logic

[Kyle Miller]

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

[Mario Carneiro]

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

[ZHAO Jinxiang]

Yes.

[Mario Carneiro]

so then there are no problems

[Mario Carneiro]

just use mathlib normally

[ZHAO Jinxiang]

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

[Kyle Miller]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kyle Miller]

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

[Mario Carneiro]

union_diff_cancel is equivalent to EM

[Kyle Miller]

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

[Kyle Miller]

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

[Mario Carneiro]

well the biggie is classical.choice

[Mario Carneiro]

also funext isn't an axiom in lean

[Kyle Miller]

(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.)

[Kyle Miller]

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

[Bryan Gin-ge Chen]

Wasn't that added in lean#409?

[Kyle Miller]

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

[Kyle Miller]

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.

[Bryan Gin-ge Chen]

Oh, sorry, I see what you mean now.

[ZHAO Jinxiang]

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?

[Kevin Buzzard]

They are definitionally, but not syntactically, equal.

[ZHAO Jinxiang]

Can we change it syntactically?

[Bhavik Mehta]

rw set.mem_def I think

[ZHAO Jinxiang]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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).

[Yury G. Kudryashov]

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