# Zulip Chat Archive

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

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

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

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

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?

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

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

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

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

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

Wasn't that added in lean#409?

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