Cardinality of finset vs fintype

Stream: new members

[Ritwick Bhargava]

Hi everyone, I'm working on defining the length of a permutation and proving some related things, but I'm getting tripped up on the differences between finset and fintype. So far I'm defining the length of a permutation as the cardinality of a certain finset (the set of all inversions):

import group_theory.perm.sign
open equiv function fintype finset

@[derive decidable_pred]
def in_order {n:ℕ} (a:perm (fin n)) : ( Σ (b : fin n), fin n) → Prop := λ x, a x.1 ≤ a x.2

--the set of all inversions of a permutations
def all_inv {n:ℕ} (a:equiv.perm (fin n)) := finset.filter (in_order a) (perm.fin_pairs_lt n)

def length {n:ℕ} (a: equiv.perm (fin n)) : ℕ := finset.card (all_inv a)

When I want to show two lengths are related, it's natural to reason about bijections between various inversions (and so moving to types), for example:

lemma length_mul_swap {n:ℕ} {h: 1<n} (a: equiv.perm (fin n)) (i: fin n) (h1: (i.val + 1) < n)  (h2: a i > a (i + ⟨1, h⟩)) :
(finset.erase (all_inv a) ⟨i + ⟨1, h⟩, i⟩) ≃ all_inv (a * swap i (i + ⟨1, h⟩))

After proving that, I'm having a surprisingly hard time showing something like

lemma length_of_swap {n:ℕ}  {h: 1<n}  (a: equiv.perm (fin n)) (i: fin n) (h1: (i.val + 1) < n)  (h2: a i > a (i + ⟨1, h⟩)) :
length(a) - 1 = length(a * (equiv.swap i (i + ⟨1, h⟩)))

even though I thought fintype.card_of_finset would make easy work of it. Can someone point me in the right direction for proving something like this? More generally, is this a reasonable approach to approach this topic? The coercions sometimes get complicated, so I'm wondering if there was a better way.

If you don't want to look at all the code above, basically a mwe for what I'm looking to prove is

import group_theory.perm.sign
open equiv function fintype finset
lemma card_lemma (a: finset (fin n)) : fintype.card a = finset.card a :=
begin
  rw fintype.card_of_finset, -- does not rewrite as expected
end

Any help or suggestions would be much appreciated, thank you!

[Mario Carneiro]

don't forget imports in your #mwe

[Kyle Miller]

lemma card_lemma {n : ℕ} (a: finset (fin n)) : fintype.card a = finset.card a :=
begin
  convert fintype.card_coe a,
end

(I think it's because fintype.card_coe doesn't have a general enough fintype instance.)

[Kyle Miller]

Yeah, that seems to be the problem:

@[simp] lemma fintype.card_coe' {α : Type*} (s : finset α) [fintype s] : -- added `[fintype s]`
  fintype.card s = s.card := by convert fintype.card_coe s

lemma card_lemma {n : ℕ} (a: finset (fin n)) : fintype.card a = finset.card a :=
begin
  simp,
end

[Ritwick Bhargava]

Mario Carneiro said:

don't forget imports in your #mwe

Sorry, edited them in

[Mario Carneiro]

It seems like finset.has_coe_to_sort was added after most of the fintype file was written and a fintype instance was not proved for it

[Mario Carneiro]

it used to be spelled ↥(s : set α) so the existing instances were all that were needed

[Mario Carneiro]

it follows from fintype.card_of_finset' where you supply iff.rfl as the proof

[Kyle Miller]

#13055

[Ritwick Bhargava]

Kyle Miller said:

Yeah, that seems to be the problem:

@[simp] lemma fintype.card_coe' {α : Type*} (s : finset α) [fintype s] : -- added `[fintype s]`
  fintype.card s = s.card := by convert fintype.card_coe s

lemma card_lemma {n : ℕ} (a: finset (fin n)) : fintype.card a = finset.card a :=
begin
  simp,
end

Thanks a lot for the help, card_coe' is exactly what I needed