How to prove some simple combinatoric identities

Stream: new members

[Ching-Tsun Chou]

I wish to prove the following simple combinatoric identities:

variable {α : Type*} [Fintype α] [DecidableEq α]

def Perm α := {l : List α // l.Nodup ∧ ∀ a, a ∈ l}

instance fintype_perm : Fintype (Perm α) := by
  sorry

theorem num_perms_all : Fintype.card (Perm α) = (Fintype.card α).factorial := by
  sorry

def hasSetPrefix (s : Finset α) : Finset (Perm α) :=
  {l : Perm α | (List.take s.card l.val).toFinset = s}

theorem num_perms_set_prefix (s : Finset α) :
    (hasSetPrefix s).card = s.card.factorial * (Fintype.card α - s.card).factorial := by
  sorry

My first thought was that such simple facts must be in Mathlib already. But I seemed to be wrong. Any advice about how I should go about proving such results? I am completely open to changing the definitions if that makes it easier to use existing results in Mathlib.

Another question I have is that I also tried an alternative definition of the type Perm:

def Perm α := {l : List α // l.length = Fintype.card α ∧ ∀ a, a ∈ l}

But Lean claims it fails to synthesize Fintype α, even though this has been explicitly declared. Why?

[Matt Diamond]

To answer your second question, it's because the α in your definition isn't the same α as the one in your variable declaration. When you write Perm α := ..., you're declaring an entirely new variable which also happens to be called α. If you want to reference the α from the variable statement, you'll need to remove the α from Perm's parameter list:

def Perm := {l : List α // l.length = Fintype.card α ∧ ∀ a, a ∈ l}

[Matt Diamond]

If you do that, you'll notice a bunch of errors in the rest of your code because your variable declaration defines α as an implicit variable. You can fix this easily by changing α to be explicit (i.e. (α : Type*) instead of {α : Type*}).

[Ching-Tsun Chou]

Thanks! That's very helpful.

[Matt Diamond]

Are you familiar with docs#Equiv.Perm ? it's a different way of representing permutations

[Matt Diamond]

docs#Fintype.card_perm is the cardinality result

[Matt Diamond]

and docs#fintypePerm is the Fintype instance

[Matt Diamond]

however, it represents permutations as automorphisms, rather than explicit orderings, so I'm not sure if that's useful

[Daniel Weber]

You can show an equivalence (Fin (Fintype.card α) ≃ α) ≃ Perm α to be able to use the results on Equiv.Perm (You can use docs#Fintype.truncEquivFin to convert Fin (Fintype.card α) to α)

[Ching-Tsun Chou]

Thanks for the suggestions! I'll look into them.

[Ching-Tsun Chou]

I don't understand the Trunc thing in  docs#Fintype.truncEquivFin and other similar results. What is it for?

[Ching-Tsun Chou]

Using the suggestions from Matt and Daniel, I modified my definitions to make them easier to work with:

noncomputable section

variable (α : Type*) [Fintype α] [DecidableEq α]

def Perm := α ≃ Fin (Fintype.card α)

instance fintype_perm : Fintype (Perm α) := Equiv.instFintype

theorem num_perms_all : Fintype.card (Perm α) = (Fintype.card α).factorial := by
  refine Fintype.card_equiv ?_
  exact Fintype.equivFinOfCardEq rfl

def hasSetPrefix (s : Finset α) : Finset (Perm α) :=
  { f : Perm α | ∀ a ∈ s, f.toFun a ≤ s.card }

theorem num_perms_set_prefix (s : Finset α) :
    (hasSetPrefix α s).card = s.card.factorial * (Fintype.card α - s.card).factorial := by
  sorry