Theory Sorting_Guarded_Partition

theory Sorting_Guarded_Partition
imports Sorting_Quicksort_Scheme
begin

(* TODO: Move *)
lemma slice_update_outside[simp]: "i∉{l..<h} ⟹ slice l h (xs[i:=x]) = slice l h xs"
  unfolding Misc.slice_def
  apply auto
  by (metis drop_take leI take_update_cancel)

lemma slice_eq_mset_upd_outside: "slice_eq_mset l h xs xs' ⟹ i∉{l..<h} ⟹ i<length xs' ⟹ slice_eq_mset l h (xs[i:=x]) (xs'[i:=x])"
  unfolding slice_eq_mset_def
  apply (auto simp: drop_update_swap not_le)
  by (metis drop_update_cancel drop_update_swap leI)



  
hide_const (open) Transcendental.pi ― ‹‹pi› is the implementation of ‹p›, not some constant related to a circle ;)›

(* TODO: Move. Found useful for ATPs *)
lemma strict_itrans: "a < c ⟹ a < b ∨ b < c" for a b c :: "_::linorder"
  by auto

(* Guarded partitioning scheme, using sentinels. *)  
  
  

context weak_ordering begin  
  
subsection ‹Hoare Partitioning Scheme›  


definition "ungrd_qsg_next_l_spec si xs p li ≡ 
  doN {
    ASSERT (li ≤ si ∧ si<length xs ∧ xs!si ≥ p);
    SPEC (λli'. li≤li' ∧ li' ≤ si ∧ (∀i∈{li..<li'}. xs!i<p) ∧ xs!li'≥p)
  }"

definition "ungrd_qsg_next_h_spec si xs p hi ≡ 
  doN {
    ASSERT (si < hi ∧ hi≤length xs ∧ xs!si ≤ p);
    SPEC (λhi'. si≤hi' ∧ hi'<hi ∧ (∀i∈{hi'<..<hi}. xs!i>p) ∧ xs!hi'≤p)
  }"
  
  
definition qsg_next_l :: "nat ⇒ 'a list ⇒ 'a ⇒ nat ⇒ nat nres" where            
  "qsg_next_l si xs p li ≡ doN {
    monadic_WHILEIT (λli'. li≤li' ∧ (∀i∈{li..<li'}. xs!i<p) ∧ li'≤ si) 
      (λli. doN { mop_cmp_idx_v xs li p}) (λli. do { ASSERT (li < si); RETURN (li + 1) }) li
  }"  

  
lemma qsg_next_l_refine: "(qsg_next_l,PR_CONST ungrd_qsg_next_l_spec)∈Id→Id→Id→Id→⟨Id⟩nres_rel"
  unfolding qsg_next_l_def ungrd_qsg_next_l_spec_def PR_CONST_def
  apply (intro fun_relI; clarsimp)
  subgoal for si xs p li
    apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λli. si - li)"] split_ifI)
    apply clarsimp_all
    subgoal by (metis le_eq_less_or_eq wo_leD)
    subgoal by (metis atLeastLessThan_iff less_Suc_eq)
    subgoal by (metis diff_less_mono2 lessI)
    subgoal using wo_not_le_imp_less by blast
    done
  done


definition qsg_next_h :: "nat ⇒ 'a list ⇒ 'a ⇒ nat ⇒ nat nres" where
  "qsg_next_h si xs p hi ≡ doN {
    ASSERT (hi>0);
    let hi = hi - 1;
    monadic_WHILEIT (λhi'. si≤hi' ∧ hi'≤hi ∧ (∀i∈{hi'<..hi}. xs!i>p))
      (λhi. doN { mop_cmp_v_idx xs p hi}) (λhi. doN { ASSERT(hi>0); RETURN (hi - 1)}) hi
  }"  

  
lemma qsg_next_h_refine: "(qsg_next_h,PR_CONST (ungrd_qsg_next_h_spec)) ∈ Id → Id → Id → Id → ⟨Id⟩nres_rel"
  unfolding qsg_next_h_def ungrd_qsg_next_h_spec_def PR_CONST_def
  apply (refine_vcg monadic_WHILEIT_rule[where R="measure id"] split_ifI)
  apply (all ‹(determ ‹elim conjE exE›)?›)
  apply simp_all
  subgoal by (metis bot_nat_0.extremum_uniqueI gr0I wo_leD)
  subgoal by (metis One_nat_def le_step_down_nat wo_leD)
  subgoal by (metis Suc_le_eq Suc_pred greaterThanAtMost_iff less_Suc_eq less_Suc_eq_le)
  subgoal by (simp add: greaterThanAtMost_upt)
  subgoal using unfold_le_to_lt by presburger
  done
  

