## 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 finsets, 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 finsets. 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 finsets:

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