Showing equality of finite sets

Stream: maths

[Gihan Marasingha]

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]

This works:

import data.set

open set

example : ({5, 6, 7, 8} : set ℤ) = ({5, 7, 5, 8, 6} : set ℤ) := by { ext, finish }

[Gihan Marasingha]

Thanks very much!

[Mario Carneiro]

simp should work too

[Bryan Gin-ge Chen]

by simp reports:

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

[Bryan Gin-ge Chen]

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]

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]

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]

probably lift to finsets and use dec_trivial

[Mario Carneiro]

or observe that 15 is in one and not the other (which can be proven fairly automatically)

[Gihan Marasingha]

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]

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]

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]

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]

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]

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]

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]

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]

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]

it's probably called not_iff

[Mario Carneiro]

docs#not_iff?

[Mario Carneiro]

Huh, congratulations on finding a hole in the library

[Mario Carneiro]

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]

Well even though not_iff isn't the same as foo, it does the job in this case.

[Mario Carneiro]

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]

all the funny decidable hypothesis theorems are now in decidable namespace

[Bryan Gin-ge Chen]

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

[Gihan Marasingha]

Be my guest. I suppose foo is a terrible name :(

[Kenny Lau]

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]

just not by using the intermediate value theorem

[Kevin Buzzard]

oh of course, there's an algorithm.