Proving the correctness of an algorithm to partition lists in Isabelle

Question

I trying to prove correct an algorithm to split a list of integers into sublists of equal sum in linear time. Here you can see the algorithm I have chosen to do so.

I would like to get some feedback regarding:

1. The convenience of my definition for the splitting function.

2. The "induction" hypothesis to use in my situation.

Please, bear in mind that up to now I have only worked with apply-scripts and not with Isar proofs.

Here is a preliminary implementation of the algorithm and the correctness definition:

definition
  "ex_balanced_sum xs = (∃ ys zs. sum_list ys = sum_list zs ∧ 
                                  xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"


 fun check_list :: "int list ⇒ int ⇒ int ⇒ bool" where
    "check_list [] n acc = False" |
    "check_list (x#xs) n acc = (if n = acc then True else (check_list xs (n-x) (acc+x)))"

fun linear_split :: "int list ⇒ bool" where
"linear_split [] = False" |
"linear_split [x] = False" |
"linear_split (x # xs) = check_list xs (sum_list xs) x" 

The theorem to prove is as follows:

lemma linear_correct: "linear_split xs ⟷ ex_balanced_sum xs"

If I reason for instance for the first implication as:

lemma linear_correct_1: "linear_split xs ⟹ ex_balanced_sum xs"
  apply(induction xs rule: linear_split.induct)

Then I get a list of subgoals that I think are not appropriate:

