Zulip Chat Archive

Stream: maths

Topic: Showing equality of finite sets


view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Gihan Marasingha (Oct 17 2020 at 10:06):

Thanks very much!

view this post on Zulip Mario Carneiro (Oct 17 2020 at 10:08):

simp should work too

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 17 2020 at 10:55):

probably lift to finsets and use dec_trivial

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip Mario Carneiro (Oct 17 2020 at 11:51):

it's probably called not_iff

view this post on Zulip Mario Carneiro (Oct 17 2020 at 11:51):

docs#not_iff?

view this post on Zulip Mario Carneiro (Oct 17 2020 at 11:54):

Huh, congratulations on finding a hole in the library

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 17 2020 at 11:58):

all the funny decidable hypothesis theorems are now in decidable namespace

view this post on Zulip 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?

view this post on Zulip Gihan Marasingha (Oct 17 2020 at 12:16):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 17 2020 at 13:39):

just not by using the intermediate value theorem

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 18:37):

oh of course, there's an algorithm.


Last updated: May 11 2021 at 16:22 UTC