Derangements formula

import data.equiv.basic
import data.fintype.basic
import data.fintype.card
import tactic.equiv_rw
import tactic.field_simp
import tactic.ring

open equiv fintype

section definitions

def is_derangement {α : Type*} (f : perm α) : Prop := (∀ x : α, f x ≠ x)

def derangements (α : Type*) := {f : perm α | is_derangement f}

end definitions


section derangement_lemmas

def derangement_congr {α β : Type*} (e : α ≃ β) : (derangements α ≃ derangements β) :=
begin
  refine subtype_equiv (perm_congr e) _,
  intro f,
  unfold derangements is_derangement,
  simp,
  rw ← not_iff_not,
  push_neg,
  split,
  {
    rintro ⟨x, hx_fixed⟩,
    use e x,
    simp [hx_fixed],
  },
  {
    rintro ⟨y, hy_fixed⟩,
    use e.symm y,
    apply e.injective,
    simp [hy_fixed],
  }
end

end derangement_lemmas


section ignore_two_cycle

variables {α : Type*} [decidable_eq α]

def is_two_cycle {α : Type*} (f : perm α) (a b : α) : Prop := f a = b ∧ f b = a

def perm_ignore_two_cycle (a b : α) :
{ f : perm α | is_two_cycle f a b } ≃ perm ({a, b}ᶜ : set α) :=
begin
  let a_and_b : set α := {a, b},

  let swap : perm α := equiv.swap a b,
  let swap' : perm a_and_b :=
  begin
    apply perm.subtype_perm swap,
    intro x,
    simp,
    split,
    {
      intro x_in,
      cases x_in; { simp [x_in] },
    },
    {
      contrapose!,
      rintro ⟨x_ne_a, x_ne_b⟩,
      simp [swap_apply_of_ne_of_ne x_ne_a x_ne_b],
      tauto,
    }
  end,

  transitivity {f : perm α // ∀ x : a_and_b, f x = swap' x},
  {
    apply subtype_equiv_right,
    intro σ,
    simp [is_two_cycle],
  },
  {
    -- TODO why can't it infer this is decidable?
    haveI : decidable_pred a_and_b := by
    {
      dsimp [decidable_pred, a_and_b],
      intro x,
      apply set.decidable_mem,
    },
    exact equiv.set.compl swap',
  },
end

-- TODO make this a simp lemma?
lemma perm_ignore_two_cycle_eq (a b : α) (f : perm α) (hf : is_two_cycle f a b) (c : ({a, b}ᶜ : set α)):
((perm_ignore_two_cycle a b) ⟨f, hf⟩ c : α) = f c :=
begin
  simp [perm_ignore_two_cycle, equiv.set.compl],
end

-- TODO this name definitely isn't up to snuff...
lemma perm_ignore_two_cycle_derangement_iff (a b : α) (hab : a ≠ b) (f : perm α) (hf : is_two_cycle f a b) :
is_derangement f ↔ is_derangement ((perm_ignore_two_cycle a b) ⟨f, hf⟩) :=
begin
  split,
  {
    rintros f_derangement ⟨x, hx⟩,
    apply subtype.ne_of_val_ne,
    simp [perm_ignore_two_cycle_eq, f_derangement x],
  },
  {
    -- easier to show that fixed point in f implies a fixed point
    -- in (f without a↔b)
    contrapose!,
    simp [is_derangement],

    --intro our fixed point and show that it's neither a nor b
    intros x x_fixed,
    have x_ne_a_b : ¬(x = a ∨ x = b),
    {
      intro contra,
      unfold is_two_cycle at hf,
      cases contra; { rw contra at x_fixed, cc },
    },

    use [x, x_ne_a_b],
    simp [subtype.ext_iff, perm_ignore_two_cycle_eq, x_fixed],
  }
end

end ignore_two_cycle


section splicing

variables {α : Type*} [decidable_eq α]

-- TODO feels like this should already exist? something something equiv_functor?
def equiv_compose (f : perm α) : perm (perm α) :=
{
  to_fun := λ g, g.trans f,
  inv_fun := λ g, g.trans f.symm,
  left_inv := λ g, by { simp [trans_assoc] },
  right_inv := λ g, by { simp [trans_assoc] },
}

-- TODO: maybe this should look more like (or even use!) `equiv.perm.decompose_option`
def perm_splice_out (a : α) :
∀ b : α, { f : perm α | f a = b } ≃ perm ({a}ᶜ : set α) :=
begin
  intro b,
  let just_a : set α := {a},

  transitivity {f : perm α // ∀ x : just_a, f x = equiv.refl just_a x},
  {
    -- we want to modify each permutation by composing it with (swap a and b)
    let compose_with_swap : perm (perm α) := equiv_compose (equiv.swap a b),

    apply equiv.trans (subtype_equiv_of_subtype' compose_with_swap) _,
    apply subtype_equiv_right,
    simp [compose_with_swap, equiv_compose],

    intro f,
    rw apply_eq_iff_eq_symm_apply,
    simp,
  },
  {
    apply equiv.set.compl,
  }
end

-- TODO should this be coe instead of val?
-- either way it should be consistent with perm_ignore_two_cycle_eq
lemma nicer_splice_lemma (a b : α) (f : perm α) (fa_eq_b : f a = b) (x : α) (hx : x ≠ a) :
(perm_splice_out a b ⟨f, fa_eq_b⟩ ⟨x, hx⟩).val = (swap a b) (f x) :=
begin
  simp [perm_splice_out, equiv.set.compl,
        subtype_equiv_of_subtype', subtype_equiv_of_subtype,
        equiv_compose],
end

lemma nice_splice_lemma (a b : α) (hab : a ≠ b) (f : perm α) (fa_eq_b : f a = b) :
f b ≠ a ∧ is_derangement f ↔
  (perm_splice_out a b) ⟨f, fa_eq_b⟩ ∈ derangements ({a}ᶜ : set α) :=
begin
  -- again, easier to show that fixed points lead to other fixed points
  rw ← not_iff_not,
  simp [derangements, is_derangement],
  rw imp_iff_not_or,
  simp,

  split,
  {
    -- if f has a fixed point, then so does (spliced-f). also happens if f b = a,
    -- because then b is a fixed point.
    rw or_imp_distrib,
    split,
    {
      intro fb_eq_a,
      use [b, hab.symm],
      simp [subtype.ext_iff_val, nicer_splice_lemma],
      apply_fun (swap a b),
      simpa,
    },
    {
      rintro ⟨x, x_fixed⟩,
      have x_ne_a : x ≠ a,
      {
        intro contra,
        rw contra at x_fixed,
        cc,
      },
      have x_ne_b : x ≠ b,
      {
        intro contra,
        rw contra at x_fixed,
        have : f a = f b, by cc,
        exact hab (f.injective this),
      },

      use [x, x_ne_a],
      simp [subtype.ext_iff_val, nicer_splice_lemma],
      apply_fun (swap a b),
      simp [x_fixed, swap_apply_of_ne_of_ne x_ne_a x_ne_b],
    }
  },
  {
    -- if (spliced-f) has a fixed point, it came from a pre-existing
    -- one, or it's b
    rintro ⟨x, x_ne_a, x_fixed⟩,
    simp [subtype.ext_iff_val, nicer_splice_lemma] at x_fixed,
    apply_fun (swap a b) at x_fixed,
    simp at x_fixed,

    by_cases x_vs_b : x = b,
    {
      left,
      simp [x_vs_b] at x_fixed,
      assumption,
    },
    {
      right,
      use x,
      rw swap_apply_of_ne_of_ne x_ne_a x_vs_b at x_fixed,
      assumption,
    }
  }
end


end splicing



section recursion

variables {α : Type*} [decidable_eq α]

def everything_but (a : α) : set α := {a}ᶜ

def neither_of (a : α) (b : everything_but a) : set α := {a, b}ᶜ

lemma special_1 (a : α) (b : everything_but a) :
{f : derangements α // is_two_cycle ↑f a b} ≃ derangements (neither_of a b) :=
begin
  cases b with b hab,

  -- TODO there's a few places i have to take subtypes of subtypes and merge
  -- their properties. is there an easier way to do this? (is that what `equiv_rw` can do?)
  transitivity {f' : {f : perm α // is_two_cycle f a b} // is_derangement f'.val},
  {
    apply equiv.trans
      (subtype_subtype_equiv_subtype_inter _ (λ f, is_two_cycle f a b))
      _,
    apply equiv.trans _ (subtype_subtype_equiv_subtype_inter _ _).symm,
    apply subtype_equiv_prop,
    tidy
  },

  have hab' : a ≠ b,
  {
    rintro rfl,
    simp [everything_but] at hab,
    exact hab,
  },

  refine subtype_equiv (perm_ignore_two_cycle a b) _,
  rintro ⟨f, hf⟩,
  exact perm_ignore_two_cycle_derangement_iff a b hab' f hf,
end


lemma special_2 (a : α) (b : everything_but a):
{f : derangements α // f a = b ∧ f b ≠ a} ≃ derangements (everything_but a) :=
begin
  cases b with b hab,

  transitivity {f' : {f : perm α // f a = b} // f'.val b ≠ a ∧ is_derangement f'.val},
  {
    apply equiv.trans
      (subtype_subtype_equiv_subtype_inter _ (λ f : perm α, f a = b ∧ f b ≠ a))
      _,
    apply equiv.trans
      _
      (subtype_subtype_equiv_subtype_inter _ (λ f : perm α, f b ≠ a ∧ is_derangement f)).symm,
    apply subtype_equiv_prop,
    tidy,
  },

  have hab' : a ≠ b,
  {
    rintro rfl,
    simp [everything_but] at hab,
    exact hab,
  },

  refine subtype_equiv (perm_splice_out a b) _,
  rintro ⟨f, hf⟩,
  exact nice_splice_lemma a b hab' f hf,
end


lemma spicy_lemma (a : α) (b : everything_but a) :
{f : derangements α // f a = b} ≃ (derangements (neither_of a b) ⊕ derangements (everything_but a)) :=
begin
  -- split the type into those that send b back to a, and those that don't
  let b_goes_back_to_a : derangements α → Prop := λ f, f b = a,

  refine equiv.trans (sum_compl (b_goes_back_to_a ∘ coe)).symm _,
  apply equiv.sum_congr,
  {
    exact (subtype_subtype_equiv_subtype_inter _ _).trans (special_1 a b),
  },
  {
    calc {f : {f : derangements α // f a = b} // ¬(b_goes_back_to_a ∘ coe) f }
        ≃ {f : derangements α // f a = b ∧ ¬b_goes_back_to_a f} : subtype_subtype_equiv_subtype_inter _ (not ∘ b_goes_back_to_a)
    ... ≃ derangements (everything_but a) : special_2 a b,
  },
end

theorem derangements_recursion_equiv (a : α):
derangements α ≃ Σ b : everything_but a, (derangements (neither_of a b) ⊕ derangements (everything_but a)) :=
begin
  -- the fiber over b = a is empty
  have fact : ∀ (b : α), {f : derangements α // f a = b} → b ∈ everything_but a,
  {
    rintros b ⟨⟨f, f_derangement⟩, fa_eq_b⟩,
    rw ← fa_eq_b,
    exact f_derangement a
  },

  calc derangements α
      ≃ Σ b : α, {f : derangements α // f a = b}
          : (sigma_preimage_equiv _).symm
  ... ≃ Σ b : everything_but a, {f : derangements α // f a = b}
          : (sigma_subtype_equiv_of_subset _ _ fact).symm
  ... ≃ Σ b : everything_but a, (derangements (neither_of a b) ⊕ derangements (everything_but a))
          : sigma_congr_right (spicy_lemma a),
end

end recursion



section finite_instances

variables {α : Type*} [decidable_eq α] [fintype α]

instance : decidable_pred (@is_derangement α) :=
begin
  intro f,
  apply fintype.decidable_forall_fintype,
end

instance : fintype (derangements α) :=
begin
  have : fintype (perm α) := by apply_instance,
  dsimp [derangements],
  exact set_fintype (set_of is_derangement),
end

instance (a : α) : fintype (everything_but a) :=
begin
  simp [everything_but],
  apply fintype.of_finset ({a}ᶜ : finset α),
  simp,
end

instance (a : α) (b : everything_but a) : fintype (neither_of a b) :=
begin
  simp [everything_but, neither_of],
  apply fintype.of_finset ({a, b}ᶜ : finset α),
  simp,
end


end finite_instances




section counting

def num_derangements (n : ℕ) : ℕ := card (derangements (fin n))

lemma num_derangements_invariant (α : Type*) [fintype α] [decidable_eq α] :
card (derangements α) = num_derangements (card α) :=
begin
  unfold num_derangements,
  apply card_eq.mpr,  -- eq because we don't need the specific equivalence
   -- TODO what's `trunc`? it's related to non-computability i think
  obtain ⟨e⟩ := equiv_fin α,
  use derangement_congr e,
end

theorem num_derangements_recursive (n : ℕ) :
num_derangements (n+2) = (n+1) * num_derangements n + (n+1) * num_derangements (n+1) :=
begin
  let X := fin(n+2),
  let star : X := 0, -- could be any element tbh

  have card_everything_but : card (everything_but star) = (n + 1),
  { simp [everything_but, finset.card_compl] },

  have card_neither_of : ∀ m : everything_but star, card (neither_of star m) = n,
  {
    simp [everything_but, finset.card_compl],
    intros m hm,

    suffices : finset.card ({star, m} : finset X) = 2,
    { simp [this] },

    -- TODO this is very clunky, what tricks can i use here?
    rw finset.card_insert_of_not_mem,
    { simp },
    {
      change _ ≠ _ at hm,
      simp [hm.symm],
    }
  },

  have card_der_1 : card (derangements (everything_but star)) = num_derangements (n+1),
  { rw [num_derangements_invariant, card_everything_but] },

  have card_der_2 : ∀ m : everything_but star, card (derangements (neither_of star m)) = num_derangements n,
  {
    intro m,
    rw num_derangements_invariant,
    rw card_neither_of
  },

  have key := card_congr (derangements_recursion_equiv star),
  rw num_derangements_invariant X at key,
  simp [card_der_1, card_der_2] at key,

  -- TODO dunno why this didn't work out with simp, but whatever
  simp [fintype.card] at card_everything_but,
  rw [key, card_everything_but],
  ring,
end

open_locale big_operators

theorem num_derangements_sum (n : ℕ) :
(num_derangements n : ℚ) = n.factorial * ∑ k in finset.range (n + 1), (-1 : ℚ)^k / k.factorial :=
begin
  refine nat.strong_induction_on n _,
  clear n, -- ???

  intros n hyp,

  -- need to knock out cases n = 0, 1
  cases n,
  { finish },  -- wow, what a tactic!

  cases n,
  { finish },

  -- now we have n ≥ 2
  rw num_derangements_recursive,
  push_cast,

  -- TODO can these proofs be inferred from some tactic?
  rw hyp n (nat.lt_succ_of_le (nat.le_succ _)),
  rw hyp n.succ (lt_add_one _),

  -- push all the constants inside the sums, strip off some trailing terms,
  -- and compare term-wise
  repeat { rw finset.mul_sum },
  conv_lhs {
    rw add_comm,
    congr,
    rw finset.sum_range_succ,
  },
  rw [add_assoc, ← finset.sum_add_distrib],

  conv_rhs {
    rw finset.sum_range_succ,
    rw finset.sum_range_succ,
    rw ← add_assoc,
  },

  congr,
  {
    -- delay factorial simplification until we're done clearing
    -- denominators
    field_simp [nat.factorial_ne_zero, -nat.factorial_succ, -nat.factorial],
    simp [nat.factorial_succ, pow_succ],
    ring,
  },
  {
    funext,
    field_simp [nat.factorial_ne_zero],
    ring,
  },
end


end counting