Theory Derangements_Enum

section"Derangements"
theory Derangements_Enum
  imports
    "HOL-Combinatorics.Multiset_Permutations"
    "Common_Lemmas"
   (* "Derangements.Derangements" *)
begin

subsection"Definition"

fun no_overlap :: "'a list ⇒ 'a list ⇒ bool" where
  "no_overlap _ [] = True"
| "no_overlap [] _ = True"
| "no_overlap (x#xs) (y#ys) = (x ≠ y ∧ no_overlap xs ys)"

lemma no_overlap_nth: "length xs = length ys ⟹ i < length xs ⟹ no_overlap xs ys ⟹ xs ! i ≠ ys ! i" 
  by(induct xs ys arbitrary: i rule: list_induct2) (auto simp: less_Suc_eq_0_disj)

lemma nth_no_overlap: "length xs = length ys ⟹ ∀ i < length xs. xs ! i ≠ ys ! i ⟹ no_overlap xs ys"
proof (induct xs ys rule: list_induct2)
  case (Cons x xs y ys)
  then show ?case using Suc_less_eq nth_Cons_Suc by fastforce
qed simp 
  
definition derangements :: "'a list ⇒ 'a list set" where
  "derangements xs = {ys. distinct ys ∧ length xs = length ys ∧ set xs = set ys ∧ no_overlap xs ys }"
text "A derangement of a list is a permutation where every element changes its position,
  assuming all elements are distinguishable."
text ‹An alternative definition exists in ‹Derangements.Derangements› \cite{AFPderan}.›
text "Cardinality: ‹count_derangements (length xs)› (from ‹Derangements.Derangements›)"
text "Example: ‹derangements [0,1,2] = {[1,2,0], [2,0,1]}›"

subsection"Algorithm"
fun derangement_enum_aux :: "'a list ⇒ 'a list ⇒ 'a list list" where
  "derangement_enum_aux [] ys = [[]]"
| "derangement_enum_aux (x#xs) ys = [y#r . y ← ys, r ← derangement_enum_aux xs (remove1 y ys), y ≠ x]"

fun derangement_enum :: "'a list  ⇒ 'a list list" where
 "derangement_enum xs = derangement_enum_aux xs xs"

subsection"Verification"

subsubsection"Correctness"

lemma derangement_enum_aux_elem_length: "zs ∈ set (derangement_enum_aux xs ys) ⟹ length xs = length zs"
  by(induct xs arbitrary: ys zs) auto

lemma derangement_enum_aux_not_in: "y ∉ set ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ y ∉ set zs"
proof(induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  then obtain z zs2 where ob: "zs = z#zs2"
    by auto
  have "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys)) ⟹ y ∉ set zs2"
    using Cons notin_set_remove1 by fast
  then show ?case using Cons ob
    by auto
qed

lemma derangement_enum_aux_in: "y ∈ set zs ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ y ∈ set ys"
  using derangement_enum_aux_not_in by fast
  
lemma derangement_enum_aux_distinct_elem: "distinct ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ distinct zs"
proof(induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  obtain z zs2 where ob: "zs = z#zs2"
    using Cons by auto
  then have ev: "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
    using Cons ob by auto

  have "distinct zs2"
    using ev Cons distinct_remove1 by fast
  moreover have "z ∉ set zs2"
    using ev Cons(2) derangement_enum_aux_in by fastforce
  ultimately show ?case using ob by simp
qed

lemma derangement_enum_aux_no_overlap: "zs ∈ set (derangement_enum_aux xs ys) ⟹ no_overlap xs zs"
  by(induct xs arbitrary: zs ys) auto

lemma derangement_enum_aux_set:
  "length xs = length ys ⟹ zs ∈ set (derangement_enum_aux xs ys) ⟹ set zs = set ys"
proof(induct xs ys arbitrary: zs rule: derangement_enum_aux.induct)
  case (1 ys)
  then show ?case by simp
next
  case (2 x xs ys)
  obtain z zs2 where ob: "zs = z#zs2"
    using 2 by auto
  have ev1: "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
    using 2 ob  by simp
  have ev2:"z ∈ set ys"
    using 2 ob by simp

  have "length xs = length (remove1 z ys)"
    using ev2 Suc_length_remove1 "2.prems"(1) by force
  then have "set zs2 = set (remove1 z ys)"
    using "2.hyps"[of z zs2] ev1 ev2  by simp

  then show ?case
    using ob notin_set_remove1 ev2 in_set_remove1 by fastforce
qed

lemma derangement_enum_correct_aux1:
  "⟦distinct zs;length ys = length zs; length ys = length xs; set ys = set zs; no_overlap xs zs⟧
   ⟹ zs ∈ set (derangement_enum_aux xs ys)"
proof(induct xs arbitrary: zs ys)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  obtain z zs2 where ob: "zs = z#zs2"
    using Cons length_0_conv neq_Nil_conv by metis

  have e1: "z ≠ x"
    using Cons.prems(5) ob  by auto

  have "distinct zs2"
    using Cons.prems(1) ob by auto 
  moreover have "length (remove1 z ys) = length zs2" using Cons.prems ob
    by (simp add: length_remove1) 
  moreover have "length (remove1 z ys) = length xs"
    by (simp add: Cons.prems(3) Cons.prems(4) length_remove1 ob) 
  moreover have "set (remove1 z ys) = set zs2"
    using Cons ob by (metis distinct_card distinct_remdups length_remdups_eq remove1.simps(2) set_remdups set_remove1_eq)
  moreover have "no_overlap xs zs2"
    using Cons.prems(5) ob by fastforce 

  ultimately have "zs2 ∈ set (derangement_enum_aux xs (remove1 z ys))"
    using Cons.hyps[of zs2 "(remove1 z ys)"] by simp
  then show ?case
    using ob e1 Cons by simp 
qed

theorem derangement_enum_correct: "distinct xs ⟹ derangements xs = set (derangement_enum xs)"
proof(standard)
  show "distinct xs ⟹ derangements xs ⊆ set (derangement_enum xs)"
    unfolding derangements_def using derangement_enum_correct_aux1 by auto 
next
  show "distinct xs ⟹ set (derangement_enum xs) ⊆ derangements xs"
    unfolding derangements_def
    using derangement_enum_aux_set derangement_enum_aux_distinct_elem derangement_enum_aux_elem_length derangement_enum_aux_no_overlap
    by auto
qed

subsubsection"Distinctness"

lemma derangement_enum_aux_distinct: "distinct ys ⟹ distinct (derangement_enum_aux xs ys)"
proof(induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  show ?case
    using inj2_distinct_concat_map_function_filter[of
        "Cons"
         ys
         "λy. derangement_enum_aux xs (remove1 y ys)"
        "λy. y ≠ x"
      ]
    using Cons Cons_inj2
    by (simp)
qed

theorem derangement_enum_distinct: "distinct xs ⟹ distinct (derangement_enum xs)"
  using derangement_enum_aux_distinct by auto

(*
subsubsection"Cardinality"
should be provable with Derangements.Derangements
*)

end