# Theory Sorting_PDQ

```theory Sorting_PDQ
imports Sorting_Setup Sorting_Partially_Sorted Sorting_Pdq_Insertion_Sort Sorting_Heapsort Sorting_Log2
begin

subsection ‹Auxiliary Definitions›

lemma slice_split_part: "l≤m ⟹ m<h ⟹ h≤length xs ⟹ slice l h xs = slice l m xs @ xs!m # slice (Suc m) h xs"
by (metis less_imp_le slice_append slice_split_hd)

(* The set properties *)

context weak_ordering begin
lemma sorted_wrt_slice_iff_nth_less: "⟦ l≤h; h≤length xs ⟧ ⟹ sorted_wrt R (slice l h xs) ⟷ (∀i j. l≤i ∧ i<j ∧ j<h ⟶ R (xs!i) (xs!j))"
unfolding sorted_wrt_iff_nth_less
apply (clarsimp simp: slice_nth)
apply auto

lemma range_leq_set_slice_conv:
"h≤length xs ⟹ (∀i∈{l..<h}. xs!i ❙≤ pv) ⟷ (∀x∈set (slice l h xs). x❙≤pv)"
"h≤length xs ⟹ (∀i∈{l..<h}. xs!i ❙≥ pv) ⟷ (∀x∈set (slice l h xs). x❙≥pv)"
by (auto simp: set_slice_conv Ball_def)

text ‹Predicate to express that slice is partitioned›
definition "partitioned pv xs l h m ≡
l≤m ∧ m<h ∧ h≤length xs
∧ (∀i∈{l..<m}. xs!i ❙≤ pv)
∧ xs!m = pv
∧ (∀i∈{m<..<h}. xs!i ❙≥ pv)"

lemma partitioned_alt: "partitioned pv xs l h m ⟷
l≤m ∧ m<h ∧ h≤length xs
∧ (∀x∈set (slice l m xs). x ❙≤ pv)
∧ xs!m = pv
∧ (∀x∈set (slice (m+1) h xs). x ❙≥ pv)"
unfolding partitioned_def
apply (rule iffI)
subgoal by (auto simp: in_set_conv_nth slice_nth) []
subgoal by (auto simp: range_leq_set_slice_conv[symmetric])
done

text ‹Shuffling a partition does not change partitioned property›
lemma shuffle_pres_part:
"partitioned pv xs⇩1 l h m ⟹ slice_eq_mset l m xs⇩1 xs⇩2 ⟹ partitioned pv xs⇩2 l h m"
"partitioned pv xs⇩1 l h m ⟹ slice_eq_mset (Suc m) h xs⇩1 xs⇩2 ⟹ partitioned pv xs⇩2 l h m"
unfolding partitioned_alt
(* TODO: Clean up proof *)
apply (clarsimp_all simp: slice_eq_mset_alt )
apply (clarsimp_all simp: slice_eq_mset_eq_length eq_outside_range_nth slice_eq_outside_range dest: mset_eq_setD)
apply (clarsimp_all simp: slice_eq_mset_alt )
apply (auto simp:  eq_outside_range_nth slice_eq_outside_range dest: mset_eq_setD)
done

text ‹After sorting the partitions, the whole slice is sorted.›
lemma parts_sorted_imp_sorted:
assumes "partitioned pv xs l h m"
assumes "sorted_wrt_lt (❙<) (slice l m xs)"
assumes "sorted_wrt_lt (❙<) (slice (Suc m) h xs)"
shows "sorted_wrt_lt (❙<) (slice l h xs)"
using assms
unfolding partitioned_def
apply (clarsimp simp: slice_nth le_by_lt sorted_wrt_slice_iff_nth_less)
by (metis (no_types, lifting) Suc_leI atLeastLessThan_iff greaterThanLessThan_iff linorder_neqE_nat local.trans)

end

(*
Configuration options for Pdqsort
*)
abbreviation "is_threshold ≡ 16::nat"  (* TODO/FIXME: replace by pdq_is_threshold, and remove *)
abbreviation "pdq_is_threshold ≡ 24"

abbreviation "ninther_threshold ≡ 128::nat"

context weak_ordering begin
subsection ‹Phases of Quicksort Scheme›

definition "part_range_cond xs l h ≡ (
∃i∈{l+1..<h}. xs!i ❙≤ xs!l)
∧ (∃i∈{l+1..<h}. xs!i ❙≥ xs!l)"

text ‹Pivot has been selected and moved to front›
definition "R_PV_TO_FRONT l h xs xs' ≡ l+1<h ∧ h≤length xs ∧ slice_eq_mset l h xs xs' ∧ part_range_cond xs' l h"

text ‹Slice has been partitioned›
definition "R_PART pv l h m xs xs' ≡ l≤m ∧ m<h ∧ h≤length xs ∧ slice_eq_mset l h xs xs' ∧ partitioned pv xs' l h m"

text ‹Left partition has been sorted›
definition "R_SORT_L pv l h m xs xs' ≡ R_PART pv l h m xs xs' ∧ sorted_wrt_lt (❙<) (slice l m xs')"

text ‹Right partition has been sorted›
definition "R_SORT_R pv l h m xs xs' ≡ R_SORT_L pv l h m xs xs' ∧ sorted_wrt_lt (❙<) (slice (Suc m) h xs')"

text ‹When right partition has been sorted, the whole slice is already sorted. ›
lemma R_SORT_R_sorted: "R_SORT_R pv l h m xs xs' ⟹ slice_eq_mset l h xs xs' ∧ sorted_wrt_lt (❙<) (slice l h xs')"
unfolding R_SORT_R_def R_SORT_L_def R_PART_def
by (auto simp: parts_sorted_imp_sorted)

text ‹Sorting the whole partition, e.g., due to heapsort fallback›
lemma R_PART_SORT: "R_PART pv l h m xs xs' ⟹ slice_sort_spec (❙<) xs' l h ≤ SPEC (λxs''. slice_eq_mset l h xs xs'' ∧ sorted_wrt_lt (❙<) (slice l h xs''))"
unfolding slice_sort_spec_sem_alt R_PART_def
apply refine_vcg
apply (auto simp: slice_eq_mset_eq_length dest: slice_eq_mset_trans)
done

subsection ‹Specifications of Subroutines›

text ‹Move pivot to front›
definition "pivot_to_front_spec xs l h ≡ doN {
ASSERT (l + 4 < h ∧ h ≤ length xs);
SPEC (λxs'.
slice_eq_mset l h xs xs'
∧ part_range_cond xs' l h
)
}"

lemma pivot_to_front_spec_rl: "⟦ l + 4 < h; h≤length xs ⟧ ⟹ pivot_to_front_spec xs l h ≤ SPEC (λxs'. R_PV_TO_FRONT l h xs xs')"
unfolding pivot_to_front_spec_def R_PV_TO_FRONT_def
by auto

text ‹Partition›
definition "partition_spec xs l h ≡ doN {
ASSERT (
l + 1 < h ∧ h ≤ length xs
∧ part_range_cond xs l h
);
SPEC (λ(alrp::bool,m,xs').
slice_eq_mset l h xs xs'
∧ l≤m ∧ m<h
∧ partitioned (xs!l) xs' l h m
)
}"

definition "partition_left_spec ≡ partition_spec" (* No discrimination required on this abs-level *)

lemma partition_spec_rl: "R_PV_TO_FRONT l h xs⇩0 xs ⟹ partition_spec xs l h ≤ SPEC (λ(_,m,xs'). m<h ∧ R_PART (xs!l) l h m xs⇩0 xs')"
unfolding partition_spec_def R_PV_TO_FRONT_def R_PART_def
apply refine_vcg
by (auto simp: slice_eq_mset_eq_length dest: slice_eq_mset_trans)

lemma aux1:
assumes BOUNDS: "l ≤ m" "m < h" "h ≤ length xs'"
assumes NOT_LESS: "¬ prev ❙< pv"
assumes PART: "partitioned pv xs' l h m"
assumes LPART: "∀x∈set (slice l h xs'). prev ❙≤ x"
shows "
⟦0 < l; part_range_cond xs l h; slice_eq_mset l h xs xs' ⟧
⟹ sorted_wrt_lt (❙<) (slice l m xs')"
proof -

from NOT_LESS have "pv ❙≤ prev" using wo_leI by blast

from PART have LEFT_PART_LE: "∀i∈{l..<m}. xs'!i ❙≤ pv"
unfolding partitioned_def by auto

from LPART have PREV_LE: "∀i∈{l..<h}. prev ❙≤ xs'!i"
using assms(3) range_leq_set_slice_conv(2) by blast

{
fix i j
assume "l≤i" "i<j" "j<m"
hence "xs'!i ❙≤ xs'!j"
by (meson LEFT_PART_LE PREV_LE ‹pv ❙≤ prev› assms(2) atLeastLessThan_iff le_less_trans less_imp_le_nat local.trans)
}
then show "sorted_wrt_lt (❙<) (slice l m xs')"
using BOUNDS
by (auto simp: sorted_wrt_slice_iff_nth_less le_by_lt)
qed

text ‹Correctness lemma for the partition-left optimization for many equal elements.›
lemma partition_left_spec_rl: "⟦R_PV_TO_FRONT l h xs⇩0 xs; 0<l; ¬(xs!(l-1) ❙< xs!l); (∀x∈set (slice l h xs⇩0). xs⇩0!(l-1) ❙≤ x) ⟧
⟹ partition_left_spec xs l h ≤ SPEC (λ(_,m,xs'). m<h ∧ R_SORT_L (xs!l) l h m xs⇩0 xs')"
unfolding partition_spec_def partition_left_spec_def R_PV_TO_FRONT_def R_PART_def R_SORT_L_def
apply refine_vcg
apply (auto simp: slice_eq_mset_eq_length slice_eq_mset_nth_outside slice_eq_mset_set_inside aux1 dest: slice_eq_mset_trans)
done

text ‹Shuffle. We only specify that the partitions must contain the same elements.›
definition "shuffle_spec xs l h m ≡ doN {
ASSERT (l≤m ∧ m<h ∧ h≤length xs);
SPEC (λ(unbal,xs').
eq_outside_range xs xs' l h
∧ mset (slice l m xs) = mset (slice l m xs')
∧ xs!m = xs'!m
∧ mset (slice (m+1) h xs) = mset (slice (m+1) h xs')
)
}"

lemma shuffle_rule: "⟦R_PART pv l h m xs⇩0 xs⟧ ⟹ shuffle_spec xs l h m ≤ SPEC (λ(_,xs'). R_PART pv l h m xs⇩0 xs')"
unfolding R_PART_def shuffle_spec_def partitioned_alt
apply refine_vcg
apply (auto simp: slice_eq_mset_alt eq_outside_rane_lenD dest: mset_eq_setD)
subgoal for xs⇩2
apply (rewrite in "⌑ = _" slice_split_part; simp add: eq_outside_rane_lenD)
apply (rewrite in "_ = ⌑" slice_split_part; simp add: eq_outside_rane_lenD)
done
done

text ‹Maybe-Sort: The specification nondeterministically decides whether to sort or not.
In any case, the elements are permutated.
›
lemma maybe_sort_rule1: "R_PART pv l h m xs⇩0 xs ⟹ maybe_sort_spec xs l m
≤ SPEC (λ(r,xs'). (r⟶R_SORT_L pv l h m xs⇩0 xs') ∧ R_PART pv l h m xs⇩0 xs')"
unfolding maybe_sort_spec_def R_PART_def R_SORT_L_def
apply (refine_vcg)
apply (clarsimp_all simp: slice_eq_mset_eq_length)
subgoal by (meson eq_imp_le less_imp_le slice_eq_mset_subslice slice_eq_mset_trans)
subgoal using shuffle_pres_part(1) by blast
subgoal by (meson less_or_eq_imp_le slice_eq_mset_subslice slice_eq_mset_trans)
subgoal using shuffle_pres_part(1) by blast
done

lemma maybe_sort_rule2: "R_SORT_L pv l h m xs⇩0 xs ⟹ maybe_sort_spec xs (Suc m) h
≤ SPEC (λ(r,xs'). (r⟶R_SORT_R pv l h m xs⇩0 xs') ∧ (¬r ⟶ R_SORT_L pv l h m xs⇩0 xs'))"
unfolding maybe_sort_spec_def R_PART_def  R_SORT_L_def R_SORT_R_def
apply (refine_vcg)
apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
subgoal
by (meson le_SucI nat_in_between_eq(2) order.strict_implies_order slice_eq_mset_subslice slice_eq_mset_trans)
subgoal
using shuffle_pres_part(2) by blast
subgoal
by (meson le_SucI le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans)
subgoal
using shuffle_pres_part(2) by blast
done

lemma sort_rule1: "R_PART pv l h m xs⇩0 xs ⟹ slice_sort_spec (❙<) xs l m
≤ SPEC (λxs'. R_SORT_L pv l h m xs⇩0 xs')"
unfolding slice_sort_spec_sem_alt R_PART_def  R_SORT_L_def R_SORT_R_def
apply (refine_vcg)
apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
subgoal by (meson le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans)
subgoal using shuffle_pres_part(1) by blast
done

lemma sort_again_rule1: "R_SORT_L pv l h m xs⇩0 xs ⟹ slice_sort_spec (❙<) xs l m
≤ SPEC (λxs'. R_SORT_L pv l h m xs⇩0 xs')"
unfolding slice_sort_spec_sem_alt R_PART_def  R_SORT_L_def R_SORT_R_def
apply (refine_vcg)
apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
subgoal by (meson le_refl less_imp_le_nat slice_eq_mset_subslice slice_eq_mset_trans)
subgoal using shuffle_pres_part(1) by blast
done

lemma sort_rule2: "R_SORT_L pv l h m xs⇩0 xs ⟹ slice_sort_spec (❙<) xs (Suc m) h
≤ SPEC (λxs'. R_SORT_R pv l h m xs⇩0 xs')"
unfolding slice_sort_spec_sem_alt R_PART_def R_SORT_L_def R_SORT_R_def
apply (refine_vcg)
apply (clarsimp_all simp: slice_eq_mset_eq_length slice_eq_mset_eq_outside(1))
subgoal by (meson le_Suc_eq less_imp_le_nat nat_in_between_eq(2) slice_eq_mset_subslice slice_eq_mset_trans)
subgoal using shuffle_pres_part(2) by blast
done

text ‹Fallback sorting. Will be instantiated by Heapsort later.›
definition "fallback_sort_spec ≡ slice_sort_spec (❙<)"

subsection ‹Abstract Pdqsort›
text ‹Recursive Pdqsort function.›
definition "pdqsort_aux leftmost xs l h (d::nat) ≡ RECT (λpdqsort_aux (leftmost,xs,l,h,d). doN {
ASSERT (l≤h ∧ h≤length xs ∧ 0<d);
ASSERT (¬leftmost ⟶ l>0 ∧ (∀x∈set (slice l h xs). xs!(l-1) ❙≤ x));

if (h-l < pdq_is_threshold) then
pdq_guarded_sort_spec leftmost xs l h
else doN {
xs ← pivot_to_front_spec xs l h;

ASSERT (l-1<length xs ∧ l<length xs);
ASSERT (¬leftmost ⟶ l>0);
if (¬leftmost ∧ ¬(xs!(l-1) ❙< xs!l)) then doN {
(_,m,xs) ← partition_left_spec xs l h;
ASSERT (m<h);
pdqsort_aux (False,xs,m+1,h,d)
} else doN {
(alrp,m,xs) ← partition_spec xs l h;
(unbal,xs) ← shuffle_spec xs l h m;

ASSERT (0<d);
let d = (if unbal then d-1 else d);

(didsort,xs) ←
if d=0 then doN {xs ← fallback_sort_spec xs l h; RETURN (True,xs)}
else if alrp ∧ ¬unbal then doN {
(r,xs) ← maybe_sort_spec xs l m;
if r then doN {
ASSERT (m<h);
maybe_sort_spec xs (m+1) h
} else RETURN (False,xs)
} else RETURN (False,xs);

if didsort then RETURN xs
else doN { ⌦‹TODO: Test optimization of not sorting left partition again, if maybe_sort sorted it›
xs ← pdqsort_aux (leftmost,xs,l,m,d);
ASSERT (m<h);
xs ← pdqsort_aux (False,xs,m+1,h,d);
RETURN xs
}
}
}

}) (leftmost,xs,l,h,d)"

(*
The correctness proof is some manual fiddling with the VCG,
but essentially uses the lemmas proved above.
*)
lemma pdqsort_aux_correct:
assumes "l≤h" "h≤length xs" "¬leftmost ⟹ l>0 ∧ (∀x∈set (slice l h xs). xs!(l-1) ❙≤ x)" "d>0"
shows "pdqsort_aux leftmost xs l h d ≤ slice_sort_spec (❙<) xs l h"
unfolding pdqsort_aux_def fallback_sort_spec_def

apply (rule order_trans)
apply (rule RECT_rule[where
V="measure (λ(leftmost,xs,l,h,d). h-l)"
and pre="λ(leftmost,xs,l,h,d). l≤h ∧ h≤length xs ∧ 0<d ∧ (¬leftmost ⟶ l>0 ∧ (∀x∈set (slice l h xs). xs!(l-1) ❙≤ x))"
and M="λ(leftmost,xs,l,h,d). slice_sort_spec (❙<) xs l h"
], refine_mono)

subgoal by simp
subgoal using assms by auto
subgoal premises prems for pdqsort args proof -

obtain leftmost xs l h d where [simp]: "args = (leftmost, xs, l, h, d)" by (cases args)

note IH = prems(1)
note LEFTMOST = prems(2)

{
fix pv m xs xs' and d'::nat
assume "R_SORT_L pv l h m xs xs'" and "0<d'"
hence "pdqsort (False,xs',Suc m,h,d') ≤ SPEC (λxs''. R_SORT_R pv l h m xs xs'')"
apply -
apply (rule order_trans[OF IH])
subgoal by (simp add: R_SORT_L_def R_PART_def partitioned_alt)
subgoal by (auto simp add: R_SORT_L_def R_PART_def partitioned_alt)
done
} note rec_sort_r_rl = this

{
fix pv m xs' and d'::nat
assume "R_PART pv l h m xs xs'" and "0<d'"
hence "pdqsort (leftmost,xs',l,m,d') ≤ SPEC (λxs''. R_SORT_L pv l h m xs xs'')"
apply -
apply (rule order_trans[OF IH])
subgoal using LEFTMOST
apply (clarsimp simp: R_PART_def slice_eq_mset_eq_length slice_eq_mset_nth_outside slice_eq_mset_set_inside)
apply (drule set_rev_mp[OF _ set_slice_subsetI, of _ l m _ l h])
by auto
subgoal by (auto simp add: R_SORT_L_def R_PART_def partitioned_alt)
done
} note rec_sort_l_rl = this

{
fix pv m xs' and d'::nat
assume "R_SORT_L pv l h m xs xs'" and "0<d'"
hence "pdqsort (leftmost,xs',l,m,d') ≤ SPEC (λxs''. R_SORT_L pv l h m xs xs'')"
using rec_sort_l_rl unfolding R_SORT_L_def by blast
} note rec_sort_l_again_rl = this

show ?thesis
apply (rewrite in "_≤⌑" slice_sort_spec_sem_alt)
apply (cases args,simp)
apply (refine_vcg pivot_to_front_spec_rl partition_spec_rl partition_left_spec_rl shuffle_rule; assumption?)
using LEFTMOST
apply (clarsimp_all simp: slice_eq_mset_eq_length eq_outside_rane_lenD)
apply (all ‹assumption?›)
subgoal
apply refine_vcg
by (auto simp: unfold_le_to_lt)
subgoal by simp
subgoal unfolding R_PV_TO_FRONT_def by (auto simp: slice_eq_mset_eq_length)
subgoal unfolding R_PV_TO_FRONT_def by (auto simp: slice_eq_mset_eq_length)
subgoal
apply (refine_vcg rec_sort_r_rl, assumption)
by (clarsimp_all simp: R_SORT_R_sorted)
subgoal
apply (all ‹erule maybe_sort_rule1[THEN order_trans]›)
apply (all ‹refine_vcg›)
apply clarsimp_all
apply (all ‹(erule maybe_sort_rule2[THEN order_trans])?›)
apply (all ‹(refine_vcg)?›)
apply (clarsimp_all simp: R_SORT_R_sorted)
subgoal
apply (refine_vcg rec_sort_l_again_rl, assumption)
apply (refine_vcg rec_sort_r_rl, assumption)
by (clarsimp_all simp: R_SORT_R_sorted)
subgoal
apply (refine_vcg rec_sort_l_rl, assumption)
apply (refine_vcg rec_sort_r_rl, assumption)
by (clarsimp_all simp: R_SORT_R_sorted)
done
subgoal
apply (intro conjI impI)
subgoal
apply (refine_vcg rec_sort_l_rl, assumption, simp)
apply (refine_vcg rec_sort_r_rl, assumption, simp)
by (clarsimp_all simp: R_SORT_R_sorted)
subgoal
apply (refine_vcg rec_sort_l_rl, assumption)
apply (refine_vcg rec_sort_r_rl, assumption)
by (clarsimp_all simp: R_SORT_R_sorted)
done
done
qed
subgoal by simp
done

text ‹Main Pdqsort function. Just a wrapper for the recursive function,
initializing the maximum number of bad partitions before switching to fallback sorting.›
definition "pdqsort xs l h ≡ doN {
ASSERT (l≤h);
let size = h-l;
if (size>1) then pdqsort_aux True xs l h (Discrete.log size)
else RETURN xs
}"

lemma pdqsort_correct: "pdqsort xs l h ≤ slice_sort_spec (❙<) xs l h"
proof -
have log_pos_aux: "1<x ⟹ 0 < Discrete.log x" for x
apply (subst log_rec) by auto

{
assume "l≤h" "h≤length xs"
hence ?thesis
unfolding pdqsort_def
apply (cases "1 < h-l"; simp)
subgoal by (rule pdqsort_aux_correct; simp add: log_pos_aux)
subgoal unfolding slice_sort_spec_def sort_spec_def by refine_vcg (auto simp: sorted_wrt01)
done
} thus ?thesis unfolding slice_sort_spec_def by (simp only: pw_le_iff refine_pw_simps) blast
qed

subsection ‹Implementation of Subroutines›

definition "sort_two xs i j ≡ doN {
ASSERT (i<length xs ∧ j<length xs ∧ i≠j);
if⇩N mop_cmp_idxs xs j i then mop_list_swap xs i j else RETURN xs

⌦‹if (xs!j ❙< xs!i) then mop_list_swap xs i j else RETURN xs›
}"

definition "sort_three xs i j k ≡ doN {
xs ← sort_two xs i j;
xs ← sort_two xs j k;
xs ← sort_two xs i j;
RETURN xs
}"

lemma sort_three_rule: "⟦
{i,j,k}⊆{l..<h}; i≠j; i≠k; j≠k; h≤length xs
⟧ ⟹ sort_three xs i j k ≤ SPEC (λxs'. slice_eq_mset l h xs xs' ∧ xs'!i ❙≤ xs'!j ∧ xs'!j ❙≤ xs'!k ∧ (∀l∈-{i,j,k}. xs!l=xs'!l))"
unfolding sort_three_def sort_two_def
apply simp
apply (simp add: swap_nth unfold_le_to_lt split: if_splits)
done

definition "three_sorted xs i j k ≡ {i,j,k} ⊆ {0..<length xs} ∧ xs!i ❙≤ xs!j ∧ xs!j ❙≤ xs!k"

lemma sort_three_sorted_rl: "sort_three xs⇩1 i j k ≤ SPEC (λxs⇩2. length xs⇩1=length xs⇩2 ∧ slice_eq_mset l h xs⇩1 xs⇩2 ∧ three_sorted xs⇩2 i j k)"
if "{i,j,k}⊆{l..<h}" "i≠j" "i≠k" "j≠k" "l<h" "h≤length xs⇩1" for i j k and xs⇩1 xs⇩2 :: "'a list"
using that
apply (refine_vcg sort_three_rule[where l=l and h=h])
apply (auto simp: slice_eq_mset_eq_length three_sorted_def)
done

lemma three_sorted_imp_part_range_cond: "⟦ three_sorted xs i l k; l<i; l<k; i<h; k<h ⟧ ⟹ part_range_cond xs l h"
unfolding three_sorted_def part_range_cond_def by auto

lemma three_sorted_swap_imp_part_range_cond: "⟦ three_sorted xs i j k; i≠j; j≠k; l<i; l<j; l<k; i<h; j<h; k<h; h≤length xs ⟧ ⟹ part_range_cond (swap xs l j) l h"
unfolding three_sorted_def part_range_cond_def by (auto simp: swap_nth)

definition "move_pivot_to_front xs l h ≡ doN {
ASSERT (l≤h ∧ h>0);
let size = h-l;
let s2 = size div 2;

if (size > ninther_threshold) then doN {
⌦‹ASSERT (l+s2+1<h ∧ h≥3 ∧ s2≥1 ∧ s2<h );›
xs←sort_three xs l              (l + s2)       (h - 1);
xs←sort_three xs (l + 1)        (l + (s2 - 1)) (h - 2);
xs←sort_three xs (l + 2)        (l + (s2 + 1)) (h - 3);
xs←sort_three xs (l + (s2 - 1)) (l + s2)       (l + (s2 + 1));
xs ← mop_list_swap xs l (l+s2);
⌦‹ASSERT (xs!l ❙≤ xs!(l + (s2 + 1)) ∧ xs!(l + (s2 - 1)) ❙≤ xs!l);›
RETURN xs
} else doN {
⌦‹ASSERT (l+s2 ≠ h-1 ∧ l+s2<h ∧ h>0);›
sort_three xs (l+s2) l (h-1)
}
}"

lemma move_pivot_to_front_refine: "move_pivot_to_front xs l h ≤ pivot_to_front_spec xs l h"
unfolding move_pivot_to_front_def pivot_to_front_spec_def
apply (refine_vcg sort_three_sorted_rl[where l=l and h=h])
apply (all ‹elim conjE; assumption?›)
supply [[linarith_split_limit = 15]]
apply simp_all
subgoal by (auto)
subgoal by (auto)
subgoal by (auto)
subgoal by (auto)
subgoal by (metis slice_eq_mset_trans)
subgoal by (erule three_sorted_swap_imp_part_range_cond) auto
subgoal by (auto)
subgoal by (erule three_sorted_imp_part_range_cond; auto)
done

definition "shuffle_left xs i j ≡ doN {ASSERT (i≠j); mop_list_swap xs i j}"
definition "shuffle_right xs i j ≡ doN {ASSERT (i≠j); mop_list_swap xs i j}"

definition "shuffle xs l h m ≡ doN {
ASSERT (l≤h ∧ l≤m ∧ m+1≤h);
let size = h-l;
let l_size = m-l;
let r_size = h - (m+1);
let highly_unbal = l_size < size div 8 ∨ r_size < size div 8;

if highly_unbal then doN {
xs ← if l_size ≥ is_threshold then doN {  ⌦‹FIXME: This should be pdq_is_threshold!›
⌦‹          ASSERT (l + l_size div 4 < h ∧ m>0 ∧ m≥l_size div 4);
›          xs ← shuffle_left xs l (l+l_size div 4);
xs ← shuffle_left xs (m-1) (m - l_size div 4);

if l_size > ninther_threshold then doN {
⌦‹            ASSERT (
l+1≤h ∧ l_size div 4 + 1≤h ∧ l + (l_size div 4 + 1)≤h
∧ l+2≤h ∧ l_size div 4 + 2≤h ∧ l + (l_size div 4 + 2)≤h
∧ m≥2 ∧ m≥3 ∧ m≥l_size div 4 + 1 ∧ m≥l_size div 4 + 2);
›
xs ← shuffle_left xs (l + 1) (l + (l_size div 4 + 1));
xs ← shuffle_left xs (l + 2) (l + (l_size div 4 + 2));
xs ← shuffle_left xs (m - 2) (m - (l_size div 4 + 1));
xs ← shuffle_left xs (m - 3) (m - (l_size div 4 + 2));
RETURN xs
} else RETURN xs
} else RETURN xs;
xs ← if r_size ≥ is_threshold then doN {  ⌦‹FIXME: This should be pdq_is_threshold!›
⌦‹         ASSERT (m+1≤h ∧ m + 1 + r_size div 4≤h ∧ h≥1 ∧ h≥r_size div 4);
›         xs ← shuffle_right xs (m+1) (m + 1 + r_size div 4);
xs ← shuffle_right xs (h-1) (h - r_size div 4);
if r_size > ninther_threshold then doN {
⌦‹          ASSERT (m+2≤h ∧ 1 + r_size div 4≤h ∧ 2 + r_size div 4≤h ∧ 3 + r_size div 4≤h
∧ h≥2 ∧ h≥3 ∧ h≥(1 + r_size div 4) ∧ h≥(2 + r_size div 4) );
›          xs ← shuffle_right xs (m + 2) (m + (2 + r_size div 4));
xs ← shuffle_right xs (m + 3) (m + (3 + r_size div 4));
xs ← shuffle_right xs (h - 2) (h - (1 + r_size div 4));
xs ← shuffle_right xs (h - 3) (h - (2 + r_size div 4));
RETURN xs
} else RETURN xs
} else RETURN xs;
RETURN (True,xs)
} else
RETURN (False,xs)
}"

definition "shuffled l h m xs xs' ≡
l≤m ∧ m<h ∧ h≤length xs
∧ eq_outside_range xs xs' l h
∧ mset (slice l m xs) = mset (slice l m xs')
∧ xs!m = xs'!m
∧ mset (slice (m+1) h xs) = mset (slice (m+1) h xs')"

lemma eq_outside_range_swap: "{i,j}⊆{l..<h} ⟹ eq_outside_range xs (swap xs' i j) l h = eq_outside_range xs xs' l h"
by (auto simp: eq_outside_range_def)

lemma shuffled_left: "⟦ {i,j}⊆{l..<m}; shuffled l h m xs xs' ⟧ ⟹ shuffled l h m xs (swap xs' i j)"
unfolding shuffled_def
by (auto simp: eq_outside_range_swap slice_swap eq_outside_rane_lenD slice_swap_outside)

lemma shuffled_right: "⟦ {i,j}⊆{Suc m..<h}; shuffled l h m xs xs' ⟧ ⟹ shuffled l h m xs (swap xs' i j)"
unfolding shuffled_def
by (auto simp: eq_outside_range_swap slice_swap eq_outside_rane_lenD slice_swap_outside)

lemma shuffle_spec_alt: "shuffle_spec xs l h m = doN {ASSERT (l≤m ∧ m<h ∧ h≤length xs); SPEC (λ(_,xs'). shuffled l h m xs xs')}"
unfolding shuffle_spec_def shuffled_def by (auto simp: pw_eq_iff refine_pw_simps)

lemma shuffled_refl: "shuffled l h m xs xs ⟷ l≤m ∧ m<h ∧ h≤length xs"
by (auto simp: shuffled_def eq_outside_range_triv)

lemma shuffle_left_rl: "shuffled l h m xs xs' ⟹ i≠j ⟹ {i,j}⊆{l..<m} ⟹ shuffle_left xs' i j ≤ SPEC (λxs''. shuffled l h m xs xs'')"
unfolding shuffle_left_def
apply refine_vcg
by (auto simp: shuffled_def eq_outside_rane_lenD)

lemma shuffle_right_rl: "shuffled l h m xs xs' ⟹ i≠j ⟹ {i,j}⊆{Suc m..<h} ⟹ shuffle_right xs' i j ≤ SPEC (λxs''. shuffled l h m xs xs'')"
unfolding shuffle_right_def
apply refine_vcg
by (auto simp: shuffled_def eq_outside_rane_lenD)

lemma shuffle_correct: "shuffle xs l h m ≤ shuffle_spec xs l h m"
unfolding shuffle_spec_alt
apply (refine_vcg)
unfolding shuffle_def
apply (subgoal_tac "shuffled l h m xs xs")
apply refine_vcg
apply (all ‹(thin_tac "m-l < _ ∨ _")?›)

(* TODO: The splitter is probably getting in the way here! *)
subgoal
apply (refine_vcg shuffle_left_rl; assumption?)
supply [[linarith_split_limit = 25]]
apply auto 
apply (refine_vcg shuffle_right_rl; assumption?)
apply auto 
apply (refine_vcg shuffle_right_rl; assumption?)
apply (simp_all)
apply auto
done
subgoal
apply (refine_vcg shuffle_right_rl; assumption?)
apply auto
done
done

text ‹
Some definitions to hide away propositions that would overwhelm the linarith-solver of the simplifier.
›
(*
Elements in between l<..i are smaller than pivot.
* at beginning of loop, will be i-1,
* after swapping, will be i
*)
definition "AUX_SMALLER C l h xs i ≡ l<h ∧ h≤length xs ∧ l≤i ∧ i<h ∧ (∀k∈{l<..i}. C (xs!k) (xs!l))"

(*
Elements in between j..<h are not smaller than pivot

* at beginning of loop, will be j+1
* after swapping, will be j
*)
definition "AUX_NOTSM C l h xs j   ≡ l<h ∧ h≤length xs ∧ l<j ∧ j≤h ∧ (∀k∈{j..<h}. C (xs!k) (xs!l))"

definition "RIGHT_GUARD C l h xs i ≡ l<h ∧ h≤length xs ∧ (∃k∈{i<..<h}. ¬ C (xs!k) (xs!l))"

definition "LEFT_GUARD C l xs j ≡ l<length xs ∧ (∃k∈{l<..<j}. ¬ C (xs!k) (xs!l))"

lemma AUX_SMALLER_init: "⟦ l<h; h≤length xs ⟧ ⟹ AUX_SMALLER C l h xs l"
unfolding AUX_SMALLER_def by auto

lemma AUX_NOTSM_init: "⟦l<h; h≤length xs⟧ ⟹ AUX_NOTSM C l h xs h"
unfolding AUX_NOTSM_def by auto

lemma RIGHT_GUARD_from_prc: "part_range_cond xs l h ⟹ l<h ∧ h≤length xs ⟹ RIGHT_GUARD (❙<) l h xs l"
unfolding part_range_cond_def RIGHT_GUARD_def
by (auto simp: unfold_le_to_lt)

lemma LEFT_GUARD_from_prc: "part_range_cond xs l h ⟹ l<h ∧ h≤length xs ⟹ LEFT_GUARD (❙>) l xs h"
unfolding part_range_cond_def LEFT_GUARD_def
by (auto simp: unfold_le_to_lt)

lemma LEFT_GUARD_init: "⟦AUX_SMALLER (Not oo C) l h xs (i - Suc 0); l < i;  Suc l < j⇩0; i ≠ Suc l⟧ ⟹ LEFT_GUARD C l xs j⇩0"
unfolding AUX_SMALLER_def LEFT_GUARD_def
by fastforce

lemma RIGHT_GUARD_init: " ⟦AUX_NOTSM (Not ∘∘ C) l h xs (Suc j); AUX_SMALLER C l h xs i⇩0; Suc j ≠ h⟧ ⟹ RIGHT_GUARD C l h xs i⇩0"
unfolding AUX_NOTSM_def RIGHT_GUARD_def AUX_SMALLER_def
by fastforce

lemma PV_SWAP:
assumes "AUX_SMALLER C l h xs (i-1)" "AUX_NOTSM (Not oo C) l h xs (j+1)"
assumes "l<i" "i<j" "¬ C(xs!i) (xs!l)" "C (xs!j) (xs!l)"
shows "AUX_SMALLER C l h (swap xs i j) i" "AUX_NOTSM (Not oo C) l h (swap xs i j) j"
using assms
unfolding AUX_SMALLER_def AUX_NOTSM_def
by (auto simp: swap_nth)

lemma PARTITIONED_FINALLY: "¬(i<j) ⟹ ¬xs!i❙<xs!l ⟹ AUX_SMALLER (❙<) l h xs (i-1) ⟹ AUX_NOTSM (Not oo (❙<)) l h xs (j+1) ⟹ partitioned (xs!l) (swap xs l (i-Suc 0)) l h (i-Suc 0)"
unfolding partitioned_def AUX_SMALLER_def AUX_NOTSM_def
apply (auto simp: swap_nth unfold_lt_to_le)
apply (metis Suc_leI atLeastLessThan_iff connex leD le_less_linear le_neq_implies_less le_trans nat_le_Suc_less_imp)
by (metis atLeastLessThan_iff connex leD leI le_neq_implies_less le_trans nat_le_Suc_less_imp not_less_eq_eq)

lemma PARTITIONED_FINALLY2: "¬(i<j) ⟹ ¬ xs!j❙>xs!l ⟹ AUX_SMALLER (Not oo (❙>)) l h xs (i-1) ⟹ AUX_NOTSM (❙>) l h xs (j+1) ⟹ partitioned (xs!l) (swap xs l j) l h j"
unfolding partitioned_def AUX_SMALLER_def AUX_NOTSM_def
apply (simp add: unfold_lt_to_le swap_nth; safe; simp)
subgoal using connex by blast
subgoal by (meson connex dual_order.order_iff_strict greaterThanAtMost_iff leI less_le_trans nat_le_Suc_less_imp)
subgoal by (meson connex dual_order.order_iff_strict greaterThanAtMost_iff leI less_le_trans nat_le_Suc_less_imp)
done

definition "mop_C_idx C xs i j ≡ doN { ASSERT (i<length xs ∧ j<length xs); RETURN (C (xs!i) (xs!j)) }"

definition "find_next_unguarded C xs l h i⇩0 ≡ doN {
ASSERT(l<length xs ∧ l≤i⇩0 ∧ i⇩0<h ∧ h≤length xs ∧ (∃si∈{i⇩0<..<h}. ¬ C (xs!si) (xs!l)) );
monadic_WHILEIT (λi. i⇩0<i ∧ i<h ∧ (∀j∈{i⇩0<..<i}. C (xs!j) (xs!l)))
(λi. doN { ASSERT (i≠l); mop_C_idx C xs i l } )
(λi. doN { ASSERT (i<h); RETURN (i+1)})
(i⇩0 + 1)
}"

definition "find_next_guarded C xs l h i⇩0 ≡ doN {
ASSERT(l<length xs ∧ l≤i⇩0 ∧ i⇩0<h ∧ h≤length xs );
monadic_WHILEIT (λi. i⇩0<i ∧ i<h ∧ (∀j∈{i⇩0<..<i}. C (xs!j) (xs!l)))
(λi. if i < h - 1 then doN { ASSERT (i≠l); mop_C_idx C xs i l } else RETURN False)
(λi. doN { ASSERT (i<h); RETURN (i+1)})
(i⇩0 + 1)
}"

definition "first_find_next C xs l j h i⇩0 ≡ doN {
ASSERT (j<h);
if j+1=h then find_next_guarded C xs l h i⇩0
else find_next_unguarded C xs l h i⇩0
}"

definition "find_prev_unguarded C xs l j⇩0 ≡ doN {
ASSERT(l<length xs ∧ l+1<j⇩0 ∧ j⇩0≤length xs ∧ (∃si∈{l<..<j⇩0}. ¬C (xs!si) (xs!l)) ∧ j⇩0≥1 );
monadic_WHILEIT (λj. l<j ∧ j<j⇩0 ∧ (∀k∈{j<..<j⇩0}. C (xs!k) (xs!l)))
(λj. mop_C_idx C xs j l)
(λj. doN {ASSERT(j≥1); RETURN (j-1)})
(j⇩0 - 1)
}"

definition "find_prev_guarded C xs l j⇩0 ≡ doN {
ASSERT(l<length xs ∧ l+1<j⇩0 ∧ j⇩0≤length xs ∧ j⇩0≥1 );
monadic_WHILEIT (λj. l<j ∧ j<j⇩0 ∧ (∀k∈{j<..<j⇩0}. C (xs!k) (xs!l)))
(λj. if l+1<j then mop_C_idx C xs j l else RETURN False )
(λj. doN {ASSERT(j≥1); RETURN (j-1)})
(j⇩0 - 1)
}"

definition "first_find_prev C xs l i h ≡ doN {
ASSERT (l<h);
if i=l+1 then find_prev_guarded C xs l h
else find_prev_unguarded C xs l h
}"

lemma find_next_unguarded_rl: "⟦ AUX_SMALLER C l h xs i⇩0; RIGHT_GUARD C l h xs i⇩0 ⟧
⟹ find_next_unguarded C xs l h i⇩0 ≤ SPEC (λi. i⇩0<i ∧ i<h ∧ AUX_SMALLER C l h xs (i-1) ∧ ¬C (xs!i) (xs!l) )"
unfolding find_next_unguarded_def AUX_SMALLER_def RIGHT_GUARD_def mop_C_idx_def
apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. length xs - i)"])
apply clarsimp_all
subgoal
apply safe
apply simp_all
subgoal by (metis Suc_lessI greaterThanLessThan_iff less_antisym)
subgoal by (metis greaterThanLessThan_iff less_SucE)
subgoal by auto
done
done

lemma find_next_guarded_rl: "⟦ AUX_SMALLER C l h xs i⇩0; i⇩0+1<h ⟧
⟹ find_next_guarded C xs l h i⇩0 ≤ SPEC (λi. i⇩0<i ∧ i<h ∧ AUX_SMALLER C l h xs (i-1) ∧ ( i=h-1 ∨ ¬C (xs!i) (xs!l) ) )"
unfolding find_next_guarded_def AUX_SMALLER_def RIGHT_GUARD_def mop_C_idx_def
apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. length xs - i)"])
apply clarsimp_all
subgoal by (fastforce elim: less_SucE)
subgoal by auto
done

lemma first_find_next_rl: "⟦ AUX_NOTSM (Not oo C) l h xs (j+1); i⇩0+1<h; AUX_SMALLER C l h xs i⇩0; i⇩0+1 < h ⟧ ⟹
first_find_next C xs l j h i⇩0 ≤ SPEC (λi. i⇩0<i ∧ i<h ∧ AUX_SMALLER C l h xs (i-1) ∧ ( i=h-1 ∨ ¬C (xs!i) (xs!l) ))"
unfolding first_find_next_def
apply (refine_vcg find_next_guarded_rl find_next_unguarded_rl)
apply (auto simp: RIGHT_GUARD_init)
apply (auto simp: AUX_NOTSM_def)
done

lemma find_prev_unguarded_rl: "⟦ AUX_NOTSM C l h xs j⇩0; LEFT_GUARD C l xs j⇩0 ⟧ ⟹
find_prev_unguarded C xs l j⇩0 ≤ SPEC (λj. l<j ∧ j<j⇩0 ∧ AUX_NOTSM C l h xs (j+1) ∧ ¬C (xs!j) (xs!l))"
unfolding find_prev_unguarded_def AUX_NOTSM_def LEFT_GUARD_def mop_C_idx_def
apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. i)"])
apply simp_all
apply auto []
apply auto []
apply auto []
subgoal
apply safe
apply simp_all
subgoal by (metis (full_types) greaterThanLessThan_iff leD le_less_linear le_neq_implies_less nat_le_Suc_less_imp)
subgoal by (metis greaterThanLessThan_iff leD linorder_neqE_nat nat_le_Suc_less_imp)
subgoal by auto
done
done

lemma find_prev_guarded_rl: "⟦ AUX_NOTSM C l h xs j⇩0; l+1 < j⇩0 ⟧ ⟹
find_prev_guarded C xs l j⇩0 ≤ SPEC (λj. l<j ∧ j<j⇩0 ∧ AUX_NOTSM C l h xs (j+1) ∧ (j = l+1 ∨ ¬C (xs!j) (xs!l)))"
unfolding find_prev_guarded_def AUX_NOTSM_def LEFT_GUARD_def mop_C_idx_def
apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λi. i)"])
apply simp_all
apply auto []
apply auto []
apply (metis Suc_le_lessD atLeastLessThan_iff atLeastSucLessThan_greaterThanLessThan
greaterThanLessThan_iff leD le_less_linear less_imp_diff_less nat_le_Suc_less_imp nat_neq_iff)
apply auto []
done

lemma first_find_prev_rl: "⟦ AUX_SMALLER (Not oo C) l h xs (i-1); l<i; AUX_NOTSM C l h xs j⇩0; l+1 < j⇩0 ⟧ ⟹
first_find_prev C xs l i j⇩0 ≤ SPEC (λj. l<j ∧ j<j⇩0 ∧ AUX_NOTSM C l h xs (j+1) ∧ (j = l+1 ∨ ¬C (xs!j) (xs!l)))"
unfolding first_find_prev_def
apply (refine_vcg find_prev_guarded_rl find_prev_unguarded_rl; assumption?)
apply (auto simp: LEFT_GUARD_init)
done

definition "part_right_invar xs⇩0 l h ≡ λ(xs,i,j).
slice_eq_mset l h xs⇩0 xs
∧ xs⇩0!l = xs!l
∧ l < h ∧ h≤length xs
∧ {i,j} ⊆ {l<..<h}
∧ AUX_SMALLER (❙<) l h xs (i-1)
∧ AUX_NOTSM (Not oo (❙<)) l h xs (j+1)
∧ ¬ xs!i ❙< xs!l ∧ (i<j ⟶ xs!j ❙< xs!l)
"

lemma part_right_invar_boundsD:
assumes "part_right_invar xs⇩0 l h (xs,i,j)"
shows "i<length xs" "j<length xs" "length xs⇩0 = length xs" "i - Suc 0 < length xs" "l ≤ i-Suc 0" "i-Suc 0 < h" "xs⇩0!l = xs!l"
using assms unfolding part_right_invar_def AUX_SMALLER_def AUX_NOTSM_def
apply (auto simp: slice_eq_mset_eq_length)
done

lemma part_right_invar_pres:
assumes "part_right_invar xs⇩0 l h (xs,i,j)" "i<j"
shows "AUX_SMALLER (❙<) l h (swap xs i j) i"
and "RIGHT_GUARD (❙<) l h (swap xs i j) i"
and "AUX_NOTSM (Not oo (❙<)) l h (swap xs i j) j"
and "LEFT_GUARD (Not oo (❙<)) l (swap xs i j) j"
using assms unfolding part_right_invar_def
apply -
subgoal by (auto simp: PV_SWAP)
subgoal unfolding RIGHT_GUARD_def by (auto simp: swap_nth)
subgoal by (auto simp: PV_SWAP)
subgoal unfolding LEFT_GUARD_def by (auto simp: swap_nth)
done

lemma mop_list_safe_swap: "mop_list_swap xs i j = doN { ASSERT (i<length xs ∧ j<length xs); if i≠j then mop_list_swap xs i j else RETURN xs }"
by (auto simp: pw_eq_iff refine_pw_simps)

definition "partition_right xs l h ≡ doN {
ASSERT (l<h ∧ h≤length xs);

i ← find_next_unguarded (❙<) xs l h l;

j ← first_find_prev (Not oo (❙<)) xs l i h;

let alrp = i≥j;

(xs,i,j)←
WHILEIT
(part_right_invar xs l h)
(λ(xs,i,j). i<j)
(λ(xs,i,j). doN {
ASSERT (i≠j);
xs←mop_list_swap xs i j;
i←find_next_unguarded (❙<) xs l h i;
j←find_prev_unguarded (Not oo (❙<)) xs l j;
RETURN (xs,i,j)
})
(xs,i,j);

ASSERT (i≥1);
xs ← mop_list_swap xs l (i-1);

ASSERT (∀k∈{l..<i-1}. xs!k❙<xs!(i-1)); ― ‹Not required by high-level spec, but to ensure that left side contains only truly smaller elements›

RETURN (alrp,i-1,xs)
}"

lemma bincond_double_neg[simp]: "Not oo (Not oo C) = C" by (intro ext) auto

lemma partition_right_correct: "partition_right xs l h ≤ partition_spec xs l h"
unfolding partition_right_def partition_spec_def
apply (refine_vcg find_next_unguarded_rl first_find_prev_rl[where h=h] find_prev_unguarded_rl[where h=h]  WHILEIT_rule[where R="measure (λ(xs,i,j). j)"])
apply (all ‹(elim conjE)?, assumption?›)

apply (clarsimp_all simp: AUX_SMALLER_init AUX_NOTSM_init RIGHT_GUARD_from_prc part_right_invar_boundsD part_right_invar_pres)
subgoal unfolding part_right_invar_def by auto
subgoal unfolding part_right_invar_def by auto
subgoal unfolding part_right_invar_def by auto
subgoal unfolding part_right_invar_def AUX_SMALLER_def by (auto simp: swap_nth)
subgoal unfolding part_right_invar_def AUX_SMALLER_def by auto
subgoal
apply (erule PARTITIONED_FINALLY)
unfolding part_right_invar_def
by clarsimp_all
done

definition "part_left_invar xs⇩0 l h ≡ λ(xs,i,j).
slice_eq_mset l h xs⇩0 xs
∧ xs⇩0!l = xs!l
∧ l < h ∧ h≤length xs
∧ {i,j} ⊆ {l<..<h}
∧ AUX_SMALLER (Not oo (❙>)) l h xs (i-1)
∧ AUX_NOTSM (❙>) l h xs (j+1)
∧ ¬ xs!j ❙> xs!l ∧ (i<j ⟶ xs!i ❙> xs!l)
"

lemma part_left_invar_boundsD:
assumes "part_left_invar xs⇩0 l h (xs,i,j)"
shows "i<length xs" "j<length xs" "length xs⇩0 = length xs" "i - Suc 0 < length xs" "l ≤ i-Suc 0" "i-Suc 0 < h" "xs⇩0!l = xs!l" "l≤j" "j<h"
using assms unfolding part_left_invar_def AUX_SMALLER_def AUX_NOTSM_def
apply (auto simp: slice_eq_mset_eq_length)
done

lemma part_left_invar_pres:
assumes "part_left_invar xs⇩0 l h (xs,i,j)" "i<j"
shows "AUX_SMALLER (Not oo (❙>)) l h (swap xs i j) i"
and "RIGHT_GUARD (Not oo (❙>)) l h (swap xs i j) i"
and "AUX_NOTSM (❙>) l h (swap xs i j) j"
and "LEFT_GUARD (❙>) l (swap xs i j) j"
using assms unfolding part_left_invar_def
apply -
subgoal by (auto simp: PV_SWAP)
subgoal unfolding RIGHT_GUARD_def by (auto simp: swap_nth)
subgoal using PV_SWAP by fastforce
subgoal unfolding LEFT_GUARD_def by (auto simp: swap_nth)
done

definition "partition_left xs l h ≡ doN {
ASSERT (l<h ∧ h≤length xs);

j ← find_prev_unguarded (❙>) xs l h;

i ← first_find_next (Not oo (❙>)) xs l j h l;

(xs,i,j)←
WHILEIT
(part_left_invar xs l h)
(λ(xs,i,j). i<j)
(λ(xs,i,j). doN {
ASSERT (i≠j);
xs←mop_list_swap xs i j;
j←find_prev_unguarded (❙>) xs l j;
i←find_next_unguarded (Not oo (❙>)) xs l h i;
RETURN (xs,i,j)
})
(xs,i,j);

ASSERT (l≠j);
xs ← mop_list_swap xs l j;

ASSERT (∀k∈{j<..<h}. xs!k❙>xs!j); ― ‹Not required by high-level spec, but to ensure that right side contains only truly greater elements›

RETURN (False,j,xs)
}"

lemma partition_left_correct: "partition_left xs l h ≤ partition_left_spec xs l h"
unfolding partition_left_def partition_spec_def partition_left_spec_def
apply (refine_vcg find_next_unguarded_rl first_find_next_rl[where h=h] find_prev_unguarded_rl[where h=h]  WHILEIT_rule[where R="measure (λ(xs,i,j). j)"])
apply (all ‹(elim conjE)?, assumption?›)
apply (clarsimp_all simp: AUX_SMALLER_init AUX_NOTSM_init LEFT_GUARD_from_prc part_left_invar_boundsD part_left_invar_pres)
subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto
subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto
subgoal unfolding part_left_invar_def AUX_NOTSM_def by (auto simp: swap_nth)
subgoal unfolding part_left_invar_def AUX_NOTSM_def by auto
subgoal unfolding part_left_invar_def by auto
subgoal
apply (erule PARTITIONED_FINALLY2)
unfolding part_left_invar_def
by clarsimp_all
done

text ‹We use the guarded arithmetic operations on natural numbers, to avoid to many
in-bounds conditions to be visible to the simplifier ... this would make the simplifier
extremely slow when invoked from within Sepref in the next step.
›

definition "shuffle2 xs l h m ≡ doN {
size ← mop_nat_sub h l;
l_size ← mop_nat_sub m l;
t_m1 ← mop_nat_add_bnd h m 1;
r_size ← mop_nat_sub h t_m1;
t_sd8 ← mop_nat_div size 8;

let highly_unbal = l_size < t_sd8 ∨ r_size < t_sd8;

if highly_unbal then doN {
xs ← if l_size ≥ is_threshold then doN {
t_lsd4 ← mop_nat_div l_size 4;
i_lls4 ← mop_nat_add_bnd h l t_lsd4; ⌦‹l + l_size div 4›
i_mm1 ← mop_nat_sub m 1; ⌦‹m-1›
i_mmls4 ← mop_nat_sub m t_lsd4; ⌦‹m - l_size div 4›

xs ← shuffle_left xs l i_lls4;
xs ← shuffle_left xs i_mm1 i_mmls4;

if l_size > ninther_threshold then doN {
i_l1 ← mop_nat_add_bnd h l 1;
i_l2 ← mop_nat_add_bnd h l 2;
i_mm2 ← mop_nat_sub m 2;
i_mm3 ← mop_nat_sub m 3;

i_lls41 ← mop_nat_add_bnd h i_lls4 1;
i_lls42 ← mop_nat_add_bnd h i_lls4 2;
i_mmls41 ← mop_nat_sub i_mmls4 1;
i_mmls42 ← mop_nat_sub i_mmls4 2;

xs ← shuffle_left xs i_l1 i_lls41;
xs ← shuffle_left xs i_l2 i_lls42;
xs ← shuffle_left xs i_mm2 i_mmls41;
xs ← shuffle_left xs i_mm3 i_mmls42;
RETURN xs
} else RETURN xs
} else RETURN xs;
xs ← if r_size ≥ is_threshold then doN {
i_m1 ← mop_nat_add_bnd h m 1;
i_h1 ← mop_nat_sub h 1;

t_rsd4 ← mop_nat_div r_size 4;
i_mp1 ← mop_nat_add_bnd h i_m1 t_rsd4;
i_hm ← mop_nat_sub h t_rsd4;

xs ← shuffle_right xs i_m1 i_mp1;
xs ← shuffle_right xs i_h1 i_hm;
if r_size > ninther_threshold then doN {

i_m2 ← mop_nat_add_bnd h m 2;
i_m3 ← mop_nat_add_bnd h m 3;
i_h2 ← mop_nat_sub h 2;
i_h3 ← mop_nat_sub h 3;
i_hm1 ← mop_nat_sub i_hm 1;
i_hm2 ← mop_nat_sub i_hm 2;
i_mp2 ← mop_nat_add_bnd h i_mp1 1;
i_mp3 ← mop_nat_add_bnd h i_mp1 2;

xs ← shuffle_right xs i_m2 i_mp2;
xs ← shuffle_right xs i_m3 i_mp3;
xs ← shuffle_right xs i_h2 i_hm1;
xs ← shuffle_right xs i_h3 i_hm2;
RETURN xs
} else RETURN xs
} else RETURN xs;
RETURN (True,xs)
} else
RETURN (False,xs)
}"

lemma shuffle2_aux: "⟦ ninther_threshold < m - l; l ≤ h; l ≤ m; m + 1 ≤ h⟧  ⟹ l + (m - l) div 4 + 1 ≤ h"
apply simp
done

lemma mop_nat_simps:
"a+b≤h ⟹ mop_nat_add_bnd h a b = RETURN (a+b)"
"b≤a ⟹ mop_nat_sub a b = RETURN (a-b)"
"b≠0 ⟹ mop_nat_div a b = RETURN (a div b)"

lemma shuffle2_refine: "shuffle2 xs l h m ≤ shuffle xs l h m"
proof -

have A:
"(shuffle_right,shuffle_right)∈Id → nat_rel → nat_rel → ⟨Id⟩nres_rel"
"(shuffle_left,shuffle_left)∈Id → nat_rel → nat_rel → ⟨Id⟩nres_rel"
by (auto intro!: nres_relI)
note A = A[param_fo]

{
assume "l≤h" "l≤m" "m+1≤h"
then have ?thesis
unfolding shuffle2_def
apply (simp split del: if_split add: Let_def mop_nat_simps cong: if_cong)
unfolding shuffle_def Let_def
apply (simp named_ss Main_ss: split del: if_split cong: if_cong)
apply (split if_split; intro conjI impI; simp only: if_True if_False)
apply (split if_split; intro conjI impI; simp only: if_True if_False)
apply (all ‹(cases "ninther_threshold < m - l"; simp only: if_True if_False)?›)
apply (all ‹(cases "is_threshold ≤ h - Suc m"; simp only: if_True if_False)?›)
apply (all ‹(cases "ninther_threshold < h - Suc m"; simp only: if_True if_False)?›)
apply (rule refine_IdD)
apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
apply (rule refine_IdD)
apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
apply (rule refine_IdD)
apply (refine_rcg A[THEN nres_relD]; (rule IdI)?; simp)
done
} thus ?thesis
unfolding shuffle_def by (simp only: pw_le_iff refine_pw_simps) blast
qed

text ‹Again, we replace the nat arithmetic by assertion-guarded operations, to avoid
overwhelming the simplifier.›
definition "move_pivot_to_front2 xs l h ≡ doN {
ASSERT (l≤h ∧ h>0);

size ← mop_nat_sub h l;
s2 ← mop_nat_div size 2;

if (size > ninther_threshold) then doN {
⌦‹ASSERT (l+s2+1<h ∧ h≥3 ∧ s2≥1 ∧ s2<h );›
ASSERT (l+2≤h ∧ l+s2+1≤h ∧ l+s2≥1 ∧ h≥3 );
xs←sort_three xs l              (l + s2)      (h - 1);
xs←sort_three xs (l + 1)        (l + s2 - 1) (h - 2);
xs←sort_three xs (l + 2)        (l + s2 + 1) (h - 3);
xs←sort_three xs (l + s2 - 1) (l + s2)       (l + s2 + 1);
ASSERT (l≠l+s2);
xs ← mop_list_swap xs l (l+s2);
⌦‹ASSERT (xs!l ❙≤ xs!(l + (s2 + 1)) ∧ xs!(l + (s2 - 1)) ❙≤ xs!l);›
RETURN xs
} else doN {
ASSERT (l+s2≤h ∧ h≥1);
sort_three xs (l+s2) l (h-1)
}
}"

lemma move_pivot_to_front2_refine: "move_pivot_to_front2 xs l h ≤ move_pivot_to_front xs l h"
unfolding move_pivot_to_front2_def move_pivot_to_front_def Let_def mop_nat_defs
apply (simp split del: if_split)
apply (rule refine_IdD)
apply refine_rcg
apply refine_dref_type
apply simp_all
done

text ‹We explicitly introduce evaluation order of conditions that must be short-circuited.›
definition "pdqsort_aux2 leftmost xs l h (d::nat) ≡ RECT (λpdqsort_aux (leftmost,xs,l,h,d). doN {
ASSERT (l≤h);

if (h-l < pdq_is_threshold) then
pdq_guarded_sort_spec leftmost xs l h
else doN {
xs ← pivot_to_front_spec xs l h;

ASSERT (¬leftmost ⟶ l>0);
if⇩N (if leftmost then RETURN False else doN { ASSERT (l≥1); b←mop_cmp_idxs xs (l-1) l; RETURN (¬b) } ) then doN {
(_,m,xs) ← partition_left_spec xs l h;
ASSERT (m<h);
pdqsort_aux (False,xs,m+1,h,d)
} else doN {
(alrp,m,xs) ← partition_spec xs l h;
(unbal,xs) ← shuffle_spec xs l h m;

ASSERT (0<d);
let d = (if unbal then d-1 else d);

(didsort,xs) ←
if d=0 then doN {xs ← fallback_sort_spec xs l h; RETURN (True,xs)}
else if alrp ∧ ¬unbal then doN {
(r,xs) ← maybe_sort_spec xs l m;
if r then doN {
ASSERT (m<h);
maybe_sort_spec xs (m+1) h
} else RETURN (False,xs)
} else RETURN (False,xs);

if didsort then RETURN xs
else doN { ⌦‹TODO: Test optimization of not sorting left partition again, if maybe_sort sorted it›
xs ← pdqsort_aux (leftmost,xs,l,m,d);
ASSERT (m<h);
xs ← pdqsort_aux (False,xs,m+1,h,d);
RETURN xs
}
}
}

}) (leftmost,xs,l,h,d)"

(* TODO: Move. TODO: really refine2? *)
lemma ifN_refine[refine2]:
assumes "b≤RETURN b'" "c≤⇓R c'" "d≤⇓R d'"
shows "(if⇩N b then c else d) ≤⇓R (if b' then c' else d')"
using assms if_bind_cond_refine by blast

lemma pdqsort_aux2_refine: "pdqsort_aux2 leftmost xs l h d ≤ pdqsort_aux leftmost xs l h d"
unfolding pdqsort_aux2_def pdqsort_aux_def
apply (rule refine_IdD if_bind_cond_refine)
apply refine_rcg
apply refine_dref_type
apply (all ‹(simp named_ss HOL_ss: prod_rel_simp pair_in_Id_conv)?›)
apply (all ‹(elim conjE)?›)
apply simp_all
by auto

end

subsection ‹Refinement to Isabelle-LLVM›

text ‹Some boilerplate code for every subroutine.›

context sort_impl_context begin

sepref_register
left_find_prev_ug: "find_prev_unguarded (❙>)"
left_find_next_ug: "find_next_unguarded (Not oo (❙>))"
left_find_next_g: "find_next_guarded (Not oo (❙>))"
left_first_find_next: "first_find_next (Not oo (❙>))"

lemma mop_C_idx_unfolds:
"mop_C_idx (❙>) xs i j = mop_cmp_idxs xs j i"
"mop_C_idx (Not oo (❙>)) xs i j = doN { b←mop_cmp_idxs xs j i; RETURN (¬b) }"
"mop_C_idx (❙<) xs i j = mop_cmp_idxs xs i j"
"mop_C_idx (Not oo (❙<)) xs i j = doN { b←mop_cmp_idxs xs i j; RETURN (¬b) }"
unfolding mop_C_idx_def
by (auto simp: pw_eq_iff refine_pw_simps)

sepref_def left_find_prev_ug_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_unguarded (❙>)))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_prev_unguarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def left_find_next_ug_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_unguarded (Not oo (❙>))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_next_unguarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def left_find_next_g_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_guarded (Not oo (❙>))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_next_guarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def left_first_find_next_impl [llvm_inline] is "uncurry4 (PR_CONST (first_find_next (Not oo (❙>))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding first_find_next_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def partition_left_impl is "uncurry2 (PR_CONST partition_left)" :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn ×⇩a size_assn ×⇩a arr_assn"
unfolding partition_left_def PR_CONST_def
by sepref

thm partition_right_def

sepref_register
right_find_prev_ug: "find_prev_unguarded (Not oo (❙<))"
right_find_next_ug: "find_next_unguarded (❙<)"
right_find_next_g: "find_prev_guarded (Not oo (❙<))"
right_first_find_next: "first_find_prev (Not oo (❙<))"

sepref_def right_find_prev_ug_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_unguarded (Not oo (❙<))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_prev_unguarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def right_find_next_ug_impl [llvm_inline] is "uncurry3 (PR_CONST (find_next_unguarded (❙<)))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_next_unguarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def right_find_prev_g_impl [llvm_inline] is "uncurry2 (PR_CONST (find_prev_guarded (Not oo (❙<))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding find_prev_guarded_def mop_C_idx_unfolds PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def right_first_find_prev_impl [llvm_inline] is "uncurry3 (PR_CONST (first_find_prev (Not oo (❙<))))" :: "arr_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding first_find_prev_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_def partition_right_impl [llvm_inline] is "uncurry2 (PR_CONST partition_right)" :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn ×⇩a size_assn ×⇩a arr_assn"
unfolding partition_right_def PR_CONST_def
apply (rewrite at "mop_list_swap _ _ (_-1)" mop_list_safe_swap)
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_register shuffle2

sepref_def shuffle_impl [llvm_inline] is "uncurry3 shuffle2"   :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn ×⇩a arr_assn"
unfolding shuffle2_def PR_CONST_def shuffle_left_def shuffle_right_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_register sort_three

sepref_def sort_three_impl [llvm_inline] is "uncurry3 (PR_CONST sort_three)"   :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a arr_assn"
unfolding sort_three_def sort_two_def PR_CONST_def
by sepref

sepref_def move_pivot_to_front_impl [llvm_inline] is "uncurry2 (PR_CONST move_pivot_to_front2)" :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a arr_assn"
unfolding move_pivot_to_front2_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

sepref_register pivot_to_front_spec partition_left_spec partition_spec shuffle_spec fallback_sort_spec

lemma move_pivot_to_front2_refine': "(PR_CONST move_pivot_to_front2, PR_CONST pivot_to_front_spec)∈Id→Id→Id→⟨Id⟩nres_rel"
proof -
note move_pivot_to_front2_refine also note move_pivot_to_front_refine
finally show ?thesis by (auto intro!: nres_relI)
qed

lemma partition_left_refine': "(PR_CONST partition_left, PR_CONST partition_left_spec) ∈ Id→Id→Id→⟨Id⟩nres_rel"
using partition_left_correct by (auto intro!: nres_relI)

lemma partition_right_refine': "(PR_CONST partition_right, PR_CONST partition_spec) ∈ Id→Id→Id→⟨Id⟩nres_rel"
using partition_right_correct by (auto intro!: nres_relI)

lemma shuffle_refine': "(shuffle2, shuffle_spec) ∈ Id→Id→Id→Id→⟨Id⟩nres_rel"
proof -
note shuffle2_refine also note shuffle_correct
finally show ?thesis by (auto intro!: nres_relI)
qed

lemma heapsort_refine_fbs': "(PR_CONST heapsort,PR_CONST fallback_sort_spec) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
unfolding fallback_sort_spec_def PR_CONST_def
using heapsort_correct'[OF IdI IdI IdI] by (auto intro!: nres_relI)

lemmas [sepref_fr_rules] =
move_pivot_to_front_impl.refine[FCOMP move_pivot_to_front2_refine']
partition_left_impl.refine[FCOMP partition_left_refine']
partition_right_impl.refine[FCOMP partition_right_refine']
shuffle_impl.refine[FCOMP shuffle_refine']
heapsort_hnr[FCOMP heapsort_refine_fbs']

sepref_register pdqsort_aux
sepref_def pdqsort_aux_impl [llvm_inline] is "uncurry4 (PR_CONST pdqsort_aux2)" :: "bool1_assn⇧k *⇩a arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a arr_assn"
unfolding pdqsort_aux2_def PR_CONST_def
supply [[goals_limit = 1]]
apply (annot_snat_const "TYPE(size_t)")
by sepref

lemma pdqsort_aux2_refine': "(PR_CONST pdqsort_aux2, PR_CONST pdqsort_aux) ∈ Id → Id → Id → Id → Id → ⟨Id⟩nres_rel"
using pdqsort_aux2_refine by (auto intro: nres_relI)

lemmas [sepref_fr_rules] = pdqsort_aux_impl.refine[FCOMP pdqsort_aux2_refine']

sepref_register pdqsort
sepref_def pdqsort_impl is "uncurry2 (PR_CONST pdqsort)" :: "arr_assn⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a arr_assn"
unfolding pdqsort_def PR_CONST_def
apply (annot_snat_const "TYPE(size_t)")
by sepref

end

end
```