Solution for Arrays.QuickSort.triple_quicksort
introv Hn Hi. gen i L. induction_wf IH: (downto 0) n. intros.
xwp. xapp. xif; intros C.
{ xapp triple_pivot; try math. intros j x L0 L1 L2 (HP&EL0&Hj&H1&H2).
subst L0. lets E: permut_length HP. rew_list in *.
xchange hseg_app. xchange hseg_cons. rew_list.
xapp. xapp; try math. intros L1' (HP1&HS1).
lets EQ1: permut_length HP1. math_rewrite (i + length L1 + 1 = j + 1).
xapp. xapp. xapp. xapp; try math. intros L2' (HP2&HS2).
lets EQ2: permut_length HP2.
xchange (>> hseg_cons_r (vals_int L2')). { math. }
xchange hseg_app_r. { rew_list. math. }
xsimpl (L1' ++ x :: L2').
{ split.
{ applys permut_trans HP. applys* permut_app. applys* permut_cons. }
{ applys* sorted_app_le. applys permut_Forall H1 HP1.
applys* sorted_cons_gt. applys permut_Forall H2 HP2. } }
{ rew_list*. } }
{ xval. xsimpl*. split.
{ applys permut_refl. }
{ destruct L as [|x[|]].
{ applys sorted_nil. }
{ applys sorted_one. }
{ rew_list in Hn. false. math. } } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback