Theory Rank_Util

theory Rank_Util
  imports "HOL-Library.Multiset"
          Count_Util
          "SuffixArray.Prefix"
begin

section "Rank Definition"

text ‹Count how many occurrences of an element are in a certain index in the list›

text ‹Definition 3.7 from \<^cite>‹"Cheung_CPP_2025"›: Rank›
definition rank :: "'a list ⇒ 'a ⇒ nat ⇒ nat"
  where
"rank s x i ≡ count_list (take i s) x"

section "Rank Properties"

subsection "List Properties"

lemma rank_cons_same:
  "rank (x # xs) x (Suc i) = Suc (rank xs x i)"
  by (simp add: rank_def)

lemma rank_cons_diff:
  "a ≠ x ⟹ rank (a # xs) x (Suc i) = rank xs x i"
  by (simp add: rank_def)

subsection "Counting Properties"

lemma rank_length:
  "rank xs x (length xs) = count_list xs x"
  by (simp add: rank_def)

lemma rank_gre_length:
  "length xs ≤ n ⟹ rank xs x n = count_list xs x"
  by (simp add: rank_def)

lemma rank_not_in:
  "x ∉ set xs ⟹ rank xs x i = 0"
  by (metis gr_zeroI in_count rank_def set_take_subset subset_code(1))

lemma rank_0:
  "rank xs x 0 = 0"
  by (simp add: rank_def)

text ‹Theorem 3.11 from \<^cite>‹"Cheung_CPP_2025"›: Rank Equivalence›
lemma rank_card_spec:
  "rank xs x i = card {j. j < length xs ∧ j < i ∧ xs ! j = x}"
proof -
  have "rank xs x i = count_list (take i xs) x"
    by (meson rank_def)
  moreover
  have "count_list (take i xs) x = card {j. j < length (take i xs) ∧ (take i xs) ! j = x}"
    by (metis count_list_card)
  moreover
  have "{j. j < length (take i xs) ∧ (take i xs) ! j = x} = 
        {j. j < length xs ∧ j < i ∧ xs ! j = x}"
    by fastforce
  ultimately show ?thesis
    by simp
qed


lemma le_rank_plus_card:
  "i ≤ j ⟹
   rank xs x j = rank xs x i + card {k. k < length xs ∧ i ≤ k ∧ k < j ∧ xs ! k = x}"
proof -
  assume "i ≤ j"

  let ?X = "{k. k < length xs ∧ k < j ∧ xs ! k = x}"
  have "rank xs x j = card ?X"
    by (simp add: rank_card_spec)
  moreover
  let ?Y = "{k. k < length xs ∧ k < i ∧ xs ! k = x}"
  have "rank xs x i = card ?Y"
    by (simp add: rank_card_spec)
  moreover
  let ?Z = "{k. k < length xs ∧ i ≤ k ∧ k < j ∧ xs ! k = x}"
  have "?Y ∪ ?Z = ?X"
  proof safe
    fix k
    assume "k < i"
    then show "k < j"
      using ‹i ≤ j› order_less_le_trans by blast
  next
    fix k
    assume "¬ i ≤ k"
    then show "k < i"
      using linorder_le_less_linear by blast
  qed
  moreover
  have "?Y ∩ ?Z = {}"
    by force
  hence "card (?Y ∪ ?Z) = card ?Y + card ?Z"
    by (simp add: card_Un_disjoint)
  ultimately show ?thesis
    by presburger
qed

subsection "Bound Properties"

lemma rank_lower_bound:
  assumes "k < rank xs x i"
  shows "k < i"
proof -
  from rank_card_spec[of xs x i]
  have "rank xs x i = card {j. j < length xs ∧ j < i ∧ xs ! j = x}" .
  hence "k < card {j. j < length xs ∧ j < i ∧ xs ! j = x}"
    using assms by presburger
  moreover
  {
    have "i ≤ length xs ∨ length xs < i"
      using linorder_not_less by blast
    moreover
    have "i ≤ length xs ⟹ {j. j < length xs ∧ j < i ∧ xs ! j = x} ⊆ {0..<i}"
      using atLeast0LessThan by blast
    hence "i ≤ length xs ⟹ card {j. j < length xs ∧ j < i ∧ xs ! j = x} ≤ i"
      using subset_eq_atLeast0_lessThan_card by presburger
    moreover
    have "length xs < i ⟹ {j. j < length xs ∧ j < i ∧ xs ! j = x} ⊆ {0..<length xs}"
      using atLeast0LessThan by blast
    hence "length xs < i ⟹ card {j. j < length xs ∧ j < i ∧ xs ! j = x} ≤ length xs"
      using subset_eq_atLeast0_lessThan_card by presburger
    hence "length xs < i ⟹ card {j. j < length xs ∧ j < i ∧ xs ! j = x} ≤ i"
      by linarith
    ultimately have "card {j. j < length xs ∧ j < i ∧ xs ! j = x} ≤ i"
      by blast
  }
  ultimately show ?thesis
    using dual_order.strict_trans1 by blast
