(* Title: A General Method for the Proof of Theorems on Tail-recursive Functions Author: Pasquale Noce Security Certification Specialist at Arjo Systems - Gep S.p.A. pasquale dot noce dot lavoro at gmail dot com pasquale dot noce at arjowiggins-it dot com *) section "Case study 1" theory CaseStudy1 imports Main begin text ‹ \null In the first case study, the problem will be examined of defining a function ‹l_sort› performing insertion sort on lists of elements of a linear order, and then proving the correctness of this definition, i.e. that the lists output by the function actually be sorted and contain as many occurrences of any value as the input lists. Such function constitutes a paradigmatic example of a function admitting a straightforward tail-recursive definition. Here below is a naive one: \null › fun l_sort_naive :: "'a::linorder list ⇒ 'a list ⇒ 'a list ⇒ 'a list" where "l_sort_naive (x # xs) ys [] = l_sort_naive xs [] (ys @ [x])" | "l_sort_naive (x # xs) ys (z # zs) = (if x ≤ z then l_sort_naive xs [] (ys @ x # z # zs) else l_sort_naive (x # xs) (ys @ [z]) zs)" | "l_sort_naive [] ys zs = zs" text ‹ \null The first argument is deputed to contain the values still having to be inserted into the sorted list, accumulated in the third argument. For each of such values, the items of the sorted list are orderly moved into a temporary one (second argument) to search the insertion position. Once found, the sorted list is restored, the processed value is moved from the unsorted list to the sorted one, and another iteration of the loop is performed up to the exhaustion of the former list. A further couple of functions are needed to express the aforesaid correctness properties of function ‹l_sort_naive›: \null › fun l_sorted :: "'a::linorder list ⇒ bool" where "l_sorted (x # x' # xs) = (x ≤ x' ∧ l_sorted (x' # xs))" | "l_sorted _ = True" definition l_count :: "'a ⇒ 'a list ⇒ nat" where "l_count x xs ≡ length [x'←xs. x' = x]" text ‹ \null Then, the target correctness theorems can be enunciated as follows: \null ‹l_sorted (l_sort_naive xs [] [])› \null ‹l_count x (l_sort_naive xs [] []) = l_count x xs› \null Unfortunately, attempts to apply recursion induction to such goals turn out to be doomed, as can easily be ascertained by considering the former theorem: \null › theorem "l_sorted (l_sort_naive xs [] [])" proof (rule l_sort_naive.induct [of "λxs ys zs. l_sorted (l_sort_naive xs ys zs)"], simp_all del: l_sort_naive.simps(3)) txt ‹ \null Simplification deletes all the subgoals generated by recursive equations. However, the following subgoal arises from the non-recursive one: \null @{subgoals [display]} \null which is hopeless as the formula is false for any unsorted list ‹zs›. \null › oops subsection "Step 1" type_synonym 'a l_type = "'a list × 'a list × 'a list" fun l_sort_aux :: "'a::linorder l_type ⇒ 'a l_type" where "l_sort_aux (x # xs, ys, []) = l_sort_aux (xs, [], ys @ [x])" | "l_sort_aux (x # xs, ys, z # zs) = (if x ≤ z then l_sort_aux (xs, [], ys @ x # z # zs) else l_sort_aux (x # xs, ys @ [z], zs))" | "l_sort_aux ([], ys, zs) = ([], ys, zs)" text ‹ \null Observe that the Cartesian product of the input types has been implemented as a product type. › subsection "Step 2" definition l_sort_in :: "'a list ⇒ 'a l_type" where "l_sort_in xs ≡ (xs, [], [])" definition l_sort_out :: "'a l_type ⇒ 'a list" where "l_sort_out X ≡ snd (snd X)" definition l_sort :: "'a::linorder list ⇒ 'a list" where "l_sort xs ≡ l_sort_out (l_sort_aux (l_sort_in xs))" text ‹ \null Since the significant inputs of function ‹l_sort_naive› match pattern ‹_›, ‹[]›, ‹[]›, those of function ‹l_sort_aux› match pattern ‹(_, [], [])›, thus being in a one-to-one correspondence with the type of the first component. The target correctness theorems can then be put into the following equivalent form: \null ‹l_sorted (l_sort xs)› \null ‹l_count x (l_sort xs) = l_count x xs› › subsection "Step 3" text ‹ The conditional recursive equation in the definition of function ‹l_sort_aux› will equivalently be associated to two distinct introduction rules in the definition of the inductive set ‹l_sort_set›, one for either truth value of the Boolean condition, handled as an additional assumption. The advantage is twofold: simpler introduction rules are obtained, and case distinctions are saved as rule induction is applied. \null › inductive_set l_sort_set :: "'a::linorder l_type ⇒ 'a l_type set" for X :: "'a l_type" where R0: "X ∈ l_sort_set X" | R1: "(x # xs, ys, []) ∈ l_sort_set X ⟹ (xs, [], ys @ [x]) ∈ l_sort_set X" | R2: "⟦(x # xs, ys, z # zs) ∈ l_sort_set X; x ≤ z⟧ ⟹ (xs, [], ys @ x # z # zs) ∈ l_sort_set X" | R3: "⟦(x # xs, ys, z # zs) ∈ l_sort_set X; ¬ x ≤ z⟧ ⟹ (x # xs, ys @ [z], zs) ∈ l_sort_set X" subsection "Step 4" lemma l_sort_subset: assumes XY: "Y ∈ l_sort_set X" shows "l_sort_set Y ⊆ l_sort_set X" proof (rule subsetI, erule l_sort_set.induct) show "Y ∈ l_sort_set X" using XY . next fix x xs ys assume "(x # xs, ys, []) ∈ l_sort_set X" thus "(xs, [], ys @ [x]) ∈ l_sort_set X" by (rule R1) next fix x xs ys z zs assume "(x # xs, ys, z # zs) ∈ l_sort_set X" and "x ≤ z" thus "(xs, [], ys @ x # z # zs) ∈ l_sort_set X" by (rule R2) next fix x xs ys z zs assume "(x # xs, ys, z # zs) ∈ l_sort_set X" and "¬ x ≤ z" thus "(x # xs, ys @ [z], zs) ∈ l_sort_set X" by (rule R3) qed lemma l_sort_aux_set: "l_sort_aux X ∈ l_sort_set X" proof (induction rule: l_sort_aux.induct, simp_all del: l_sort_aux.simps(2)) fix ys :: "'a list" and zs show "([], ys, zs) ∈ l_sort_set ([], ys, zs)" by (rule R0) next fix x :: 'a and xs ys have "(x # xs, ys, []) ∈ l_sort_set (x # xs, ys, [])" by (rule R0) hence "(xs, [], ys @ [x]) ∈ l_sort_set (x # xs, ys, [])" by (rule R1) hence "l_sort_set (xs, [], ys @ [x]) ⊆ l_sort_set (x # xs, ys, [])" by (rule l_sort_subset) moreover assume "l_sort_aux (xs, [], ys @ [x]) ∈ l_sort_set (xs, [], ys @ [x])" ultimately show "l_sort_aux (xs, [], ys @ [x]) ∈ l_sort_set (x # xs, ys, [])" by (rule subsetD) next fix x :: 'a and xs ys z zs assume case1: "x ≤ z ⟹ l_sort_aux (xs, [], ys @ x # z # zs) ∈ l_sort_set (xs, [], ys @ x # z # zs)" and case2: "¬ x ≤ z ⟹ l_sort_aux (x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys @ [z], zs)" have 0: "(x # xs, ys, z # zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule R0) show "l_sort_aux (x # xs, ys, z # zs) ∈ l_sort_set (x # xs, ys, z # zs)" proof (cases "x ≤ z", simp_all) assume "x ≤ z" with 0 have "(xs, [], ys @ x # z # zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule R2) hence "l_sort_set (xs, [], ys @ x # z # zs) ⊆ l_sort_set (x # xs, ys, z # zs)" by (rule l_sort_subset) moreover have "l_sort_aux (xs, [], ys @ x # z # zs) ∈ l_sort_set (xs, [], ys @ x # z # zs)" using case1 and ‹x ≤ z› by simp ultimately show "l_sort_aux (xs, [], ys @ x # z # zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule subsetD) next assume "¬ x ≤ z" with 0 have "(x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule R3) hence "l_sort_set (x # xs, ys @ [z], zs) ⊆ l_sort_set (x # xs, ys, z # zs)" by (rule l_sort_subset) moreover have "l_sort_aux (x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys @ [z], zs)" using case2 and ‹¬ x ≤ z› by simp ultimately show "l_sort_aux (x # xs, ys @ [z], zs) ∈ l_sort_set (x # xs, ys, z # zs)" by (rule subsetD) qed qed text ‹ \null The reader will have observed that the simplification rule arising from the second equation in the definition of function ‹l_sort_aux›, i.e. the one whose right-hand side contains a conditional, has been ignored in the initial backward steps of the previous proof. The reason is that it would actually make more complex the conclusion of the corresponding subgoal, as can easily be verified by trying to leave it enabled. \null › lemma "l_sort_aux X ∈ l_sort_set X" proof (induction rule: l_sort_aux.induct, simp_all) (*<*) prefer 2 (*>*) txt ‹ \null As a result of the application of the rule, the related subgoal takes the following form: \null @{subgoals [display, goals_limit = 1]} \null Now the conclusion is comprised of a conjunction of two implications. This is pointless, since case distinction is faster than the application of conjunction and implication introduction rules in providing sufficient assumptions for the simplification of both the induction hypotheses and the conclusion. \null › oops text ‹ \null These considerations clearly do not depend on the particular function under scrutiny, so that postponing the application of conditional simplification rules to case distinction turns out to be a generally advisable strategy for the accomplishment of step 4. › subsection "Step 5" text ‹ Two invariants are defined here below, one for each of the target correctness theorems: \null › fun l_sort_inv_1 :: "'a::linorder l_type ⇒ bool" where "l_sort_inv_1 (x # xs, y # ys, z # zs) = (l_sorted (y # ys) ∧ l_sorted (z # zs) ∧ last (y # ys) ≤ x ∧ last (y # ys) ≤ z)" | "l_sort_inv_1 (x # xs, y # ys, []) = (l_sorted (y # ys) ∧ last (y # ys) ≤ x)" | "l_sort_inv_1 (_, _, zs) = l_sorted zs" definition l_sort_inv_2 :: "'a ⇒ 'a list ⇒ 'a l_type ⇒ bool" where "l_sort_inv_2 x xs X ≡ (fst X = [] ⟶ fst (snd X) = []) ∧ l_count x (fst X) + l_count x (fst (snd X)) + l_count x (snd (snd X)) = l_count x xs" text ‹ \null More precisely, the second invariant, whose type has to match ‹'a l_type ⇒ bool› according to the method specification, shall be comprised of function ‹l_sort_inv_2 x xs›, where ‹x›, ‹xs› are the free variables appearing in the latter target theorem. Both of the above definitions are non-recursive; command ‹fun› is used in the former for the sole purpose of taking advantage of pattern matching. › subsection "Step 6" lemma l_sort_input_1: "l_sort_inv_1 (xs, [], [])" by simp lemma l_sort_input_2: "l_sort_inv_2 x xs (xs, [], [])" by (simp add: l_sort_inv_2_def l_count_def) subsection "Step 7" definition l_sort_form :: "'a l_type ⇒ bool" where "l_sort_form X ≡ fst X = []" lemma l_sort_intro_1: "l_sort_inv_1 X ⟹ l_sorted (l_sort_out X)" by (rule l_sort_inv_1.cases [of X], simp_all add: l_sort_out_def) lemma l_sort_intro_2: "⟦l_sort_inv_2 x xs X; l_sort_form X⟧ ⟹ l_count x (l_sort_out X) = l_count x xs" by (simp add: l_sort_inv_2_def, (erule conjE)+, simp add: l_sort_form_def l_sort_out_def l_count_def) subsection "Step 8" lemma l_sort_form_aux_all: "l_sort_form (l_sort_aux X)" by (rule l_sort_aux.induct [of "λX. l_sort_form (l_sort_aux X)"], simp_all add: l_sort_form_def) lemma l_sort_form_aux: "l_sort_form (l_sort_aux (xs, [], []))" by (rule l_sort_form_aux_all) subsection "Step 9" text ‹ The proof of the first invariance property requires the following lemma, stating that in case two lists are sorted, their concatenation still is such as long as the last item of the former is not greater than the first one of the latter. \null › lemma l_sorted_app [rule_format]: "l_sorted xs ⟶ l_sorted ys ⟶ last xs ≤ hd ys ⟶ l_sorted (xs @ ys)" proof (induction xs rule: l_sorted.induct, simp_all, (rule impI)+) fix x assume "l_sorted ys" and "x ≤ hd ys" thus "l_sorted (x # ys)" by (cases ys, simp_all) qed lemma l_sort_invariance_1: assumes XY: "Y ∈ l_sort_set X" and X: "l_sort_inv_1 X" shows "l_sort_inv_1 Y" using XY proof (rule l_sort_set.induct, simp_all) show "l_sort_inv_1 X" using X . next fix x :: 'a and xs ys assume I: "l_sort_inv_1 (x # xs, ys, [])" show "l_sorted (ys @ [x])" proof (cases ys, simp) fix a as assume "ys = a # as" hence "l_sorted ys ∧ last ys ≤ x" using I by simp moreover have "l_sorted [x]" by simp ultimately show ?thesis by (simp add: l_sorted_app) qed next fix x :: 'a and xs ys z zs assume XZ: "x ≤ z" and I: "l_sort_inv_1 (x # xs, ys, z # zs)" thus "l_sorted (ys @ x # z # zs)" proof (cases ys, simp) fix a as assume "ys = a # as" hence *: "l_sorted ys ∧ l_sorted (z # zs) ∧ last ys ≤ x" using I by simp with XZ have "l_sorted (x # z # zs)" by simp with * show ?thesis by (simp add: l_sorted_app) qed next fix x :: 'a and xs ys z zs assume "¬ x ≤ z" hence XZ: "z ≤ x" by simp assume "l_sort_inv_1 (x # xs, ys, z # zs)" thus "l_sort_inv_1 (x # xs, ys @ [z], zs)" proof (cases ys, simp) assume I: "l_sorted (z # zs)" show "l_sort_inv_1 (x # xs, [z], zs)" proof (cases zs, simp) show "z ≤ x" using XZ . next fix a as assume zs: "zs = a # as" then have *: "z ≤ a ∧ l_sorted zs" using I by simp have "l_sorted [z]" by simp with zs * show ?thesis using XZ by simp qed next fix a as assume YS: "ys = a # as" and "l_sort_inv_1 (x # xs, ys, z # zs)" hence I: "l_sorted ys ∧ l_sorted (z # zs) ∧ last ys ≤ z" by simp have "l_sorted [z]" by simp hence I': "l_sorted (ys @ [z])" using I by (simp add: l_sorted_app) show ?thesis proof (cases zs, simp) show "l_sort_inv_1 (x # xs, ys @ [z], [])" using I' and XZ and YS by simp next fix b bs assume zs: "zs = b # bs" then have "z ≤ b ∧ l_sorted zs" using I by simp with zs show ?thesis using I and I' and XZ and YS by simp qed qed qed text ‹ \null Likewise, the proof of the second invariance property calls for the following lemmas, stating that the number of occurrences of a value in a list is additive with respect to both item prepending and list concatenation. \null › lemma l_count_cons: "l_count x (y # ys) = l_count x [y] + l_count x ys" by (simp add: l_count_def) lemma l_count_app: "l_count x (ys @ zs) = l_count x ys + l_count x zs" by (simp add: l_count_def) lemma l_sort_invariance_2: assumes XY: "Y ∈ l_sort_set X" and X: "l_sort_inv_2 w ws X" shows "l_sort_inv_2 w ws Y" using XY proof (rule l_sort_set.induct) show "l_sort_inv_2 w ws X" using X . next fix x xs ys assume "l_sort_inv_2 w ws (x # xs, ys, [])" thus "l_sort_inv_2 w ws (xs, [], ys @ [x])" proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app) qed (simp add: l_count_def ac_simps) next fix x xs ys z zs assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)" thus "l_sort_inv_2 w ws (xs, [], ys @ x # z # zs)" proof (simp add: l_sort_inv_2_def, subst (asm) l_count_cons, subst l_count_app, subst l_count_cons) qed (simp add: l_count_def ac_simps) next fix x xs ys z zs assume "l_sort_inv_2 w ws (x # xs, ys, z # zs)" thus "l_sort_inv_2 w ws (x # xs, ys @ [z], zs)" proof (simp add: l_sort_inv_2_def, subst (asm) (2) l_count_cons, subst l_count_app) qed (simp add: l_count_def ac_simps) qed subsection "Step 10" theorem "l_sorted (l_sort xs)" proof - let ?X = "(xs, [], [])" have "l_sort_aux ?X ∈ l_sort_set ?X" by (rule l_sort_aux_set) moreover have "l_sort_inv_1 ?X" by (rule l_sort_input_1) ultimately have "l_sort_inv_1 (l_sort_aux ?X)" by (rule l_sort_invariance_1) hence "l_sorted (l_sort_out (l_sort_aux ?X))" by (rule l_sort_intro_1) moreover have "?X = l_sort_in xs" by (simp add: l_sort_in_def) ultimately show ?thesis by (simp add: l_sort_def) qed theorem "l_count x (l_sort xs) = l_count x xs" proof - let ?X = "(xs, [], [])" have "l_sort_aux ?X ∈ l_sort_set ?X" by (rule l_sort_aux_set) moreover have "l_sort_inv_2 x xs ?X" by (rule l_sort_input_2) ultimately have "l_sort_inv_2 x xs (l_sort_aux ?X)" by (rule l_sort_invariance_2) moreover have "l_sort_form (l_sort_aux ?X)" by (rule l_sort_form_aux) ultimately have "l_count x (l_sort_out (l_sort_aux ?X)) = l_count x xs" by (rule l_sort_intro_2) moreover have "?X = l_sort_in xs" by (simp add: l_sort_in_def) ultimately show ?thesis by (simp add: l_sort_def) qed end