permutations of finsets

Stream: general

[Johan Commelin]

What is the canonical way to solve

import data.finset

example (X : Type) (x y : X) : ({x, y} : finset X) = {y, x} := sorry

[Chris Hughes]

by finish probably works.

[Chris Hughes]

Or finish [finset.ext]

[Johan Commelin]

Thanks @Chris Hughes

[Mario Carneiro]

isn't there an insert_comm theorem for this?

[Johan Commelin]

Mario, my next question would be how to prove {a,b,c,d,e} = {d,a,c,e,b}.

[Mario Carneiro]

I feel like simp should be able to use insert_comm to do general AC simplifications just as it does with addition currently (when you give it add_left_comm)

[Mario Carneiro]

In this case finset.ext should be enough since simp definitely knows how to play the game with permuting disjuncts

[Chris Hughes]

You can do simp [finset.ext, or_comm]

[Kevin Buzzard]

How come no or_assoc?

[Chris Hughes]

Because there is only one or on each side.

[Johan Commelin]

How about this one

import data.finset

example (X : Type*) (a b c d : X) (h : ({a, b} : finset X) = {c, d}) :
  (a = c ∧ b = d) ∨ (a = d ∧ b = c) := sorry

[Johan Commelin]

This are the kind of trivialities that I don't want to think about...

[Kevin Buzzard]

That doesn't even typecheck for me

[Kevin Buzzard]

failed to synthesize type class instance for
X : Type ?,
a b c d : X
⊢ has_insert ?m_1 (finset X)

[Kevin Buzzard]

I'd knock off a proof for you but I can't get anything to work

[Johan Commelin]

Hmm, does import data.finset solve it?

[Kevin Buzzard]

no

[Johan Commelin]

I copy pasted this out of a file where it does typecheck

[Johan Commelin]

Crazy

[Kevin Buzzard]

What mathlib are you using?

[Kevin Buzzard]

The first example doesn't work for me either. What have I done? I've tried in two projects.

[Kevin Buzzard]

Both mathlibs from April

[Mario Carneiro]

I don't see any reason why that wouldn't work

[Mario Carneiro]

Oh, does @eq (finset X) {a, b} {c, d} work?

[Reid Barton]

decidable equality issue?

[Johan Commelin]

Ha, that might be it. I do have open_locale classical at the top of the file

[Johan Commelin]

import data.finset
import tactic

/-!
Test
-/

open_locale classical

example (X : Type*) (a b c d : X) (h : ({a, b} : finset X) = {c, d}) :
  (a = c ∧ b = d) ∨ (a = d ∧ b = c) := sorry

[Johan Commelin]

Of course this result is classical, in every sense of the word...

[Johan Commelin]

Is this something that existing automation should be able to do? finish doesn't...

[Chris Hughes]

This is the best I could do. I think it is something that there should be an algorithm that does it, at least after simp [finset.ext] at h, because it's a first order in the language with no relation or functions other than equality which must be decidable.

example (X : Type*) (a b c d : X) (h : ({a, b} : finset X) = {c, d}) :
  (a = c ∧ b = d) ∨ (a = d ∧ b = c) :=
begin
  simp [finset.ext] at h,
  have := h a, have := h b, have := h c, have := h d,
  by_cases a = c; by_cases a = d;
  simp [*, eq_comm] at *; cc
end

[Kevin Buzzard]

More generally one could ask

example (X : Type*) (a b c d : X) :
  (a = c ∧ b = d) ∨ (a = d ∧ b = c) ↔
  ∀ x : X, (x = a ∨ x = b) ↔ (x = c ∨ x = d) := sorry

[Jesse Michael Han]

with finish using we can make it even shorter, but it must still be spoon-fed the instantiations:

example (X : Type*) (a b c d : X) (h : ({a, b} : finset X) = {c, d}) :
  (a = c ∧ b = d) ∨ (a = d ∧ b = c) :=
begin
  finish [finset.ext] using [h a, h b, h c, h d]
end

[Kevin Buzzard]

This is a bit surprising to me because h a doesn't make sense until after finset.ext has been applied to h

[Kevin Buzzard]

Aah I see, it applies simp [finset.ext] to all the hypotheses, presumably before reading what happens after using

[Michael R Douglas]

Suppose I wanted to generalize this example to a pair of N-element sets. Is there any way to do it with N a parameter ?

[Kevin Buzzard]

You're in danger of formalising the assertion that if L is a list and P is a permutation, then P L and L give the same multiset, which will be true by definition because multiset is defined as a quotient of list by permutations.

[Reid Barton]

It's also not true that {a, b, c} = {d, e, f} implies (a = d and b = e and c = f) or [5 other permutations].

[Kevin Buzzard]

because {1,1,2}={1,2,2} if they're finsets