definition "ungrd_qsg_next_lh_spec si0 siN xs p li hi ≡ doN {
  li ← ungrd_qsg_next_l_spec siN xs p li;
  hi ← ungrd_qsg_next_h_spec si0 xs p hi;
  RETURN (li,hi)
}"  

(* Situation at start, and after swaps *)
definition "qsg_part_assn1 li0 hi0 p xs0 li hi xs ≡
    0 < li0 ∧ li0≤hi0 ∧ hi0<length xs0 ∧ xs0!(li0-1) ≤ p ∧ p ≤ xs0!hi0
  ∧ slice_eq_mset li0 hi0 xs xs0
  ∧ li0≤li ∧ li≤hi ∧ hi≤hi0
  ∧ (∀i∈{li0..<li}. xs!i ≤ p) 
  ∧ (∀i∈{hi..<hi0}. p ≤ xs!i) 
"

definition "qsg_part_assn2 li0 hi0 p xs0 li hi xs ≡
    0 < li0 ∧ li0≤hi0 ∧ hi0<length xs0 ∧ xs0!(li0-1) ≤ p ∧ p ≤ xs0!hi0
  ∧ slice_eq_mset li0 hi0 xs xs0
  ∧ li0≤li ∧ li≤hi+1 ∧ hi<hi0 ∧ li≤hi0
  ∧ (∀i∈{li0..<li}. xs!i ≤ p) 
  ∧ (∀i∈{hi<..<hi0}. p ≤ xs!i) 
  ∧ xs!li ≥ p
  ∧ xs!hi ≤ p  
"

lemma qsg_part_12_aux:
  assumes SENTINELS: "xs ! (li0 - Suc 0) ≤ p" "p ≤ xs ! hi0"
  assumes LI_LE_HI: "li ≤ hi"
  assumes LI'_BOUND: "li ≤ li'" "li' ≤ hi0"
  assumes HI'_BOUND: "li0 - Suc 0 ≤ hi'" "hi' < hi" 
  assumes 
  UPTO_LI: "∀i∈{li0..<li}. xs ! i ≤ p" and
  LI_TO_LI': "∀i∈{li..<li'}. xs ! i < p" and
  DOWNTO_HI: "∀i∈{hi..<hi0}. p ≤ xs ! i" and
  HI'_TO_HI: "∀i∈{hi'<..<hi}. p < xs ! i"
  shows "li' ≤ Suc hi'" "(∀i∈{li0..<li'}. xs ! i ≤ p)" "(∀i∈{hi'<..<hi0}. p ≤ xs ! i)"