1. linear_split [] ⟹ ex_balanced_sum []
2. ⋀x. linear_split [x] ⟹ ex_balanced_sum [x]
3. ⋀x v va. linear_split (x # v # va) ⟹ ex_balanced_sum (x # v # va)

In particular, these subgoals don't have an induction hypothesis! (am I right?). I tried to perform a different induction by just writing apply(induction xs) but then the goals look as:

1. linear_split [] ⟹ ex_balanced_sum []
2. ⋀a xs. (linear_split xs ⟹ ex_balanced_sum xs) ⟹ linear_split (a # xs) ⟹ ex_balanced_sum (a # xs)

Here the hypothesis is also not an induction hypothesis since it is assuming an implication.

So, what is the best way to define this function to get a nice induction hypothesis?

Edit (a one-function version)

fun check :: "int list ⇒ int ⇒ int ⇒ bool" where
"check [] n acc = False" |
"check [x] n acc = False" |
"check (x # y # xs) n acc = (if n-x = acc+x then True else check (y # xs) (n-x) (acc+x))"

definition "linear_split xs = check xs (sum_list xs) 0"

Answer 1

Background

I was able to prove the theorem linear_correct for a function (splitl) that is very similar to the function check in the statement of the question. Unfortunately, I would prefer not to make any attempts to convert the proof into an apply script.

The proof below is the first proof that came to my mind after I started investigating the question. Thus, there may exist better proofs.

---

Proof Outline

The proof is based on the induction based on the length of the list. In particular, assume

splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs

holds for all lists with the length less than l. If l = 1, then the result is easy to show. Assume, that l>=2. Then the list can be expressed in the form x#v#xs. In this case if it is possible to split the list using splitl, then it can be shown (splitl_reduce) that either

"splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" (1)

or

"x = sum_list (v#xs)" (2).

Thus, the proof proceeds by cases for (1) and (2). For (1), the length of the list is (x + v)#xs) is l-1. Hence, by the induction hypothesis ex_balanced_sum (x + v)#xs). Therefore, by the definition of ex_balanced_sum, also ex_balanced_sum x#v#xs. For (2), it can be easily seen that the list can be expressed as [x]@(v#xs) and, in this case, given (2), it satisfies the conditions of ex_balanced_sum by definition.

The proof for the other direction is similar and based on the converse of the lemma associated with (1) and (2) above: if "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0" or "x = sum_list (v#xs)", then "splitl (x#v#xs) (sum_list (x#v#xs)) 0".

---

theory so_ptcoaatplii
imports  Complex_Main

begin

definition
  "ex_balanced_sum xs = 
  (∃ ys zs. sum_list ys = sum_list zs ∧ xs = ys @ zs ∧ ys ≠ [] ∧ zs ≠ [])"

fun splitl :: "int list ⇒ int ⇒ int ⇒ bool" where
  "splitl [] s1 s2 = False" |
  "splitl [x] s1 s2 = False" |
  "splitl (x # xs) s1 s2 = ((s1 - x = s2 + x) ∨ splitl xs (s1 - x) (s2 + x))"

lemma splitl_reduce:
  assumes "splitl (x#v#xs) (sum_list (x#v#xs)) 0" 
  shows "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
proof -
  from assms have prem_cases: 
    "((x = sum_list (v#xs)) ∨ splitl (v#xs) (sum_list (v#xs)) x)" by auto
  {
    assume "splitl (v#xs) (sum_list (v#xs)) x"
    then have "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0"
    proof(induction xs arbitrary: x v)
      case Nil then show ?case by simp
    next
      case (Cons a xs) then show ?case by simp
    qed
  } 
  with prem_cases show ?thesis by auto
qed

(*Sledgehammered*)
lemma splitl_expand:
  assumes "splitl ((x + v)#xs) (sum_list ((x + v)#xs)) 0 ∨ x = sum_list (v#xs)"
  shows "splitl (x#v#xs) (sum_list (x#v#xs)) 0"
  by (smt assms list.inject splitl.elims(2) splitl.simps(3) sum_list.Cons)

lemma splitl_to_sum: "splitl xs (sum_list xs) 0 ⟹ ex_balanced_sum xs"
proof(induction xs rule: length_induct)
  case (1 xs) show ?case
  proof-
    obtain x v xst where x_xst: "xs = x#v#xst" 
      by (meson "1.prems" splitl.elims(2))
    have main_cases:
      "splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0 ∨ x = sum_list (v#xst)"
      by (rule splitl_reduce, insert x_xst "1.prems", rule subst)
    {
      assume "splitl ((x + v)#xst) (sum_list ((x + v)#xst)) 0"
      with "1.IH" x_xst have "ex_balanced_sum ((x + v)#xst)" by simp
      then obtain yst zst where 
        yst_zst: "(x + v)#xst = yst@zst" 
        and sum_yst_eq_sum_zst: "sum_list yst = sum_list zst"
        and yst_ne: "yst ≠ []" 
        and zst_ne: "zst ≠ []"
        unfolding ex_balanced_sum_def by auto
      then obtain ystt where ystt: "yst = (x + v)#ystt" 
        by (metis append_eq_Cons_conv)
      with sum_yst_eq_sum_zst have "sum_list (x#v#ystt) = sum_list zst" by simp
      moreover have "xs = (x#v#ystt)@zst" using x_xst yst_zst ystt by auto
      moreover have "(x#v#ystt) ≠ []" by simp
      moreover with zst_ne have "zst ≠ []" by simp
      ultimately have "ex_balanced_sum xs" unfolding ex_balanced_sum_def by blast
    }
    note prem = this
    {
      assume "x = sum_list (v#xst)"
      then have "sum_list [x] = sum_list (v#xst)" by auto
      moreover with x_xst have "xs = [x] @ (v#xst)" by auto
      ultimately have "ex_balanced_sum xs" using ex_balanced_sum_def by blast
    }
    with prem main_cases show ?thesis by blast
  qed
qed


lemma sum_to_splitl: "ex_balanced_sum xs ⟹ splitl xs (sum_list xs) 0"
proof(induction xs rule: length_induct)
  case (1 xs) show ?case
  proof -
    from "1.prems" ex_balanced_sum_def obtain ys zs where 
      ys_zs: "xs = ys@zs"
      and sum_ys_eq_sum_zs: "sum_list ys = sum_list zs"
      and ys_ne: "ys ≠ []"
      and zs_ne: "zs ≠ []"
      by blast
    have prem_cases: "∃y v yst. ys = (y#v#yst) ∨ (∃y. ys = [y])"
      by (metis remdups_adj.cases ys_ne)
    {
      assume "∃y. ys = [y]"
      then have "splitl xs (sum_list xs) 0"
        using splitl.elims(3) sum_ys_eq_sum_zs ys_zs zs_ne by fastforce
    }
    note prem = this
    {
      assume "∃y v yst. ys = (y#v#yst)"
      then obtain y v yst where y_v_yst: "ys = (y#v#yst)" by auto 
      then have 
        "sum_list ((y + v)#yst) = sum_list zs ∧ ((y + v)#yst) ≠ [] ∧ zs ≠ []"
        using sum_ys_eq_sum_zs zs_ne by auto
      then have ebs_ypv: "ex_balanced_sum (((y + v)#yst)@zs)"
        using ex_balanced_sum_def by blast
      have l_ypv: "length (((y + v)#yst)@zs) < length xs" 
        by (simp add: y_v_yst ys_zs)
      from l_ypv ebs_ypv have 
        "splitl (((y + v)#yst)@zs) (sum_list (((y + v)#yst)@zs)) 0"
        by (rule "1.IH"[THEN spec, rule_format])    
      with splitl_expand have splitl_ys_exp: 
        "splitl ((y#v#yst)@zs) (sum_list ((y#v#yst)@zs)) 0"
        by (metis Cons_eq_appendI)
      from ys_zs have "splitl xs (sum_list xs) 0" 
        by (rule ssubst, insert y_v_yst splitl_ys_exp, simp)
    }
    with prem prem_cases show ?thesis by auto
  qed  
qed

lemma linear_correct: "ex_balanced_sum xs ⟷ splitl xs (sum_list xs) 0"
  using splitl_to_sum sum_to_splitl by auto

end