Zulip Chat Archive

Stream: general

Topic: permutations of finsets


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

view this post on Zulip Chris Hughes (Apr 04 2020 at 10:43):

by finish probably works.

view this post on Zulip Chris Hughes (Apr 04 2020 at 10:43):

Or finish [finset.ext]

view this post on Zulip Johan Commelin (Apr 04 2020 at 10:56):

Thanks @Chris Hughes

view this post on Zulip Mario Carneiro (Apr 04 2020 at 11:00):

isn't there an insert_comm theorem for this?

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

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

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

view this post on Zulip Chris Hughes (Apr 04 2020 at 11:39):

You can do simp [finset.ext, or_comm]

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 11:58):

How come no or_assoc?

view this post on Zulip Chris Hughes (Apr 04 2020 at 12:31):

Because there is only one or on each side.

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:12):

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

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:13):

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:15):

That doesn't even typecheck for me

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:19):

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

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:21):

Hmm, does import data.finset solve it?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:21):

no

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:21):

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

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:21):

Crazy

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:22):

What mathlib are you using?

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:24):

Both mathlibs from April

view this post on Zulip Mario Carneiro (Apr 04 2020 at 19:24):

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

view this post on Zulip Mario Carneiro (Apr 04 2020 at 19:25):

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

view this post on Zulip Reid Barton (Apr 04 2020 at 19:25):

decidable equality issue?

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

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

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:30):

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

view this post on Zulip Johan Commelin (Apr 04 2020 at 19:35):

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

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 20:15):

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

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

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

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

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

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

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

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