rfl for finite sets

Stream: general

[Frederick Pu]

What's the best way to prove that two finite sets with the same elements are equal.

open Polynomial
example : {3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3, X + 2, 2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1, 4 * X + 1, X, 2 * X, 3 * X, 4 * X, 4 * X + 4} = {X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3, 2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X, 4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} := by ...

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

yuck, I really hope we have something better than this:

import Mathlib

open Polynomial

-- easy but slow
example : {3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3, X + 2, 2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1, 4 * X + 1, X, 2 * X, 3 * X, 4 * X, 4 * X + 4} = ({X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3, 2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X, 4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} : Finset ℤ[X]):= by
  ext p
  simp only [Finset.mem_insert, Finset.mem_singleton]
  tauto

-- I just, hate this.
example : {3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3, X + 2, 2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1, 4 * X + 1, X, 2 * X, 3 * X, 4 * X, 4 * X + 4} = ({X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3, 2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X, 4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} : Finset ℤ[X]):= by
  ext p
  simp only [Finset.mem_insert, Finset.mem_singleton]
  constructor
  all_goals
    rintro (rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl|rfl)
    all_goals
      try simp only [add_left_inj, ne_eq, X_ne_zero, not_false_eq_true, mul_eq_right₀, OfNat.ofNat_ne_one,
        mul_eq_mul_right_iff, OfNat.ofNat_eq_ofNat, Nat.succ.injEq, or_self, add_right_eq_self,
        OfNat.ofNat_ne_zero, add_right_inj, OfNat.one_ne_ofNat, or_false, true_or, or_true]

[Mario Carneiro]

You can do this over sets using simp but apparently the analogous theorem for finsets is missing

theorem Finset.insert_comm {α} [DecidableEq α] (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s) :=
  ext fun _ => by simp [or_left_comm]

example :
    {3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3, X + 2,
      2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1, 4 * X + 1,
      X, 2 * X, 3 * X, 4 * X, 4 * X + 4} =
    ({X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3,
      2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X,
      4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} : Finset ℤ[X]) := by
  simp only [Finset.insert_comm]

[Frederick Pu]

Mario Carneiro said:

You can do this over sets using simp but apparently the analogous theorem for finsets is missing

theorem Finset.insert_comm {α} [DecidableEq α] (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s) :=
  ext fun _ => by simp [or_left_comm]

example :
    {3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3, X + 2,
      2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1, 4 * X + 1,
      X, 2 * X, 3 * X, 4 * X, 4 * X + 4} =
    ({X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3,
      2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X,
      4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} : Finset ℤ[X]) := by
  simp only [Finset.insert_comm]

Polynomials don't have decidable equality tho

[Mario Carneiro]

the proof works as written, just add

import Mathlib.Algebra.Polynomial.Basic

open Polynomial

at the top

[Yaël Dillies]

docs#Finset.Insert.comm ? (terrible name)

[Eric Wieser]

Note that if we change Polynomial to be computable (or rather, kernel-reducible), the proof is decide:

import Mathlib.Algebra.DirectSum.Ring

open scoped DirectSum

abbrev BetterPolynomial (R) [Semiring R] := ⨁ i : ℕ, R
abbrev BetterPolynomial.X {R} [Semiring R] : BetterPolynomial R := .single 1 1

open BetterPolynomial in
example :
    ({3 * X + 4, 2 * X + 4, X + 4, X + 3, 2 * X + 3, 3 * X + 3, 4 * X + 3,
    X + 2, 2 * X + 2, 3 * X + 2, 4 * X + 2, X + 1, 2 * X + 1, 3 * X + 1,
    4 * X + 1, X, 2 * X, 3 * X, 4 * X, 4 * X + 4}  : Finset (BetterPolynomial ℕ)) =
      {X, X + 1, X + 2, X + 3, X + 4, 2 * X, 2 * X + 1, 2 * X + 2, 2 * X + 3, 2 * X + 4, 3 * X, 3 * X + 1, 3 * X + 2, 3 * X + 3, 3 * X + 4, 4 * X, 4 * X + 1, 4 * X + 2, 4 * X + 3, 4 * X + 4} := by
  decide

[Eric Wieser]

(#12491 adds the missing instance)