# Theory Challenge1A

```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.›

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 (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```