proof -

  show G1: "(∀i∈{li0..<li'}. xs ! i ≤ p)" using UPTO_LI LI_TO_LI' by (auto simp: unfold_lt_to_le)
  
  show G2: "(∀i∈{hi'<..<hi0}. p ≤ xs ! i)" using HI'_TO_HI DOWNTO_HI by (auto simp: unfold_lt_to_le)
  
  consider "li<li'" | "hi' < hi-1" | "li'=li" "hi'=hi-1"
    using ‹hi' < hi› ‹li ≤ li'› by linarith
  then show "li' ≤ Suc hi'" proof cases
    case 1
    hence "xs!(li'-1) < p" using LI_TO_LI' by simp
    moreover have "∀i∈{hi'<..hi0}. p ≤ xs!i" using ‹p ≤ xs ! hi0›
      by (metis G2 greaterThanAtMost_iff greaterThanLessThan_iff le_eq_less_or_eq)
    ultimately show ?thesis
      using ‹li' ≤ hi0›
      apply clarsimp
      by (metis Suc_leD Suc_lessE ‹xs ! (li' - 1) < p› diff_Suc_1 greaterThanAtMost_iff le_def unfold_lt_to_le)
  next
    case 2
    hence "p < xs!(hi'+1)" using HI'_TO_HI by simp
    moreover have "(∀i∈{li0-1..<li'}. xs ! i ≤ p)" using G1 ‹xs ! (li0 - Suc 0) ≤ p› 
      apply clarsimp
      by (metis atLeastLessThan_iff le_antisym le_refl nat_le_Suc_less_imp nat_less_le nat_neq_iff)
    ultimately show ?thesis
      using ‹li0 - Suc 0 ≤ hi'›
      apply clarsimp
      by (meson atLeastLessThan_iff le_SucI le_def unfold_lt_to_le)
  next
    case 3
    then show ?thesis using ‹li≤hi› by linarith
  qed
qed  

lemma qsg_part_12: "qsg_part_assn1 li0 hi0 p xs0 li hi xs 
  ⟹ ungrd_qsg_next_lh_spec (li0-1) hi0 xs p li hi ≤ SPEC (λ(li',hi').
    qsg_part_assn2 li0 hi0 p xs0 li' hi' xs ∧ hi'<hi
     )"
  unfolding ungrd_qsg_next_lh_spec_def ungrd_qsg_next_l_spec_def ungrd_qsg_next_h_spec_def
  apply refine_vcg
  unfolding qsg_part_assn1_def
  apply (clarsimp_all simp: slice_eq_mset_eq_length)
  subgoal by (metis hd_drop_conv_nth slice_eq_mset_def)
  subgoal by linarith
  subgoal for i
    apply (subst slice_eq_mset_nth_outside, assumption)
    apply auto
    by (metis diff_diff_cancel less_imp_diff_less slice_eq_mset_eq_length)
  subgoal for hi' li'  
    unfolding qsg_part_assn2_def
    apply (clarsimp intro!: qsg_part_12_aux)
    apply (blast dest: qsg_part_12_aux)
    done
  done  

  
  
definition "qsg_partition_aux li0 hi0 p xs0 ≡ doN {
  ― ‹Initialize›
  ASSERT (li0>0);
  (li,hi) ← ungrd_qsg_next_lh_spec (li0-1) hi0 xs0 p li0 hi0;
  
  (xs,li,hi) ← WHILEIT 
    (λ(xs,li,hi). qsg_part_assn2 li0 hi0 p xs0 li hi xs)
    (λ(xs,li,hi). li<hi) 
    (λ(xs,li,hi). doN {
      ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
      xs ← mop_list_swap xs li hi;
      let li = li + 1;
      
      (li,hi) ← ungrd_qsg_next_lh_spec (li0-1) hi0 xs p li hi;
      RETURN (xs,li,hi)
    }) 
    (xs0,li,hi);
  
  RETURN (xs,li)
}"  


definition "gpartition_spec li hi p xs xs' m ≡ 
    slice_eq_mset li hi xs' xs 
  ∧ m∈{li..hi}
  ∧ (∀i∈{li..<m}. xs'!i ≤ p)
  ∧ (∀i∈{m..<hi}. p ≤ xs'!i)"


definition "gpartition_SPEC li hi p xs ≡ do {
  ASSERT (li≤hi ∧ hi≤length xs);
  SPEC (λ(xs',m). gpartition_spec li hi p xs xs' m)
}"

lemma qsg_part1_init: "⟦0 < li; hi < length xs; xs ! (li - Suc 0) ≤ p; p ≤ xs ! hi; li ≤ hi⟧ ⟹ qsg_part_assn1 li hi p xs li hi xs"
  unfolding qsg_part_assn1_def
  by simp

lemma qsg_part2_in_bounds: 
  assumes "qsg_part_assn2 li0 hi0 p xs0 li hi xs" 
  shows "li<length xs" "hi<length xs"
  using assms unfolding qsg_part_assn2_def
  by (auto dest: slice_eq_mset_eq_length)
  
  
lemma qsg_part_21: "⟦qsg_part_assn2 li0 hi0 p xs0 li hi xs; li < hi⟧ ⟹ qsg_part_assn1 li0 hi0 p xs0 (Suc li) hi (swap xs li hi)"
  unfolding qsg_part_assn2_def qsg_part_assn1_def
  apply (intro conjI)
  apply clarsimp_all
  subgoal by (metis atLeastLessThan_iff diff_diff_cancel less_Suc_eq_le less_imp_diff_less nat_less_le slice_eq_mset_eq_length swap_indep swap_nth1)
  subgoal by (metis Suc_diff_Suc diff_is_0_eq greaterThanLessThan_iff nat.simps(3) not_less_iff_gr_or_eq slice_eq_mset_eq_length strict_itrans swap_indep swap_nth2)
  done
  
lemma qsg_part_2fin: "⟦qsg_part_assn2 li0 hi0 p xs0 li hi xs; ¬ li < hi⟧ ⟹ gpartition_spec li0 hi0 p xs0 xs li"  
  unfolding qsg_part_assn2_def gpartition_spec_def
  apply clarsimp
  by (metis atLeastLessThan_iff atLeastSucLessThan_greaterThanLessThan le_antisym linorder_le_less_linear nat_Suc_less_le_imp)
  
lemma qsg_partition_aux_correct:
  "⟦0<li; hi<length xs; xs!(li-1) ≤ p; p ≤ xs!hi⟧ ⟹ qsg_partition_aux li hi p xs ≤ gpartition_SPEC li hi p xs"  
  unfolding qsg_partition_aux_def gpartition_SPEC_def
  apply (refine_vcg WHILEIT_rule[where R="measure (λ(_,_,hi). hi)"] qsg_part_12[where xs0=xs])  
  apply clarsimp_all
  subgoal by (simp add: qsg_part1_init)
  subgoal by (simp add: qsg_part2_in_bounds)
  subgoal by (simp add: qsg_part2_in_bounds)
  subgoal by (simp add: qsg_part_21)
  subgoal by (simp add: qsg_part_2fin)
  done    

definition "qsg_partition li0 hi0 p xs0 ≡ do {
  ASSERT (li0+1<hi0 ∧ hi0≤length xs0);

  (e0,xs) ← mop_idx_v_swap xs0 li0 (COPY p);
  let li=li0+1;
  
  let hi=hi0-1;
  (eN,xs) ← mop_idx_v_swap xs hi (COPY p);

  (xs,m) ← qsg_partition_aux li hi p xs;
  
  let li = li-1;

  let e0ok = e0 ≤ p;
  let eNok = p ≤ eN;
  (_,xs) ← mop_idx_v_swap xs li e0;
  (_,xs) ← mop_idx_v_swap xs hi eN;
  
  ASSERT (slice_eq_mset li (hi+1) xs xs0);
  
  if e0ok ∧ eNok then
    RETURN (xs,m)
  else if e0ok ∧ ¬eNok then do {
    xs ← mop_list_swap xs m hi;
    ASSERT (m<hi0);
    let m=m+1;
    RETURN (xs,m)
  } else if eNok then do {
    ASSERT (1≤m);
    let m=m-1;
    xs ← mop_list_swap xs li m;
    RETURN (xs,m)
  } else do {
    xs ← mop_list_swap xs li hi;
    RETURN (xs,m)
  }
  
}"


term mop_cmp_idx_v

definition "qsg_partition_wrapper li hi p xs ≡ do {
  if li<hi then (
    if li+1<hi then qsg_partition li hi p xs
    else doN {
      ifN mop_cmp_idx_v xs li p then RETURN (xs,hi)
      else RETURN (xs,li)
    }
  ) else RETURN (xs,li)
}"


lemma qsg_partition_correct: "li+1<hi ⟹ qsg_partition li hi p xs ≤ gpartition_SPEC li hi p xs"
  unfolding qsg_partition_def gpartition_SPEC_def
  apply (refine_vcg qsg_partition_aux_correct[THEN order_trans])
  apply simp_all
  apply clarsimp_all
  apply simp_all
  unfolding gpartition_SPEC_def
  apply refine_vcg
  apply clarsimp_all
  apply simp_all
  unfolding gpartition_spec_def
  apply clarsimp_all
  apply (simp_all add: slice_eq_mset_eq_length)
  subgoal for xs' m
    apply (drule slice_eq_mset_upd_outside[where i="li" and x="xs ! li"]; simp?)
    apply (drule slice_eq_mset_upd_outside[where i="hi - Suc 0" and x="xs ! (hi - Suc 0)"]; simp?)
    apply (simp add: list_update_swap)
    apply (erule slice_eq_mset_subslice)
    apply auto
    done
  subgoal for xs' m
    apply (intro conjI)
    subgoal by simp
    subgoal by (auto simp: nth_list_update' slice_eq_mset_eq_length)
    subgoal by (clarsimp simp: nth_list_update' slice_eq_mset_eq_length)
    done
  subgoal for xs' m
    apply (intro conjI)
    subgoal
      apply (simp (no_asm_simp) add: slice_eq_mset_eq_length swap_nth nth_list_update) 
      using connex
      by blast
    subgoal by (fastforce simp: slice_eq_mset_eq_length swap_nth nth_list_update)
    done
  subgoal for xs' m
    apply (intro conjI)
    subgoal by (metis Suc_le_D Suc_to_right atLeastLessThan_iff le_Suc_eq le_eq_less_or_eq nz_le_conv_less slice_eq_mset_swap(1) zero_less_Suc)
    subgoal by simp 
    subgoal by simp 
    subgoal by (fastforce simp add: slice_eq_mset_eq_length swap_nth nth_list_update) 
    subgoal
      apply (simp (no_asm_simp) add: slice_eq_mset_eq_length swap_nth nth_list_update)
      apply safe
      subgoal using connex apply blast done
      subgoal by (metis atLeastLessThan_iff le_def le_eq_less_or_eq nat_le_Suc_less_imp)
      subgoal using connex by blast
      subgoal using connex by blast
      subgoal by (metis Suc_le_D Suc_le_lessD Suc_to_right atLeastLessThan_iff nat_in_between_eq(2))
      by (meson atLeastLessThan_iff le_antisym linorder_not_le nat_le_Suc_less_imp)
    done  
  subgoal for xs' m
    apply (intro conjI)
    subgoal by simp 
    subgoal
      apply (simp (no_asm_simp) add: slice_eq_mset_eq_length swap_nth nth_list_update) 
      using connex
      by blast
    subgoal
      apply (simp (no_asm_simp) add: slice_eq_mset_eq_length swap_nth nth_list_update)
      by (meson atLeastLessThan_iff connex diff_is_0_eq' diffs0_imp_equal le_def nat_le_Suc_less_imp)
    done
  done

  
  sepref_register gpartition_SPEC
  
  lemma qsg_partition_wrapper_refine: "(qsg_partition_wrapper, PR_CONST gpartition_SPEC) ∈ Id → Id → Id → Id → ⟨Id⟩nres_rel"
    unfolding qsg_partition_wrapper_def
    apply (clarsimp split!: if_split intro!: nres_relI)
    subgoal by (simp add: qsg_partition_correct)
    unfolding gpartition_SPEC_def
    apply (all refine_vcg)
    apply simp_all
    unfolding gpartition_spec_def
    apply auto
    subgoal by (metis connex le_less_Suc_eq strict_itrans wo_leD)
    subgoal by (metis le_less_Suc_eq strict_itrans wo_leI)
    done
  
  
end  
  

context sort_impl_context begin

  
sepref_register ungrd_qsg_next_l_spec ungrd_qsg_next_h_spec 

(* TODO: We can get rid of the length xs restriction: the stopper element will always lie within <h, which is size_t representable! *)
sepref_definition qsg_next_l_impl [llvm_inline] is "uncurry3 (qsg_next_l)" :: "size_assnk *a (arr_assn)k *a elem_assnk *a size_assnk →a size_assn"
  unfolding qsg_next_l_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref

lemmas [sepref_fr_rules] = qsg_next_l_impl.refine[FCOMP qsg_next_l_refine]  
  
term qsg_next_h

sepref_definition qsg_next_h_impl [llvm_inline] is "uncurry3 (qsg_next_h)" :: "size_assnk *a (arr_assn)k *a elem_assnk *a size_assnk →a size_assn"
  unfolding qsg_next_h_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref
  
lemmas [sepref_fr_rules] = qsg_next_h_impl.refine[FCOMP qsg_next_h_refine]  
  

sepref_register qsg_partition_aux  
sepref_def qsg_partition_aux_impl (*[llvm_inline]*) is "uncurry3 (PR_CONST qsg_partition_aux)" 
  :: "[λ_. True]c size_assnk *a size_assnk *a elem_assnk *a (arr_assn)d 
    → arr_assn ×a size_assn [λ(((_,_),_),ai) (r,_). r=ai]c"
  unfolding qsg_partition_aux_def PR_CONST_def ungrd_qsg_next_lh_spec_def
  apply (simp only: nres_monad_laws split)
  apply (annot_snat_const "TYPE(size_t)")
  by sepref

(* TODO: Move *)                  
lemma unfold_let_le: "(let x = a≤b in f x) = (let x = ¬ b<a in f x)"  
  by (simp add: unfold_le_to_lt)
        
(* TODO: Move *)                  
  
definition "list_guarded_swap xs i j ≡ if i≠j then mop_list_swap xs i j else RETURN xs "  
  
lemma list_guarded_swap_refine[refine]: 
  "⟦ (xs,xs')∈⟨Id⟩list_rel; (i,i')∈Id; (j,j')∈Id ⟧ ⟹ list_guarded_swap xs i j ≤⇓Id (mop_list_swap xs' i' j')"
  unfolding list_guarded_swap_def
  apply simp
  apply refine_vcg
  by simp

sepref_register list_guarded_swap  
  
sepref_def list_guarded_swap_impl [llvm_inline] is "uncurry2 list_guarded_swap" 
  :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk → arr_assn [λ((p,_),_) r. r=p]c"
  unfolding list_guarded_swap_def
  by sepref

end

context sort_impl_copy_context begin
  
(* Some refinement to tame exploding sepref *)  
definition "qsg_partition_swap_back hi0 li hi m xs e0ok eNok ≡ do {
  if e0ok ∧ eNok then
    RETURN (xs,m)
  else if e0ok ∧ ¬eNok then do {
    xs ← list_guarded_swap xs m hi;
    ASSERT (m<hi0);
    let m=m+1;
    RETURN (xs,m)
  } else if eNok then do {
    ASSERT (1≤m);
    let m=m-1;
    xs ← list_guarded_swap xs li m;
    RETURN (xs,m)
  } else do {
    xs ← list_guarded_swap xs li hi;
    RETURN (xs,m)
  }

}"
  
definition "qsg_partition2 li hi0 p xs0 ≡ do {
  (e0,xs) ← mop_idx_v_swap xs0 li (COPY p);
  ASSERT (li<hi0);
  let li=li+1;
  
  ASSERT (hi0>0);
  let hi=hi0-1;
  (eN,xs) ← mop_idx_v_swap xs hi (COPY p);

  (xs,m) ← qsg_partition_aux li hi p xs;
  
  ASSERT (li>0);
  let li = li-1;

  let e0ok = e0 ≤ p;
  let eNok = p ≤ eN;
  (_,xs) ← mop_idx_v_swap xs li e0;
  (_,xs) ← mop_idx_v_swap xs hi eN;

  qsg_partition_swap_back hi0 li hi m xs e0ok eNok
}"

lemma qsg_partition2_refine: "(PR_CONST  qsg_partition2, PR_CONST qsg_partition) ∈ Id → Id → Id → Id → ⟨Id⟩nres_rel"
  unfolding qsg_partition2_def qsg_partition_def qsg_partition_swap_back_def PR_CONST_def
  apply refine_rcg
  apply refine_dref_type
  apply simp_all
  done

sepref_register qsg_partition_swap_back

sepref_def qsg_partition_swap_back_impl is "uncurry6 (qsg_partition_swap_back)" 
  :: "[λ_. True]c size_assnk *a size_assnk *a size_assnk *a size_assnk *a (arr_assn)d *a bool1_assnk *a bool1_assnk
    → arr_assn ×a size_assn [λ((((((_,_),_),_),ai),_),_) (r,_). r=ai]c"
  unfolding qsg_partition_swap_back_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref_dbg_keep
  
  

sepref_register qsg_partition

sepref_definition qsg_partition_impl [llvm_code] (*[llvm_inline]*) is "uncurry3 (PR_CONST qsg_partition2)" 
  :: "[λ_. True]c size_assnk *a size_assnk *a elem_assnk *a (arr_assn)d 
    → arr_assn ×a size_assn [λ(((_,_),_),ai) (r,_). r=ai]c"
  unfolding qsg_partition2_def PR_CONST_def unfold_let_le
  supply [[goals_limit = 1]]
  apply (annot_snat_const "TYPE(size_t)")
  apply sepref_dbg_keep
  done

lemmas qsg_partition_impl'_hnr[sepref_fr_rules] = qsg_partition_impl.refine[FCOMP qsg_partition2_refine]


sepref_register qsg_partition_wrapper
sepref_definition qsg_partition_wrapper_impl [llvm_code] is "uncurry3 (qsg_partition_wrapper)"
  :: "[λ_. True]c size_assnk *a size_assnk *a elem_assnk *a (arr_assn)d 
    → arr_assn ×a size_assn [λ(((_,_),_),ai) (r,_). r=ai]c"
  unfolding qsg_partition_wrapper_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref


lemmas qsg_partition_wrapper_impl'_hnr[sepref_fr_rules] = qsg_partition_wrapper_impl.refine[FCOMP qsg_partition_wrapper_refine]  
  

end

end