1

I'm trying to prove time complexity of merge sort algorithm in Isabelle HOL:

theory Merge_Sort_Time
  imports Complex_Main "HOL-ex.BigO"
begin

fun merge :: "'a::linorder list ⇒ 'a list ⇒ 'a list" where
  "merge xs [] = xs"
| "merge [] ys = ys"
| "merge (x#xs) (y#ys) = (if x ≤ y then x # merge xs (y#ys)
                                   else y # merge (x#xs) ys)"

fun msort :: "'a::linorder list ⇒ 'a list" where
  "msort [] = []"
| "msort [x] = [x]"
| "msort xs = (let n = length xs div 2 in
               merge (msort (take n xs)) (msort (drop n xs)))"

fun msort_time :: "nat ⇒ real" where
  "msort_time 0 = 0"
| "msort_time (Suc 0) = 1"
| "msort_time n = msort_time (n div 2) + msort_time (n - n div 2) + n"

lemma msort_time_upper_bound:
  "msort_time ∈ O(λn. n * log 2 n)"
  sorry

end

The problem is that the lemma is unprovable because it doesn't hold for n = 1.

The lemma is expanded into:

msort_time ∈ {h. ∃c. ∀x. ¦h x¦ ≤ c * ¦x * log 2 x¦}

But probably it should be:

msort_time ∈ {h. ∃c n. ∀x ≥ n. ¦h x¦ ≤ c * ¦x * log 2 x¦}

Maybe I can use another library for Big O notation?

I've tried to prove the following lemma instead but got stuck:

lemma sum_log:
  "x > 0 ⟹ y > 0 ⟹
   x * log 2 x + y * log 2 y ≤ (x + y) * log 2 (x + y)"
  by (simp add: add_mono_thms_linordered_semiring(1) distrib_right)

lemma msort_time_upper_bound:
  "∃c. ∀n ≥ 2. msort_time n ≤ c * n * log 2 n"
proof
  let ?c = 3
  show "∀n ≥ 2. msort_time n ≤ ?c * n * log 2 n"
  proof
    fix n :: nat
    show "n ≥ 2 ⟶ msort_time n ≤ ?c * real n * log 2 n"
    proof
      assume "n ≥ 2"
      then show "msort_time n ≤ ?c * real n * log 2 n"
      proof (induct n rule: less_induct)
        case (less n)
        then show ?case
        proof -
          consider
            (n1) "n < 2" |
            (n2) "n = 2" |
            (n3) "n = 3" |
            (n4) "n ≥ 4"
            by arith
          then show "msort_time n ≤ ?c * real n * log 2 n"
          proof (cases)
            case n1
            then show ?thesis by (simp add: less.prems less_le_not_le)
          next
            case n2
            then show ?thesis by (simp add: numeral_2_eq_2)
          next
            case n3
            then have "msort_time n = 8"
              by (induct rule: msort_time.induct; simp)
            also have "... < ?c * n" by (simp add: n3)
            also have "... < ?c * n * log 2 n" by (simp add: n3)
            finally show ?thesis by linarith
          next
            case n4

            let ?a = "n div 2"
            let ?b = "n - ?a"

            have a: "2 ≤ ?a ∧ ?a < n" using n4 by simp_all
            have b: "2 ≤ ?b ∧ ?b < n" using n4 by simp_all

            have IH_a: "msort_time ?a ≤ ?c * real ?a * log 2 ?a"
              using a less.hyps by blast
            have IH_b: "msort_time ?b ≤ ?c * real ?b * log 2 ?b"
              using b less.hyps by blast

            have "msort_time n = msort_time ?a + msort_time ?b + n"
              by (metis dual_order.strict_iff_not less.prems lessI msort_time.elims not_numeral_le_zero numeral_2_eq_2)

            also have "... ≤ ?c * real ?a * log 2 ?a + ?c * real ?b * log 2 ?b + n"
              using IH_a IH_b by argo

            also have "... ≤ ?c * (real ?a + real ?b) * log 2 (real ?a + real ?b) + n"
              using sum_log[of ?a ?b] b by linarith

            also have "... ≤ ?c * n * log 2 n + n"
              by simp

            also have "... ≤ 2 * ?c * n * log 2 n"
              using n4 mult_ge1_I by simp

            finally show ?thesis
              sorry
          qed
        qed
      qed
    qed
  qed
