## Stream: general

### Topic: permutations of finsets

#### Johan Commelin (Apr 04 2020 at 10:10):

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 (Apr 04 2020 at 10:43):

by finish probably works.

#### Chris Hughes (Apr 04 2020 at 10:43):

Or finish [finset.ext]

#### Johan Commelin (Apr 04 2020 at 10:56):

Thanks @Chris Hughes

#### Mario Carneiro (Apr 04 2020 at 11:00):

isn't there an insert_comm theorem for this?

#### Johan Commelin (Apr 04 2020 at 11:03):

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

#### Mario Carneiro (Apr 04 2020 at 11:10):

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 (Apr 04 2020 at 11:11):

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

#### Chris Hughes (Apr 04 2020 at 11:39):

You can do simp [finset.ext, or_comm]

#### Kevin Buzzard (Apr 04 2020 at 11:58):

How come no or_assoc?

#### Chris Hughes (Apr 04 2020 at 12:31):

Because there is only one or on each side.

#### Johan Commelin (Apr 04 2020 at 19:12):

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 (Apr 04 2020 at 19:13):

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

#### Kevin Buzzard (Apr 04 2020 at 19:15):

That doesn't even typecheck for me

#### Kevin Buzzard (Apr 04 2020 at 19:15):

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


#### Kevin Buzzard (Apr 04 2020 at 19:19):

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

#### Johan Commelin (Apr 04 2020 at 19:21):

Hmm, does import data.finset solve it?

no

#### Johan Commelin (Apr 04 2020 at 19:21):

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

Crazy

#### Kevin Buzzard (Apr 04 2020 at 19:22):

What mathlib are you using?

#### Kevin Buzzard (Apr 04 2020 at 19:23):

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

#### Kevin Buzzard (Apr 04 2020 at 19:24):

Both mathlibs from April

#### Mario Carneiro (Apr 04 2020 at 19:24):

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

#### Mario Carneiro (Apr 04 2020 at 19:25):

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

#### Reid Barton (Apr 04 2020 at 19:25):

decidable equality issue?

#### Johan Commelin (Apr 04 2020 at 19:29):

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

#### Johan Commelin (Apr 04 2020 at 19:29):

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 (Apr 04 2020 at 19:30):

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

#### Johan Commelin (Apr 04 2020 at 19:35):

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

#### Chris Hughes (Apr 04 2020 at 19:43):

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 (Apr 04 2020 at 20:15):

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 (Apr 04 2020 at 21:55):

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 (Apr 04 2020 at 22:23):

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 (Apr 04 2020 at 22:24):

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

#### Michael R Douglas (Apr 05 2020 at 13:20):

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 (Apr 05 2020 at 13:22):

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 (Apr 05 2020 at 13:35):

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 (Apr 05 2020 at 13:45):

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

Last updated: May 11 2021 at 14:11 UTC