# Zulip Chat Archive

## Stream: maths

### Topic: Showing equality of finite sets

#### Gihan Marasingha (Oct 17 2020 at 09:56):

Is there a tactic to show two finite sets (for simplicity, let's say sets of integers) are equal? That is, can I do the following in one line? Same question for showing two such sets are not equal.

```
import data.set
open set
example : ({5, 6, 7, 8} : set ℤ) = ({5, 7, 5, 8, 6} : set ℤ) :=
begin
rw ext_iff, -- Use the definition of set equality
intro x, -- Assume `x` is an integer.
split, -- It suffices to prove `x ∈ {5, 6, 7, 8} → x ∈ {5, 7, 5, 8, 6}` and the converse.
{ rintro (h₈ | h₇ | h₆ | h₅ | k),
{ rw h₈, right, left, refl, },
{ rw h₇, right, right, right, left, refl, },
{ rw h₆, left, refl, },
{ rw h₅, right, right, left, refl, },
{ exfalso, apply k, }, }, -- The case `x ∈ ∅`.
{ rintro (h₆ | h₈ | h₅ | h₇ | h₅ | k),
{ rw h₆, right, right, left, refl, },
{ rw h₈, left, refl, },
{ rw h₅, right, right, right, left, refl, },
{ rw h₇, right, left, refl, },
{ rw h₅, right, right, right, left, refl, },
{ exfalso, apply k }, },
end
```

#### Bryan Gin-ge Chen (Oct 17 2020 at 10:05):

This works:

```
import data.set
open set
example : ({5, 6, 7, 8} : set ℤ) = ({5, 7, 5, 8, 6} : set ℤ) := by { ext, finish }
```

#### Gihan Marasingha (Oct 17 2020 at 10:06):

Thanks very much!

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

`simp`

should work too

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

`by simp`

reports:

```
tactic failed, there are unsolved goals
state:
⊢ {5, 6, 7, 8} = {7, 5, 8, 6}
```

#### Bryan Gin-ge Chen (Oct 17 2020 at 10:11):

Worth noting perhaps that if you use `finset`

s, `dec_trivial`

works:

```
import data.finset
example : ({5, 6, 7, 8} : finset ℤ) = ({5, 7, 5, 8, 6} : finset ℤ) := dec_trivial
```

#### Kenny Lau (Oct 17 2020 at 10:14):

```
example : ({5, 6, 7, 8} : set ℤ) = ({5, 7, 5, 8, 6} : set ℤ) :=
by simp only [set.singleton_def, set.insert_comm, set.insert_eq_of_mem, set.mem_insert]
```

#### Bryan Gin-ge Chen (Oct 17 2020 at 10:53):

I don't know how to prove an inequality easily though:

```
import data.set
example : ({5, 6, 7, 8} : set ℤ) ≠ ({15, 15, 7, 5, 8, 6} : set ℤ) := by sorry
```

#### Mario Carneiro (Oct 17 2020 at 10:55):

probably lift to finsets and use dec_trivial

#### Mario Carneiro (Oct 17 2020 at 10:56):

or observe that `15`

is in one and not the other (which can be proven fairly automatically)

#### Gihan Marasingha (Oct 17 2020 at 10:59):

Using your ideas, I can simplify a proof that two sets aren't equal, but am I missing a trick in the proof below? I understand that `dec_trivial`

would work if these were `finset`

s. And how might one do this with `simp only`

?

```
example : ({5, 6, 7, 8} : set ℤ) ≠ ({5, 5, 8, 6} : set ℤ) :=
begin
intro h,
rw ext_iff at h,
contrapose! h,
use 7,
finish,
end
```

#### Mario Carneiro (Oct 17 2020 at 11:04):

```
import data.set.basic tactic.norm_num
theorem ne_of_mem_of_not_mem_right {α β} [has_mem α β] {s t : β}
(a : α) (h₁ : a ∈ s) (h₂ : a ∉ t) : s ≠ t := λ h, h₂ $ h ▸ h₁
example : ({5, 6, 7, 8} : set ℤ) ≠ ({5, 5, 8, 6} : set ℤ) :=
ne_of_mem_of_not_mem_right 7 (by simp) (by norm_num)
```

#### Mario Carneiro (Oct 17 2020 at 11:07):

or without the lemma:

```
example : ({5, 6, 7, 8} : set ℤ) ≠ ({5, 5, 8, 6} : set ℤ) :=
λ e, (by norm_num : (7:ℤ) ∉ ({5, 5, 8, 6} : set ℤ)) $ e ▸ by simp
```

#### Bryan Gin-ge Chen (Oct 17 2020 at 11:21):

Here's a proof going through `finset`

s:

```
import data.set
example : ({5, 6, 7, 8} : set ℤ) ≠ ({15, 15, 7, 5, 8, 6} : set ℤ) :=
begin
have : ({5, 6, 7, 8} : finset ℤ) ≠ {15, 15, 7, 5, 8, 6} := dec_trivial,
contrapose! this,
simp only [this, finset.coe_inj.symm, finset.coe_insert, finset.coe_singleton],
end
```

#### Gihan Marasingha (Oct 17 2020 at 11:35):

Now that I see `norm_num`

proves non-membership, here's an alternative. I needed an intermediate result, `foo`

. Is this in mathlib?

```
import data.set
open set
open classical
local attribute [instance] prop_decidable
theorem foo (p q : Prop): ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (q ∧ ¬p) :=
by rw [@iff_def p q, not_and_distrib, not_imp, not_imp]
example : ({5, 6, 7, 8} : set ℤ) ≠ ({5, 5, 8, 6} : set ℤ) :=
begin
intro h,
rw ext_iff at h,
contrapose! h,
use 7,
rw foo,
norm_num,
end
```

#### Kevin Buzzard (Oct 17 2020 at 11:41):

I don't know if `foo`

is in that huge `logic.basic`

file which has loads of this stuff, but just to remark that `tauto!`

proves goals like this:

```
import tactic
theorem foo (p q : Prop): ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (q ∧ ¬p) :=
by tauto!
```

#### Kevin Buzzard (Oct 17 2020 at 11:42):

Searching for things like this is harder than us mathematicians might think it should be, because sometimes the proofs in logic.basic have random decidable hypotheses which we wouldn't think to put in, because they're not true constructively, which can confuse `library_search`

(and this certainly doesn't look true constructively: I don't think

```
pq: Prop
h: ¬(p ↔ q)
⊢ p ∧ ¬q ∨ q ∧ ¬p
```

is going anywhere because constructively the hypothesis is useless and you don't know whether to go left or right).

#### Gihan Marasingha (Oct 17 2020 at 11:46):

Yes, I think I'm teaching the first cohort of maths student at Exeter who really need to know the difference between classical and non-classical reasoning.

I've had the question, 'Isn't negation introduction just the same as proof by contradiction?' Which it is to a classical mathematician. I hope my colleagues don't hate me.

#### Kevin Buzzard (Oct 17 2020 at 11:49):

Yes, constructivists get super-hung up on the fact that the proof that there is no rational number whose square is 2 is constructive even though we say "let's prove it by contradiction". They seem less hung up on the fact that the intermediate value theorem is not valid constructively so they can't construct the square root function :-)

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

it's probably called `not_iff`

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

#### Mario Carneiro (Oct 17 2020 at 11:54):

Huh, congratulations on finding a hole in the library

#### Mario Carneiro (Oct 17 2020 at 11:55):

it's extra weird because we actually have a definition for the rhs, it is `xor`

, but there are literally no theorems about it, not even the obvious `\not (a \iff b) <-> xor a b`

which this would be equivalent to

#### Gihan Marasingha (Oct 17 2020 at 11:56):

Well even though `not_iff`

isn't the same as `foo`

, it does the job in this case.

#### Mario Carneiro (Oct 17 2020 at 11:57):

Kevin Buzzard said:

Searching for things like this is harder than us mathematicians might think it should be, because sometimes the proofs in logic.basic have random decidable hypotheses which we wouldn't think to put in, because they're not true constructively, which can confuse

`library_search`

(and this certainly doesn't look true constructively: I don't think`pq: Prop h: ¬(p ↔ q) ⊢ p ∧ ¬q ∨ q ∧ ¬p`

is going anywhere because constructively the hypothesis is useless and you don't know whether to go left or right).

Note that this is no longer the case, I reformed `logic.basic`

to go classical a few months ago

#### Mario Carneiro (Oct 17 2020 at 11:58):

all the funny decidable hypothesis theorems are now in `decidable`

namespace

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

Now, who wants to take all the useful lemmas from this thread and PR them before we forget?

#### Gihan Marasingha (Oct 17 2020 at 12:16):

Be my guest. I suppose `foo`

is a terrible name :(

#### Kenny Lau (Oct 17 2020 at 13:39):

Kevin Buzzard said:

They seem less hung up on the fact that the intermediate value theorem is not valid constructively so they can't construct the square root function :-)

You actually can construct the square root function

#### Kenny Lau (Oct 17 2020 at 13:39):

just not by using the intermediate value theorem

#### Kevin Buzzard (Oct 17 2020 at 18:37):

oh of course, there's an algorithm.

Last updated: May 11 2021 at 16:22 UTC