## Stream: maths

### Topic: law of excluded middle in set membership

#### 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?

#### 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

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


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


#### ZHAO Jinxiang (Oct 17 2020 at 07:55):

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

#### Kevin Buzzard (Oct 17 2020 at 07:56):

Because sets are functions taking values in Prop not bool

#### 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


Set unit = Prop

#### Kenny Lau (Oct 17 2020 at 07:57):

unfortunately it does

#### 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

#### 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

#### Kevin Buzzard (Oct 17 2020 at 08:00):

So your question is simply whether this is true constructively

#### Kevin Buzzard (Oct 17 2020 at 08:01):

And so maybe this is ok

#### Kevin Buzzard (Oct 17 2020 at 08:01):

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

Oh no crap

#### Kevin Buzzard (Oct 17 2020 at 08:03):

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

#### Kevin Buzzard (Oct 17 2020 at 08:03):

So you're in trouble

#### Kevin Buzzard (Oct 17 2020 at 08:04):

So you're not ok as Kenny says

#### 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


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

#### 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?

yes

#### Mario Carneiro (Oct 17 2020 at 08:33):

well, it will use a decidable instance if it can

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

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

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

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

#### ZHAO Jinxiang (Oct 17 2020 at 08:42):

What's pp.all?

#### 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

#### 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

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

#### 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

#### Mario Carneiro (Oct 17 2020 at 08:47):

the majority of mathlib use is predicated on full classical logic

#### Kyle Miller (Oct 17 2020 at 08:47):

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

#### Mario Carneiro (Oct 17 2020 at 08:47):

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

Yes.

#### Mario Carneiro (Oct 17 2020 at 08:48):

so then there are no problems

#### Mario Carneiro (Oct 17 2020 at 08:48):

just use mathlib normally

#### ZHAO Jinxiang (Oct 17 2020 at 08:48):

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

#### Kyle Miller (Oct 17 2020 at 08:49):

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

#### 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

#### 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

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

#### Mario Carneiro (Oct 17 2020 at 08:51):

union_diff_cancel is equivalent to EM

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

#### Kyle Miller (Oct 17 2020 at 08:52):

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

#### Mario Carneiro (Oct 17 2020 at 08:52):

well the biggie is classical.choice

#### Mario Carneiro (Oct 17 2020 at 08:53):

also funext isn't an axiom in lean

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

#### 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?)

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

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

#### Bryan Gin-ge Chen (Oct 17 2020 at 09:07):

Oh, sorry, I see what you mean now.

#### 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?

#### Kevin Buzzard (Oct 18 2020 at 15:58):

They are definitionally, but not syntactically, equal.

#### ZHAO Jinxiang (Oct 18 2020 at 15:59):

Can we change it syntactically?

#### Bhavik Mehta (Oct 18 2020 at 15:59):

rw set.mem_def I think

#### 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


#### Kevin Buzzard (Oct 18 2020 at 22:56):

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

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

#### 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