proposition: Lemma body_sink: semax_body Vprog Gprog f_sink sink_spec.
proof: Proof. start_function. assert (Hc : i = Zlength arr_contents \/ 0 <= i < Zlength arr_contents) by lia. destruct Hc as [Hc | Hc]. * forward_loop ( PROP () LOCAL (temp _k (Vint (Int.repr i)); temp _first_available (Vint (Int.repr first_available))) SEP (harray arr_contents arr) ). entailer!. forward_if False. exfalso. lia. forward. Exists arr_contents. entailer!. eapply weak_heapOrdered_bounded_oob. 2: apply H3. rewrite Zlength_correct, Nat2Z.id. apply le_refl. * assert (Hx : i < Zlength arr_contents) by lia. specialize (H2 Hx). clear H1 Hx. rename H2 into H1. rename H3 into H2. forward_loop (EX i' : Z, EX arr_contents' : list heap_item, PROP (0 <= i' < Zlength arr_contents; sink arr_contents (Z.to_nat i) = sink arr_contents' (Z.to_nat i')) LOCAL (temp _k (Vint (Int.repr i')); temp _arr arr; temp _first_available (Vint (Int.repr first_available))) SEP (harray arr_contents' arr)). Exists i arr_contents. entailer!. Intros i' arr_contents'. assert (Zlength arr_contents = Zlength arr_contents'). { unfold sink in H4. generalize (sink_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat i)); intro. generalize (sink_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat i')); intro. apply Permutation_Zlength in H5. apply Permutation_Zlength in H6. congruence. } forward_if (Zleft_child i' < first_available). { forward. entailer!. rewrite Zleft_child_unfold; lia. } { forward. Exists arr_contents'. entailer!. unfold sink at 2 in H4. rewrite <- Zleft_child_unfold in H6; try lia. unfold Zleft_child in H6. rewrite H5 in H6. rewrite Zlength_correct in H6. erewrite sink_done in H4. 2: apply Znth_nth_error; lia. rewrite <- H4. { split. * apply sink_hO_bounded. apply cmp_po. apply cmp_linear. apply H2. * apply sink_permutation. } intros. assert (left_child (Z.to_nat i') < length arr_contents')%nat by (apply nth_error_Some; congruence). lia. intros. assert (right_child (Z.to_nat i') < length arr_contents')%nat by (apply nth_error_Some; congruence). unfold right_child in H7. lia. } forward. rewrite mul_repr, add_repr. rewrite <- Zleft_child_unfold. 2: lia. forward_if (EX b : bool, PROP (if b then Zright_child i' < first_available /\ cmp_rel (Znth (Zright_child i') arr_contents') (Znth (Zleft_child i') arr_contents') else Zright_child i' >= first_available \/ ~cmp_rel (Znth (Zright_child i') arr_contents') (Znth (Zleft_child i') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool b); temp _k (Vint (Int.repr i')); temp _j (Vint (Int.repr (Zleft_child i'))); temp _arr arr; temp _first_available (Vint (Int.repr first_available))) SEP (harray arr_contents' arr)). { forward_call (Zright_child i', Zleft_child i', arr, arr_contents'). { entailer!. simpl. repeat f_equal. rewrite Zright_child_unfold, Zleft_child_unfold; lia. } { rewrite Int.unsigned_repr in H7. rewrite Zright_child_unfold, Zleft_child_unfold in *; lia. rewrite Zleft_child_unfold in *; rep_lia. } forward. Exists (cmp (Znth (Zright_child i') arr_contents') (Znth (Zleft_child i') arr_contents')). unfold cmp_rel. rewrite Zright_child_unfold, Zleft_child_unfold in *. rewrite Int.unsigned_repr in H7. 2,3,4,5: rep_lia. case cmp; entailer!. } { forward. Exists false. rewrite Zright_child_unfold, Zleft_child_unfold in *. rewrite Int.unsigned_repr in H7. entailer!. all: rep_lia. } Intro bo. set (j' := if bo then Zright_child i' else Zleft_child i'). forward_if (PROP (if bo then Zright_child i' < first_available /\ cmp_rel (Znth (Zright_child i') arr_contents') (Znth (Zleft_child i') arr_contents') else Zright_child i' >= first_available \/ ~cmp_rel (Znth (Zright_child i') arr_contents') (Znth (Zleft_child i') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool bo); temp _k (Vint (Int.repr i')); temp _j (Vint (Int.repr j')); temp _arr arr; temp _first_available (Vint (Int.repr first_available))) SEP (harray arr_contents' arr)); [ destruct bo; try discriminate H7 .. | ]. { forward. subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. entailer!. tauto. } { forward. entailer!!. } Intros. forward_call (i', j', arr, arr_contents'). { subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. destruct bo; lia. } forward_if (~cmp_rel (Znth i' arr_contents') (Znth j' arr_contents')); [destruct (cmp _ _) eqn:?H in H8; try discriminate H8 .. | ]. { forward. Exists arr_contents'. entailer!. unfold sink at 2 in H4. erewrite sink_done in H4; intros. rewrite <- H4. split. apply sink_hO_bounded. apply cmp_po. apply cmp_linear. apply H2. apply sink_permutation. apply Znth_nth_error. lia. * rewrite <- (Nat2Z.id (left_child _)) in H0. change (Z.of_nat _) with (Zleft_child i') in H0. rewrite Znth_nth_error in H0. 2: rewrite Zright_child_unfold, Zleft_child_unfold in *; lia. inversion H0. subst b0. clear H0. destruct bo; subst j'; auto. transitivity (Znth (Zright_child i') arr_contents'); tauto. * assert (0 <= Zright_child i' < Zlength arr_contents'). { split. unfold Zright_child. lia. apply Z2Nat.inj_lt. unfold Zright_child. lia. lia. rewrite ZtoNat_Zlength. eapply nth_error_Some. unfold Zright_child. rewrite Nat2Z.id. congruence. } rewrite <- (Nat2Z.id (right_child _)) in H0. change (Z.of_nat _) with (Zright_child i') in H0. rewrite Znth_nth_error in H0; try lia. inversion H0. subst b0. clear H0. destruct bo; subst j'. tauto. destruct H7. lia. transitivity (Znth (Zleft_child i') arr_contents'). trivial. destruct (cmp_linear (Znth (Zleft_child i') arr_contents') (Znth (Zright_child i') arr_contents')); auto. contradiction. } { forward. entailer!. unfold cmp_rel, j' in H0. congruence. } forward_call (i', j', arr, arr_contents'). { subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. destruct bo; lia. } forward. Exists j' (Zexchange arr_contents' i' j'). entailer!. split. subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. destruct bo; lia. unfold sink at 2. unfold Zexchange. erewrite sink_step. apply H4. apply Znth_nth_error; lia. unfold left_child. replace (1 + Z.to_nat i' + Z.to_nat i')%nat with (Z.to_nat (2 * i' + 1)) by lia. apply Znth_nth_error. split. lia. rewrite <- Zleft_child_unfold; try lia. rewrite <- Zleft_child_unfold; try lia. case_eq (nth_error arr_contents' (right_child (Z.to_nat i'))); intros. + assert (h = Znth (Zright_child i') arr_contents'). { rewrite <- (nat_of_Z_eq (right_child _)) in H0. rewrite Znth_nth_error in H0. inversion H0. trivial. assert ((Z.to_nat (Z.of_nat (right_child (Z.to_nat i')))) < length arr_contents')%nat by (apply nth_error_Some; congruence). rewrite Zlength_correct. lia. } subst h. assert (Zright_child i' < Zlength arr_contents'). { assert (right_child (Z.to_nat i') < length arr_contents')%nat by (apply nth_error_Some; congruence). unfold Zright_child. rewrite Zlength_correct. lia. } clear H0. subst j'. destruct bo. - right. split. unfold Zright_child. lia. tauto. - left. split. unfold Zleft_child. lia. destruct H7. lia. tauto. + subst j'. destruct bo. - rewrite H5 in H7. apply nth_error_None in H0. destruct H7. unfold Zright_child in H7. rewrite Zlength_correct in H7. lia. - split. unfold Zleft_child. lia. tauto. Time Qed. Lemma body_swim: semax_body Vprog Gprog f_swim swim_spec. Proof. start_function. rename H1 into Hz. forward_loop (EX i' : Z, EX arr_contents' : list heap_item, PROP (0 <= i' < Zlength arr_contents; swim arr_contents (Z.to_nat i) = swim arr_contents' (Z.to_nat i')) LOCAL (temp _k (Vint (Int.repr i')); temp _arr arr) SEP (harray arr_contents' arr)). Exists i arr_contents. entailer!. Intros i' arr_contents'. assert (Zlength arr_contents = Zlength arr_contents'). { unfold swim in H2. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat i)); intro. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat i')); intro. apply Permutation_Zlength in H3. apply Permutation_Zlength in H4. congruence. } generalize (parent_le (Z.to_nat i')); intro Hq. assert (Hx: i' = 0 \/ i' > 0) by lia. forward_if (EX b : bool, PROP (if b then i' > 0 /\ cmp_rel (Znth i' arr_contents') (Znth (Zparent i') arr_contents') else i' = 0 \/ ~cmp_rel (Znth i' arr_contents') (Znth (Zparent i') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool b); temp _k (Vint (Int.repr i')); temp _arr arr) SEP (harray arr_contents' arr)). { destruct Hx as [Hx | Hx]. subst i'. inversion H4. forward_call (i', Zparent i', arr, arr_contents'). { entailer!. rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. } { assert (parent (Z.to_nat i') <= (Z.to_nat i'))%nat by apply parent_le. unfold Zparent. lia. } forward. unfold cmp_rel. case (cmp (Znth i' arr_contents') (Znth (Zparent i') arr_contents')). Exists true. entailer!. Exists false. entailer!. } { forward. Exists false. entailer!. } Intro b. forward_if (PROP (i' > 0 /\ cmp_rel (Znth i' arr_contents') (Znth (Zparent i') arr_contents')) LOCAL (temp _k (Vint (Int.repr i')); temp _arr arr) SEP (harray arr_contents' arr)); [ destruct b; try discriminate H4 .. | ]. { forward. entailer!!. tauto. } { forward. Exists arr_contents'. entailer!!. split. { assert (heap_ordered (swim arr_contents (Z.to_nat i))). { apply swim_hO; auto. apply cmp_po. apply cmp_linear. } unfold swim at 2 in H2. destruct H5. * subst i'. simpl in H2. rewrite swim_0 in H2. rewrite <- H2. trivial. * erewrite swim_done in H2; eauto. rewrite <- H2. trivial. apply Znth_nth_error; lia. unfold Zparent. rewrite <- Znth_nth_error; try lia. rewrite Nat2Z.id. trivial. } { unfold swim in H2. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat i)); intro. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat i')); intro. rewrite H2 in H6. etransitivity. apply H6. symmetry. trivial. } } forward_call (i', Zparent i', arr, arr_contents'). { entailer!. rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. } { unfold Zparent. lia. } forward. Exists (Zparent i') (Zexchange arr_contents' i' (Zparent i')). entailer!. split. unfold Zparent. lia. split. * destruct H4. unfold swim, Zparent, Zexchange in *. rewrite Nat2Z.id. erewrite swim_step. congruence. rewrite H3, Zlength_correct in H1. 4: apply H5. 2: apply Znth_nth_error. 3: rewrite <- Znth_nth_error. 3: rewrite Nat2Z.id; trivial. 1,2,3: lia. * rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. Time Qed. Lemma body_insert_nc: semax_body Vprog Gprog f_insert_nc insert_nc_spec. Proof. start_function. unfold valid_pq. Intros arr junk. destruct junk. { exfalso. unfold heap_size, heap_capacity in *. rewrite Zlength_app, Zlength_nil in H2. lia. } change (h0 :: junk) with ([h0] ++ junk) in *. rewrite app_assoc in *. rewrite harray_split. Intros. assert (0 <= heap_size h) by apply Zlength_nonneg. forward. unfold harray. entailer!. forward. unfold hitem. forward. unfold harray at 1. forward. entailer!. rewrite Zlength_app, Zlength_one. unfold heap_size in *. lia. forward. forward. forward. { entailer!. apply H10. discriminate. } forward. assert (0 <= heap_size h < Zlength (heap_items h ++ [h0])). { rewrite Zlength_app, Zlength_one. unfold heap_size in *. lia. } entailer!. forward. forward. deadvars!. rewrite upd_Znth_overwrite, upd_Znth_same, map_app, upd_Znth_app2, Zlength_map. unfold heap_size at 3. rewrite Z.sub_diag. simpl fst. change (Vint (fst iv), Vint (snd iv)) with (heap_item_rep iv). rewrite upd_Znth_map. rewrite <- map_app. rewrite upd_Znth0. 2,3,4: autorewrite with sublist; unfold heap_size in *; lia. replace (Zlength (heap_items h ++ [h0])) with (Zlength (heap_items h ++ [iv])). 2: do 2 rewrite Zlength_app, Zlength_one; lia. forward_call (heap_size h, arr, heap_items h ++ [iv]). { rewrite Zlength_app, Zlength_one. unfold heap_size in *. split. lia. split. - red. rewrite Zlength_correct, Nat2Z.id. apply weak_heapOrdered2_postpend. apply cmp_po. trivial. - rep_lia. } Intro vret. forward. forward. Exists ((Z.to_nat (heap_capacity h))%nat, vret). unfold heap_capacity. rewrite Nat2Z.id. simpl fst. unfold valid_pq. entailer!. * transitivity (snd h ++ [iv]); trivial. change (iv :: heap_items h) with ([iv] ++ heap_items h). apply Permutation_app_comm. * Exists arr junk. entailer!. + rewrite Zlength_app. apply Permutation_Zlength in H5. unfold heap_items. simpl. rewrite <- H5. unfold heap_capacity in *. simpl. rewrite <- H2. autorewrite with sublist. lia. + unfold heap_size, heap_capacity, heap_items. simpl fst. simpl snd. generalize (Permutation_Zlength _ _ _ H5); intro. rewrite <- H10. replace (Zlength (heap_items h ++ [iv])) with (Zlength (snd h) + 1). 2: rewrite Zlength_app; trivial. cancel. rewrite harray_split. cancel. repeat rewrite Zlength_app. rewrite <- H10. rewrite Zlength_app. apply derives_refl. Time Qed. Lemma body_remove_min_nc: semax_body Vprog Gprog f_remove_min_nc remove_min_nc_spec. Proof. start_function. unfold valid_pq. Intros arr junk. rewrite harray_split. Intros. destruct h. destruct l. inversion H. unfold heap_items, heap_capacity, heap_size in *. simpl in H, H0, H1 |-*. clear H. generalize (foot_split_spec _ (h :: l)). case foot_split. destruct o; intro. 2: destruct H; subst l0; discriminate. rename h into root. rename h0 into foot. assert (Hx: Zlength l = Zlength (root :: l) - 1) by (rewrite Zlength_cons; lia). assert (Hy : 0 <= Zlength l) by apply Zlength_nonneg. forward. forward. forward. forward. unfold harray. entailer!. forward_call (0, Zlength l, arr, root :: l). entailer!. simpl. congruence. { simpl in H2. rewrite app_comm_cons, Zlength_app in H2. rep_lia. } forward. forward. unfold harray at 1. assert (Hrl: 0 <= Zlength (root :: l) - 1 <= Int.max_unsigned). { simpl in H2. rewrite app_comm_cons, Zlength_app in H2. rep_lia. } forward. { entailer!. rewrite Zlength_Zexchange. lia. } { entailer!. rewrite Znth_map. rewrite <- Hx. rewrite Znth_Zexchange'; try lia. rewrite Znth_0_cons. unfold heap_item_rep. trivial. rewrite Zlength_Zexchange. lia. } unfold hitem. forward. forward. forward. forward. { entailer!. rewrite Zlength_Zexchange. lia. } { entailer!. rewrite Znth_map. 2: rewrite Zlength_Zexchange; lia. rewrite <- Hx. rewrite Znth_Zexchange'; try lia. rewrite Znth_0_cons. apply Forall_map in H6. rewrite Forall_Znth in H6. specialize (H6 (Zlength l)). do 2 rewrite Zlength_map in H6. rewrite Zlength_Zexchange in H6. assert (Hq: 0 <= (Zlength l) < Zlength (root :: l)) by lia. specialize (H6 Hq). rewrite Znth_map in H6. 2: rewrite Zlength_map, Zlength_Zexchange; lia. rewrite Znth_map in H6. 2: rewrite Zlength_Zexchange; lia. rewrite Znth_Zexchange' in H6; try lia. apply H6. discriminate. } change (data_at _ _ _ arr) with (harray (Zexchange (root :: l) 0 (Zlength l)) arr). forward. forward. forward. rewrite <- Hx. rewrite Znth_map. 2: rewrite Zlength_Zexchange; lia. rewrite Znth_Zexchange'; try lia. rewrite Znth_0_cons. autorewrite with norm. rewrite <- Hx. unfold heap_item_rep. rewrite H. destruct l. * destruct l0. 2: destruct l0; discriminate. inversion H. subst foot. clear H Hx. simpl. forward_call (0, arr, @nil heap_item, 0, 0). rewrite Zlength_nil. { rewrite Zexchange_eq. unfold harray. rewrite data_at_isptr. entailer. rewrite data_at_zero_array_eq; auto. entailer!. } { split. split; inversion 1. apply weak_heapOrdered_bounded_root_weak_heapOrdered. apply hOwhO. apply cmp_po. apply heapOrdered_empty. } Intro vret. Exists (n, vret) root. Intros. simpl fst. simpl snd. apply Permutation_nil in H3. subst vret. clear H Hy. sep_apply harray_emp. do 2 rewrite fold_harray. unfold valid_pq, hitem. first [now entailer ! | entailer; Exists arr (root :: junk); simpl; entailer!; [apply heapOrdered_empty | rewrite <- harray_split; apply derives_refl]]. * destruct l0; inversion H. subst h0. deadvars!. assert (Zlength (h :: l) = Zlength (root :: l0)). { rewrite H5, Zlength_app, Zlength_one, Zlength_cons. lia. } rewrite H3, Zexchange_head_foot. rewrite harray_split. forward_call (0, arr, (foot :: l0), Zlength (foot :: l0), 0). entailer!. { split. intros _. generalize (Zlength_nonneg junk); intro. simpl in H2. repeat rewrite Zlength_cons in *. rewrite Zlength_app in H2. lia. apply weak_heapOrdered_bounded_root_weak_heapOrdered. apply weak_heapOrdered_root with root. rewrite H5, app_comm_cons in H1. apply heapOrdered_cutfoot in H1. trivial. } Intro vret. Exists (n, vret) root. simpl fst. unfold hitem, heap_item_rep, heap_size, heap_capacity. simpl fst. simpl snd. entailer!. { split. constructor. rewrite H5. transitivity ([foot] ++ l0). apply Permutation_app_comm. auto. generalize (root_minimal _ _ _ _ H1 root eq_refl); intro. rewrite H5 in H11. apply Forall_inv_tail in H11. eapply forall_permutation. apply H11. transitivity ([foot] ++ l0). apply Permutation_app_comm. simpl. tauto. } unfold valid_pq. Exists arr (root :: junk). unfold heap_size, heap_capacity. simpl. replace (Zlength vret) with (Zlength (root :: l0)). 2: { apply Permutation_Zlength in H6. trivial. } apply heapOrdered_bounded_root_heapOrdered in H4. entailer!. { simpl fst in H2. rewrite <- H2. apply Permutation_Zlength in H6. autorewrite with sublist. rewrite <- H6. simpl snd. autorewrite with sublist in *. lia. } change (root :: junk) with ([root] ++ junk). rewrite app_assoc. do 2 rewrite harray_split. apply Permutation_Zlength in H6. rewrite app_comm_cons. rewrite Zlength_app. rewrite H6. rewrite Zlength_app. assert (Zlength (root :: l0) = Zlength vret). { rewrite <- H6. do 2 rewrite Zlength_cons. trivial. } do 3 rewrite app_comm_cons. do 4 rewrite Zlength_app. rewrite H11. do 2 rewrite Zlength_one. rewrite Zlength_cons. rewrite H3, H11. cancel. Time Qed. Lemma body_less: semax_body Vprog Gprog f_less less_spec. Proof. start_function. unfold harray. forward. rewrite Znth_map; trivial. forward. do 2 (rewrite Znth_map; trivial). forward. entailer!!. repeat rewrite Znth_map in * by trivial. simpl. unfold cmp. destruct (negb _); auto. Time Qed. Lemma body_size: semax_body Vprog Gprog f_size size_spec. Proof. start_function. unfold valid_pq. Intros arr junk. forward. forward. unfold valid_pq. Exists arr. Exists junk. entailer!. Time Qed. Lemma body_capacity: semax_body Vprog Gprog f_capacity capacity_spec. Proof. start_function. unfold valid_pq. Intros arr junk. forward. forward. unfold valid_pq. Exists arr. Exists junk. entailer!. Time Qed. Lemma heap_item_rep_morph: forall x y, (fst (heap_item_rep x), snd (heap_item_rep y)) = heap_item_rep (fst x, snd y). Proof. unfold heap_item_rep. destruct x,y; reflexivity. 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