qed

corollary rank_Suc_ex:
  assumes "k < rank xs x i"
  shows "∃l. i = Suc l"
  by (metis Nat.lessE assms rank_lower_bound)

lemma rank_upper_bound:
  "⟦i < length xs; xs ! i = x⟧ ⟹ rank xs x i < count_list xs x"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case
    by (simp add: rank_def)
next
  case (Cons a xs i)
  then show ?case
  proof (cases i)
    case 0
    then show ?thesis
      by (metis Cons.prems(2) count_in list.set_intros(1) nth_Cons_0 rank_0)
  next
    case (Suc n)
    then show ?thesis
      by (metis Cons.hyps Cons.prems Suc_less_eq length_Cons nth_Cons_Suc rank_cons_diff 
                rank_cons_same rank_length)
  qed
qed

lemma rank_idx_mono:
  "i ≤ j ⟹ rank xs x i ≤ rank xs x j"
proof (cases "i = j")
  assume "i = j"
  then show ?thesis
    by simp
next
  assume "i ≤ j" "i ≠ j"
  hence "i < j"
    using antisym_conv2 by blast
  hence "prefix xs j = prefix xs i @ list_slice xs i j"
    by (metis ‹i ≤ j› append_take_drop_id list_slice.elims min.absorb1 take_take)
  hence "rank xs x j = rank xs x i + count_list (list_slice xs i j) x"
    by (metis count_list_append rank_def)
  then show ?thesis
    by fastforce
qed

lemma rank_less:
  "⟦i < length xs; i < j; xs ! i = x⟧ ⟹ rank xs x i < rank xs x j"
proof -
  let ?X = "{k. k < length xs ∧ i ≤ k ∧ k < j ∧ xs ! k = x}"
  assume "i < length xs" "i < j" "xs ! i = x"
  with le_rank_plus_card[of i j xs x]
  have "rank xs x j = rank xs x i + card ?X"
    using nless_le by blast
  moreover
  have "i ∈ ?X"
    using ‹i < j› ‹i < length xs› ‹xs ! i = x› by blast
  hence "card ?X > 0"
    using card_gt_0_iff by fastforce
  ultimately show ?thesis
    by linarith
qed

lemma rank_upper_bound_gen:
  "rank xs x i ≤ count_list xs x"
  by (metis nat_le_linear rank_gre_length rank_idx_mono)


subsection "Sorted Properties"

lemma sorted_card_rank_idx:
  assumes "sorted xs"
  and     "i < length xs"
shows "i = card {j. j < length xs ∧ xs ! j < xs ! i} + rank xs (xs ! i) i"
proof -

  let ?A = "{j. j < length xs ∧ xs ! j < xs ! i}"
  let ?B = "{j. j < length xs ∧ xs ! j = xs ! i}"


  have "?B ≠ {}"
    using assms(2) by blast

  have "Min ?B ∈ ?B"
    by (metis (no_types, lifting) Min_in ‹?B ≠ {}› finite_nat_set_iff_bounded mem_Collect_eq)
  hence "Min ?B < length xs" "xs ! (Min ?B) = xs ! i"
    by simp_all

  have "Min ?B ≤ i"
    by (simp add: assms(2))

  have P: "∀k < Min ?B. xs ! k < xs ! i"
  proof (intro allI impI)
    fix k
    assume "k < Min ?B"
    with sorted_nth_mono[OF assms(1) _ ‹Min ?B < length xs›]
    have "xs ! k ≤ xs ! (Min ?B)"
      using le_eq_less_or_eq by presburger
    
    show "xs ! k < xs ! i"
    proof (rule ccontr)
      assume "¬ xs ! k < xs ! i"
      with ‹xs ! k ≤ xs ! (Min ?B)› ‹xs ! (Min ?B) = xs ! i›
      have "xs ! k = xs ! i"
        by order
      with ‹k < Min ?B› ‹Min ?B < length xs›
      have "k ∈ ?B"
        by auto
      then show False
        by (metis (mono_tags, lifting) Min_gr_iff ‹k < Min ?B› ‹?B ≠ {}› finite_nat_set_iff_bounded 
                                       less_irrefl_nat mem_Collect_eq)
    qed
  qed

  have "?A = {0..<Min ?B}"
  proof (intro equalityI subsetI)
    fix x
    assume "x ∈ ?A"
    hence "x < length xs" "xs ! x < xs ! i"
      by blast+
    hence "xs ! x < xs ! Min ?B"
      using ‹xs ! Min ?B = xs ! i› by simp
    hence "x < Min ?B"
      using assms(1) ‹x < length xs› ‹Min ?B < length xs›
      by (meson dual_order.strict_iff_not not_le_imp_less sorted_nth_mono)
    then show "x ∈ {0..<Min ?B}"
      using atLeastLessThan_iff by blast
  next
    fix x 
    assume "x ∈ {0..<Min ?B}"
    with P ‹Min ?B < length xs›
    show "x ∈ ?A"
      by auto
  qed
  moreover
  {
    let ?C = "{j. j < length xs ∧ j < i ∧ xs ! j = xs ! i}"
    from rank_card_spec[of xs "xs ! i" i]
    have "rank xs (xs ! i) i = card ?C" .
    moreover
    have "?C = {Min ?B..<i}" 
    proof (intro equalityI subsetI)
      fix x
      assume "x ∈ ?C"
      hence "x < length xs" "x < i" "xs ! x = xs ! i"
        by blast+
      hence "Min ?B ≤ x"
        by simp
      with ‹x < i›
      show "x ∈ {Min ?B..<i}"
        using atLeastLessThan_iff by blast
    next
      fix x
      assume "x ∈ {Min ?B..<i}"
      hence "Min ?B ≤ x" "x < i"
        using atLeastLessThan_iff by blast+
      moreover
      have "xs ! x = xs ! i"
      proof -
        have "xs ! x ≤ xs ! i"
          using assms(1,2) ‹x < i› 
          by (simp add: sorted_wrt_nth_less)
        moreover
        have "xs ! Min ?B ≤ xs ! x"
          using assms(1,2) ‹Min ?B ≤ x› ‹x < i›
          by (meson order.strict_trans sorted_iff_nth_mono)
        ultimately show ?thesis
          using ‹xs ! Min ?B = xs ! i› by order
      qed
      ultimately show "x ∈ ?C"
        using assms(2) by fastforce
    qed
    ultimately have "rank xs (xs ! i) i = card {Min ?B..<i}"
      by presburger
  }
  ultimately show ?thesis
    by (simp add: ‹Min ?B ≤ i›)
qed

lemma sorted_rank:
  assumes "sorted xs"
  and     "i < length xs"
  and     "xs ! i = a"
shows "rank xs a i = i - card {k. k < length xs ∧ xs ! k < a}"
  using assms(1) assms(2) assms(3) sorted_card_rank_idx by fastforce

lemma sorted_rank_less:
  assumes "sorted xs"
  and     "i < length xs"
  and     "xs ! i < a"
shows "rank xs a i = 0"
proof -
  have "rank xs a i = card {k. k < length xs ∧ k < i ∧ xs ! k = a}"
    by (simp add: rank_card_spec)
  moreover
  have "{k. k < length xs ∧ k < i ∧ xs ! k = a} = {}"
    using assms sorted_wrt_nth_less by fastforce
  ultimately show ?thesis
    by fastforce
qed

lemma sorted_rank_greater:
  assumes "sorted xs"
  and     "i < length xs"
  and     "xs ! i > a"
shows "rank xs a i = count_list xs a"
proof -
  let ?A = "{k. k < length xs ∧ k < i ∧ xs ! k = a}"
  have "rank xs a i = card ?A"
    by (simp add: rank_card_spec)
  moreover
  let ?B = "{k. k < length xs ∧ k ≥ i ∧ xs ! k = a}"
  let ?C = "{k. k < length xs ∧ xs ! k = a}"
  {
    have "?A ∪ ?B = ?C"
    proof safe
      fix x
      assume "¬ i ≤ x"
      then show "x < i"
        using linorder_le_less_linear by blast
    qed
    moreover
    have "?B = {}"
    proof -
      have "∀k < length xs. k ≥ i ⟶ xs ! k > a"
        by (meson assms(1) assms(3) dual_order.strict_trans1 sorted_nth_mono)
      then show ?thesis
        by blast
    qed
    ultimately have "?A = ?C"
      by blast
  }
  ultimately show ?thesis
    by (simp add: count_list_card)
qed

end