qed

Could you please help to prove it?

Could you please give some suggestions on simplification of the proof. Is it possible to decrease number of nested proofs?

Improve this question
2

1 Answer 1

Reset to default
1

Here is a complete proof that msort_time is in O(n log n), which passes without errors in Isabelle2025:

theory Merge_Sort_Time
  imports Complex_Main "HOL-Library.Landau_Symbols"
begin

fun msort_time :: "nat ⇒ real" where
  "msort_time 0 = 0"
| "msort_time (Suc 0) = 1"
| "msort_time n = msort_time (n div 2) + msort_time (n - n div 2) + n"

lemma log2_bound: 
  "x ≥ 2 ⟹ log 2 (x + 1/2) ≤ log 2 x + 1"
proof-
  assume "x ≥ 2"
  then have "x + 1/2 ≤ 2 * x" by linarith
  then have "log 2 (x + 1/2) ≤ log 2 (2 * x)" by auto
  then show ?thesis using Transcendental.log_mult ‹x ≥ 2› by auto
qed

lemma msort_time_upper_bound:
  "n ≥ 2 ⟹ msort_time n ≤ 3 * n * log 2 n"
proof (induction rule: msort_time.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by simp
next
  case (3 n)
  consider (a) "n = 0" | (b) "n = 1" | (c) "n ≥ 2" by linarith
  then show ?case
  proof (cases)
    case a
    then show ?thesis by force
  next
    case b
    then show ?thesis apply simp by (smt (z3) log_le_one_cancel_iff)
  next
    case c
    then have "(Suc (Suc n) div 2) ≥ 2" "Suc (Suc n) - Suc (Suc n) div 2 ≥ 2" by simp+
    with 3 have IH:
      "msort_time (Suc (Suc n) div 2) ≤ 3 * real (Suc (Suc n) div 2) * log 2 (Suc (Suc n) div 2)"
      "msort_time (Suc (Suc n) - Suc (Suc n) div 2) ≤
       3 * real (Suc (Suc n) - Suc (Suc n) div 2) * log 2 (Suc (Suc n) - Suc (Suc n) div 2)" by argo+

    define m where "m = Suc (Suc n)"
    define k where "k = (real m) / 2"
    have "m ≥ 4" "k ≥ 2" unfolding m_def k_def using ‹n ≥ 2› by auto

    from IH have expr: "msort_time m ≤
      3 * real (Suc (Suc n) div 2) * log 2 (Suc (Suc n) div 2) +
      3 * real (Suc (Suc n) - Suc (Suc n) div 2) * log 2 (Suc (Suc n) - Suc (Suc n) div 2) + m"
      unfolding m_def by simp

    then show ?thesis
    proof (cases "m mod 2 = 0")
      case True
      then have "real (Suc (Suc n) div 2) = k" "real (Suc (Suc n) - Suc (Suc n) div 2) = k"
        unfolding k_def m_def by force+
      with expr have "msort_time m ≤ 3 * k * log 2 k + 3 * k * log 2 k + m" by metis
      also have "... ≤ 3 * (real m) * log 2 ((real m) / 2) + m" using k_def by force
      also have "... ≤ 3 * (real m) * (log 2 (real m) - 1) + m" using log_divide[of "2"] ‹m ≥ 4› by simp
      also have "... ≤ 3 * (real m) * log 2 (real m) - 3 * (real m) + m" by argo
      also have "... ≤ 3 * (real m) * log 2 (real m)" by auto
      finally show ?thesis unfolding m_def by blast
    next
      case False
      then have "real (Suc (Suc n) div 2) = k - 1/2"
        unfolding k_def m_def by (simp add: diff_divide_distrib field_char_0_class.of_nat_div)
      moreover have "real (Suc (Suc n) - Suc (Suc n) div 2) = k + 1/2"
        by (smt (verit) calculation div_le_dividend field_sum_of_halves k_def m_def of_nat_diff)
      ultimately have 
        "msort_time m ≤ 3 * (k - 1/2) * log 2 (k - 1/2) + 3 * (k + 1/2) * log 2 (k + 1/2) + m"
        using expr by presburger
      also have "... ≤ 3 * (k - 1/2) * log 2 k + 3 * (k + 1/2) * log 2 (k + 1 / 2) + m"
        using Transcendental.log_le_cancel_iff ‹k ≥ 2› by simp
      also have "... ≤ 3 * (k - 1/2) * log 2 k + 3 * (k + 1/2) * (log 2 k + 1) + m"
        using log2_bound ‹k ≥ 2› by auto
      also have "... ≤ 3 * 2 * k * log 2 k + 3 * (k + 1/2) + m" by argo
      also have "... ≤ 3 * (real m) * (log 2 (real m / 2)) + 3 * ((real m / 2) + 1/2) + m"
        unfolding k_def m_def by argo
      also have "... ≤ 3 * (real m) * (log 2 (real m) - 1) + 3/2 * real m + 3/2 + m"
        using log_divide[of "2"] ‹m ≥ 4› by auto
      also have "... ≤ 3 * (real m) * log 2 (real m) - 1/2 * (real m) + 3/2" by argo
      also have "... ≤ 3 * (real m) * log 2 (real m)" using ‹m ≥ 4› by simp
      finally show ?thesis unfolding m_def by blast
    qed
  qed
qed

lemma msort_time_nonneg: "msort_time n ≥ 0"
  by (induction rule: msort_time.induct) auto

lemma n_log_n_nonneg: "n ≥ 2 ⟹ (real n) * (log 2 (real n)) ≥ 0" by simp

lemma norm_nonneg: "x ≥ 0 ⟹ norm x = x" by simp

lemma msort_time_bigO:
  "msort_time ∈ O(λn. n * (log 2 n))"
  unfolding bigo_def
  apply (subst eventually_at_top_linorder)
  apply (rule Set.CollectI)
  using msort_time_upper_bound norm_nonneg[OF msort_time_nonneg] norm_nonneg[OF n_log_n_nonneg]
  by (metis mult.assoc zero_less_numeral)

end

Some notes on the proof:

  • Disclaimer: I don't really have experience with Big O in Isabelle specifically and I don't know whether there is a "standard" way to work with Big O in Isabelle, but it seems that the file HOL-Library.Landau_Symbols is frequently used. In this file, you have a definition of Big O basically corresponding to the "classical" definition of Big O, which requires that the inequality holds for all n greater than a constant.
lemma bigo_equiv: "(f::(real ⇒ real)) ∈ O(g) = (∃c > 0. ∃N. ∀n≥N. norm (f n) ≤ c * norm (g n))"
  unfolding bigo_def
  apply(subst eventually_at_top_linorder) by blast
  • If you want to prove a statement on a recursively defined function (msort_time in this case) it usually makes sense to use computation induction. Assuming you have a recursive function f which terminates, Isabelle/HOL automatically generates a custom induction principle based on the function definition, f.induct, which you can use as the induction rule.
  • For making proofs less complicated: It is often advisable to formulate lemma statements using Isabelle's meta-logic, instead of the first-order logic. For example, this means using the quantifier \And (which basically corresponds to $\bigwedge$ in LaTeX) instead of \forall, or leaving the quantifier out and making the quantification implicit. This usually allows you to prove things more directly and can make things easier for Isabelle's automation.
Improve this answer
Sign up to request clarification or add additional context in comments.

Comments

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.