section ‹Challenge 1.A› theory Challenge1A imports Main begin text ‹Problem definition: 🌐‹https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges%202019/ghc_sort.pdf›› subsection ‹Implementation› text ‹We phrase the algorithm as a functional program. Instead of a list of indexes for segment boundaries, we return a list of lists, containing the segments.› text ‹We start with auxiliary functions to take the longest increasing/decreasing sequence from the start of the list › fun take_incr :: "int list ⇒ _" where "take_incr [] = []" | "take_incr [x] = [x]" | "take_incr (x#y#xs) = (if x<y then x#take_incr (y#xs) else [x])" fun take_decr :: "int list ⇒ _" where "take_decr [] = []" | "take_decr [x] = [x]" | "take_decr (x#y#xs) = (if x≥y then x#take_decr (y#xs) else [x])" fun take where "take [] = []" | "take [x] = [x]" | "take (x#y#xs) = (if x<y then take_incr (x#y#xs) else take_decr (x#y#xs))" definition "take2 xs ≡ let l=take xs in (l,drop (length l) xs)" ― ‹Splits of a longest increasing/decreasing sequence from the list› text ‹The main algorithm then iterates until the whole input list is split› function cuts where "cuts xs = (if xs=[] then [] else let (c,xs) = take2 xs in c#cuts xs)" by pat_completeness auto subsection ‹Termination› text ‹First, we show termination. This will give us induction and proper unfolding lemmas.› lemma take_non_empty: "take xs ≠ []" if "xs ≠ []" using that apply (cases xs) apply clarsimp subgoal for x ys apply (cases ys) apply auto done done termination apply (relation "measure length") apply (auto simp: take2_def Let_def) using take_non_empty apply auto done declare cuts.simps[simp del] subsection ‹Correctness› subsubsection ‹Property 1: The Exact Sequence is Covered› lemma tdconc: "∃ys. xs = take_decr xs @ ys" apply (induction xs rule: take_decr.induct) apply auto done lemma ticonc: "∃ys. xs = take_incr xs @ ys" apply (induction xs rule: take_incr.induct) apply auto done lemma take_conc: "∃ys. xs = take xs@ys" using tdconc ticonc apply (cases xs rule: take.cases) by auto theorem concat_cuts: "concat (cuts xs) = xs" apply (induction xs rule: cuts.induct) apply (subst cuts.simps) apply (auto simp: take2_def Let_def) by (metis append_eq_conv_conj take_conc) subsubsection ‹Property 2: Monotonicity› text ‹We define constants to specify increasing/decreasing sequences.› fun incr where "incr [] ⟷ True" | "incr [_] ⟷ True" | "incr (x#y#xs) ⟷ x<y ∧ incr (y#xs)" fun decr where "decr [] ⟷ True" | "decr [_] ⟷ True" | "decr (x#y#xs) ⟷ x≥y ∧ decr (y#xs)" lemma tki: "incr (take_incr xs)" apply (induction xs rule: take_incr.induct) apply auto apply (case_tac xs) apply auto done lemma tkd: "decr (take_decr xs)" apply (induction xs rule: take_decr.induct) apply auto apply (case_tac xs) apply auto done lemma icod: "incr (take xs) ∨ decr (take xs)" apply (cases xs rule: take.cases) apply (auto simp: tki tkd simp del: take_incr.simps take_decr.simps) done theorem cuts_incr_decr: "∀c∈set (cuts xs). incr c ∨ decr c" apply (induction xs rule: cuts.induct) apply (subst cuts.simps) apply (auto simp: take2_def Let_def) using icod by blast subsubsection ‹Property 3: Maximality› text ‹Specification of a cut that consists of maximal segments: The segements are non-empty, and for every two neighbouring segments, the first value of the last segment cannot be used to continue the first segment: › fun maxi where "maxi [] ⟷ True" | "maxi [c] ⟷ c≠[]" | "maxi (c1#c2#cs) ⟷ (c1≠[] ∧ c2≠[] ∧ maxi (c2#cs) ∧ ( incr c1 ∧ ¬(last c1 < hd c2) ∨ decr c1 ∧ ¬(last c1 ≥ hd c2) ))" text ‹Obviously, our specification implies that there are no empty segments› lemma maxi_imp_non_empty: "maxi xs ⟹ []∉set xs" by (induction xs rule: maxi.induct) auto lemma tdconc': "xs≠[] ⟹ ∃ys. xs = take_decr xs @ ys ∧ (ys≠[] ⟶ ¬(last (take_decr xs) ≥ hd ys))" apply (induction xs rule: take_decr.induct) apply auto apply (case_tac xs) apply (auto split: if_splits) done lemma ticonc': "xs≠[] ⟹ ∃ys. xs = take_incr xs @ ys ∧ (ys≠[] ⟶ ¬(last (take_incr xs) < hd ys))" apply (induction xs rule: take_incr.induct) apply auto apply (case_tac xs) apply (auto split: if_splits) done lemma take_conc': "xs≠[] ⟹ ∃ys. xs = take xs@ys ∧ (ys≠[] ⟶ ( take xs=take_incr xs ∧ ¬(last (take_incr xs) < hd ys) ∨ take xs=take_decr xs ∧ ¬(last (take_decr xs) ≥ hd ys) ))" using tdconc' ticonc' apply (cases xs rule: take.cases) by auto lemma take_decr_non_empty: "take_decr xs ≠ []" if "xs ≠ []" using that apply (cases xs) apply auto subgoal for x ys apply (cases ys) apply (auto split: if_split_asm) done done lemma take_incr_non_empty: "take_incr xs ≠ []" if "xs ≠ []" using that apply (cases xs) apply auto subgoal for x ys apply (cases ys) apply (auto split: if_split_asm) done done lemma take_conc'': "xs≠[] ⟹ ∃ys. xs = take xs@ys ∧ (ys≠[] ⟶ ( incr (take xs) ∧ ¬(last (take xs) < hd ys) ∨ decr (take xs) ∧ ¬(last (take xs) ≥ hd ys) ))" using tdconc' ticonc' tki tkd apply (cases xs rule: take.cases) apply auto apply (auto simp add: take_incr_non_empty) apply (simp add: take_decr_non_empty) apply (metis list.distinct(1) take_incr.simps(3)) by (smt list.simps(3) take_decr.simps(3)) lemma [simp]: "cuts [] = []" apply (subst cuts.simps) by auto lemma [simp]: "cuts xs ≠ [] ⟷ xs ≠ []" apply (subst cuts.simps) apply (auto simp: take2_def Let_def) done lemma inv_cuts: "cuts xs = c#cs ⟹ ∃ys. c=take xs ∧ xs=c@ys ∧ cs = cuts ys" apply (subst (asm) cuts.simps) apply (cases xs rule: cuts.cases) apply (auto split: if_splits simp: take2_def Let_def) by (metis append_eq_conv_conj take_conc) theorem maximal_cuts: "maxi (cuts xs)" apply (induction "cuts xs" arbitrary: xs rule: maxi.induct) subgoal by auto subgoal for c xs apply (drule sym; simp) apply (subst (asm) cuts.simps) apply (auto split: if_splits prod.splits simp: take2_def Let_def take_non_empty) done subgoal for c1 c2 cs xs apply (drule sym) apply simp apply (drule inv_cuts; clarsimp) apply auto subgoal by (metis cuts.simps list.distinct(1) take_non_empty) subgoal by (metis append.left_neutral inv_cuts not_Cons_self) subgoal using icod by blast subgoal by (metis Nil_is_append_conv cuts.simps hd_append2 inv_cuts list.distinct(1) same_append_eq take_conc'' take_non_empty) subgoal by (metis append_is_Nil_conv cuts.simps hd_append2 inv_cuts list.distinct(1) same_append_eq take_conc'' take_non_empty) done done subsubsection ‹Equivalent Formulation Over Indexes› text ‹After the competition, we got the comment that a specification of monotonic sequences via indexes might be more readable. We show that our functional specification is equivalent to a specification over indexes.› fun ii_induction where "ii_induction [] = ()" | "ii_induction [_] = ()" | "ii_induction (_#y#xs) = ii_induction (y#xs)" locale cnvSpec = fixes fP P assumes [simp]: "fP [] ⟷ True" assumes [simp]: "fP [x] ⟷ True" assumes [simp]: "fP (a#b#xs) ⟷ P a b ∧ fP (b#xs)" begin lemma idx_spec: "fP xs ⟷ (∀i<length xs - 1. P (xs!i) (xs!Suc i))" apply (induction xs rule: ii_induction.induct) using less_Suc_eq_0_disj by auto end locale cnvSpec' = fixes fP P P' assumes [simp]: "fP [] ⟷ True" assumes [simp]: "fP [x] ⟷ P' x" assumes [simp]: "fP (a#b#xs) ⟷ P' a ∧ P' b ∧ P a b ∧ fP (b#xs)" begin lemma idx_spec: "fP xs ⟷ (∀i<length xs. P' (xs!i)) ∧ (∀i<length xs - 1. P (xs!i) (xs!Suc i))" apply (induction xs rule: ii_induction.induct) apply auto [] apply auto [] apply clarsimp by (smt less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc) end interpretation INCR: cnvSpec incr "(<)" apply unfold_locales by auto interpretation DECR: cnvSpec decr "(≥)" apply unfold_locales by auto interpretation MAXI: cnvSpec' maxi "λc1 c2. ( ( incr c1 ∧ ¬(last c1 < hd c2) ∨ decr c1 ∧ ¬(last c1 ≥ hd c2) ))" "λx. x ≠ []" apply unfold_locales by auto lemma incr_by_idx: "incr xs = (∀i<length xs - 1. xs ! i < xs ! Suc i)" by (rule INCR.idx_spec) lemma decr_by_idx: "decr xs = (∀i<length xs - 1. xs ! i ≥ xs ! Suc i)" by (rule DECR.idx_spec) lemma maxi_by_idx: "maxi xs ⟷ (∀i<length xs. xs ! i ≠ []) ∧ (∀i<length xs - 1. incr (xs ! i) ∧ ¬ last (xs ! i) < hd (xs ! Suc i) ∨ decr (xs ! i) ∧ ¬ hd (xs ! Suc i) ≤ last (xs ! i) )" by (rule MAXI.idx_spec) theorem all_correct: "concat (cuts xs) = xs" "∀c∈set (cuts xs). incr c ∨ decr c" "maxi (cuts xs)" "[] ∉ set (cuts xs)" using cuts_incr_decr concat_cuts maximal_cuts maxi_imp_non_empty[OF maximal_cuts] by auto end