proposition: Lemma body_heapsort: semax_body Vprog Gprog f_heapsort_rev heapsort_rev_spec.
proof: Proof. start_function. assert_PROP (2 * (size - 2) <= Int.max_unsigned). { apply prop_right. rep_lia. } forward_call (arr, arr_contents, size). Intros arr_contents'. forward. forward_loop (EX s : Z, EX arr_contents1 : list heap_item, EX arr_contents2 : list heap_item, PROP (s > 0 ; s = Zlength arr_contents1; heap_ordered arr_contents1; Sorted (Basics.flip cmp_rel) arr_contents2; Forall (fun x => HdRel (Basics.flip cmp_rel) x arr_contents2) arr_contents1; Permutation arr_contents (arr_contents1 ++ arr_contents2)) LOCAL (temp _arr arr; temp _active (Vint (Int.repr s))) SEP (harray (arr_contents1 ++ arr_contents2) arr)). { Exists size arr_contents' (@nil heap_item). rewrite app_nil_r. entailer!. split. apply Permutation_Zlength. trivial. apply Forall_forall. constructor. } Intros s arrc1 arrc2. generalize (Permutation_Zlength _ _ _ H9); intro. rewrite Zlength_app in H10. forward_if. 2: { assert (s = 1) by rep_lia. subst s. destruct arrc1. rewrite Zlength_nil in H12; lia. destruct arrc1. 2: do 2 rewrite Zlength_cons in H12; rep_lia. rewrite H12. forward. Exists (h :: arrc2). entailer!. 2: apply derives_refl. constructor. trivial. rewrite Forall_forall in H8. apply H8. left. trivial. } forward. rewrite harray_split. Intros. forward_call (0, s-1, arr, arrc1). destruct arrc1. rewrite Zlength_nil in H5. lia. generalize (foot_split_spec _ (h :: arrc1)). case foot_split. destruct o. 2: intros [? ?]; subst; discriminate. intros. destruct l. destruct arrc1. 2: discriminate. inversion H12. subst h0. clear H12. { rewrite Zlength_one in H5. lia. } assert (h1 = h) by (inversion H12; auto). subst h1. rewrite H12 in *. clear H12 arrc1. replace (s - 1) with (Zlength (h :: l)). 2: autorewrite with sublist in *; rep_lia. rewrite Zexchange_head_foot. rewrite harray_split. Intros. forward_call (0, arr, (h0 :: l), s-1, 0). { split. autorewrite with sublist in *. rep_lia. apply weak_heapOrdered_bounded_root_weak_heapOrdered. eapply weak_heapOrdered_root. apply heapOrdered_cutfoot in H6. apply H6. } Intros arrc1. Exists (s-1) arrc1 (h :: arrc2). entailer!. { split. apply Permutation_Zlength in H13. autorewrite with sublist in *. trivial. split. apply heapOrdered_bounded_root_heapOrdered. apply H12. split. constructor. trivial. inversion H8. trivial. split. * apply Forall_forall. intros. constructor. symmetry in H13. generalize (Permutation_in x H13 H0); intro. generalize (root_minimal _ cmp_rel cmp_po _ H6 h eq_refl); intro. rewrite Forall_forall in H14. apply H14. rewrite <- app_comm_cons. right. apply in_or_app. destruct H5. subst x. right. left. trivial. auto. * apply Permutation_trans with (((h :: l) ++ [h0]) ++ arrc2). trivial. change (h :: arrc2) with ([h] ++ arrc2). rewrite app_assoc. apply Permutation_app. 2: apply Permutation_refl. apply Permutation_trans with (h :: arrc1). 2: apply Permutation_cons_append. simpl. constructor. apply Permutation_app_comm_trans. apply H13. } { apply Permutation_Zlength in H13. rewrite Zlength_app. rewrite H13. rewrite <- Zlength_app. rewrite <- harray_split. rewrite Zlength_app. replace (Zlength ((h :: l) ++ [h0])) with (Zlength (arrc1 ++ [h])). rewrite <- Zlength_app. rewrite <- harray_split. rewrite <- app_assoc. apply derives_refl. autorewrite with sublist in *. lia. } Qed.
imports: RelationClasses Sorting VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap CertiGraph.binheap.env_binary_heap