proposition: Lemma body_free: semax_body Vprog Gprog f_pq_free pq_free_spec.
proof: Proof. start_function. unfold valid_pq, linked_heap_array, heap_array, lookup_array. Intros arr junk lookup lookup_contents. forward. sep_apply (data_at_data_at_ Tsh (tarray t_item (Zlength (heap_items h ++ junk)))). sep_apply free_items. sep_apply (data_at_data_at_ Tsh (tarray tuint (Zlength lookup_contents))). sep_apply free_lookup. simpl. rewrite !Zaux.Zdiv_eucl_unique. rewrite H2. change (16 / 4) with 4. rewrite Z.mul_comm, Z_div_mult. change 12 with (3 * 4) at 1. rewrite <- Z.mul_assoc. rewrite (Z.mul_comm 4), Z.mul_assoc, Z_div_mult. 2,3: lia. rewrite H. rewrite (Z.mul_comm (heap_capacity h)). forward_call (lookup, heap_capacity h). forward. change 12 with (4 * 3). rewrite <- Z.mul_assoc. forward_call (arr, 3 * heap_capacity h). sep_apply data_at_data_at_. sep_apply free_pq. forward_call (pq, if Archi.ptr64 then 6 else 4). entailer!. Time Qed. Lemma body_pq_make: semax_body Vprog Gprog f_pq_make pq_make_spec. Proof. start_function. forward_call (sizeof(Tstruct _structPQ noattr)). Intros pq. sep_apply malloc_pq. forward_call (sizeof(tuint) * size). { simpl; lia. } Intros table. sep_apply malloc_lookup. lia. forward_call ((sizeof(Tstruct _structItem noattr) * size)). Intros arr. sep_apply malloc_items. lia. forward_for_simple_bound size (EX i : Z, PROP () LOCAL (temp _table (pointer_val_val table); temp _arr (pointer_val_val arr); temp _size (Vint (Int.repr size)); temp _pq (pointer_val_val pq)) SEP (initializing_item_array i size (pointer_val_val arr); free_tok (pointer_val_val arr) (sizeof (Tstruct _structItem noattr) * size); data_at Tsh (tarray tuint size) (initializing_inc_list i size) (pointer_val_val table); free_tok (pointer_val_val table) (sizeof tuint * size); data_at_ Tsh t_pq (pointer_val_val pq); free_tok (pointer_val_val pq) (sizeof (Tstruct _structPQ noattr)))). { entailer!. unfold initializing_item_array, initializing_inc_list, initializing_item_list. simpl. replace (size - 0) with size by lia. cancel. } { unfold initializing_item_array. forward. forward. rewrite upd_Znth_overwrite, upd_Znth_same. simpl snd. simpl fst. 2,3: rewrite Zlength_initializing_item_list; lia. forward. rewrite upd_Znth_overwrite, upd_Znth_same. simpl snd. simpl fst. 2,3: rewrite Zlength_initializing_item_list; lia. forward. rewrite initializing_inc_list_inc. 2: lia. rewrite initializing_item_list_inc. 2: lia. entailer!. } forward. forward. forward. forward. forward. Exists (pointer_val_val pq) (Z.to_nat size, @nil heap_item). unfold valid_pq, heap_size, heap_capacity. entailer!. lia. Exists (pointer_val_val arr) (initial_item_list size) (pointer_val_val table) (List_ext.nat_inc_list (Z.to_nat size)). unfold initializing_item_array, linked_heap_array, heap_array, lookup_array. rewrite Zlength_app, Zlength_nil. rewrite initializing_inc_list_done, initializing_item_list_done. rewrite Z2Nat.id, Zlength_initial_item_list, List_ext.nat_inc_list_Zlength. 2,3: lia. entailer!. { split. apply heapOrdered_empty. simpl heap_items. simpl. apply initial_link_ok. lia. } { rewrite Z2Nat.id. cancel. lia. } Time Qed. Lemma body_edit_priority: semax_body Vprog Gprog f_pq_edit_priority pq_edit_priority_spec. Proof. start_function. unfold valid_pq. Intros arr junk lookup lookup_contents. rename H0 into Hxx. rename H1 into H0. rename H2 into H1. rename H3 into H2. assert_PROP (linked_correctly (heap_items h ++ junk) lookup_contents). { unfold linked_heap_array. entailer!. } rewrite linked_heap_array_split. Intros. forward. { unfold linked_heap_array, lookup_array. Intros. entailer!. } forward. { unfold linked_heap_array, heap_array. Intros. entailer!. } unfold linked_heap_array, lookup_array. Intros. generalize H; intro. apply In_Znth_iff in H6. destruct H6 as [target [? ?]]. destruct H5. unfold proj_keys in H6, H7. rewrite Zlength_map in H6. rewrite Znth_map in H7; auto. destruct (H8 target H6). forward. unfold heap_array. assert (Hklc: 0 <= Znth key lookup_contents <= Int.max_unsigned). { specialize (H8 _ H6). cbn in H8. rewrite H7 in H8. destruct H8. rewrite Z.add_0_l in H11. rewrite H11. rewrite Zlength_app in H2. rep_lia. } forward. { entailer!. } { entailer!. rewrite Znth_map. 2: lia. rewrite H10. apply I. } forward. { entailer!. } rewrite Znth_map. 2: { rewrite <- H7. rewrite H10. lia. } rewrite <- H7. rewrite H10. change (0 + target) with target in *. remember (Znth target (heap_items h)) as hi. remember (key, newpri, heap_item_payload hi) as new_hi. forward_if. * assert (cmp_rel (key, newpri, heap_item_payload hi) hi). { unfold cmp_rel. unfold cmp. unfold heap_item_priority. simpl. rewrite H11. trivial. } forward_call (target, arr, upd_Znth target (heap_items h) new_hi, lookup, lookup_contents). { unfold linked_heap_array, heap_array, lookup_array. entailer!. * split; trivial. simpl. rewrite Zlength_upd_Znth. intros. replace (heap_item_key (Znth i (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)))) with (heap_item_key (Znth i (heap_items h))). apply H8; trivial. rewrite <- Znth_map. 2: lia. rewrite <- (Znth_map _ heap_item_key). 2: rewrite Zlength_upd_Znth; lia. rewrite <- upd_Znth_map. unfold heap_item_key at 4. simpl fst. case (eq_dec i (Znth (heap_item_key hi) lookup_contents)); intro. 2: rewrite Znth_upd_Znth_diff; auto. subst i. rewrite Znth_upd_Znth_same. rewrite Znth_map. rewrite <- Heqhi. trivial. lia. rewrite Zlength_map. lia. trivial. * rewrite <- upd_Znth_map. rewrite Zlength_upd_Znth. cancel. } { rewrite Zlength_upd_Znth. split3; trivial. - generalize (Znth_nth_error _ _ H6); intro. rewrite <- Heqhi in H13. generalize (heapOrdered_lower_priority_weak_heapOrdered2 _ _ _ _ H1 _ _ H13 _ H12); intros. rewrite upd_Znth_update. rewrite Heqnew_hi. apply H14. trivial. - rewrite Zlength_app in H2. rep_lia. } Intros vret. destruct vret as [heap_contents' lookup_contents']. Exists (fst h, heap_contents'). entailer!. + unfold heap_items. simpl snd. simpl fst in H15. symmetry in H15. transitivity (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)); trivial. replace (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)) with (update_pri_by_key (snd h) (heap_item_key hi) newpri). reflexivity. unfold update_pri_by_key. apply List_ext.list_eq_Znth; rewrite Zlength_map. { rewrite Zlength_upd_Znth. trivial. } intros. case (eq_dec i (Znth (heap_item_key hi) lookup_contents)); intro. - subst i. rewrite Znth_upd_Znth_same. 2,3: lia. rewrite Znth_map. 2: lia. change (snd h) with (heap_items h). rewrite <- Heqhi. unfold update_pri_if_key. case Z.eq_dec; auto. intro Hx; contradiction. - rewrite Znth_upd_Znth_diff; auto. rewrite Znth_map. 2: lia. unfold update_pri_if_key. case Z.eq_dec; intro; auto. destruct (H8 _ H7). unfold heap_items in H21. rewrite <- e in H21. lia. + unfold valid_pq. Exists arr junk lookup lookup_contents'. rewrite linked_heap_array_split. unfold heap_capacity, heap_size, heap_items. simpl fst in *. simpl snd in *. generalize H15; intro. apply Permutation_Zlength in H7. rewrite Zlength_upd_Znth in H7. unfold heap_items in H7. do 2 rewrite Zlength_app. rewrite H7. entailer!. split. { destruct H13. apply Permutation_Zlength in H13. rewrite <- H13. trivial. } split. { rewrite <- H7. unfold heap_items, heap_capacity in H2. rewrite <- H2. rewrite Zlength_app; trivial. } clear H17 H18 H10 H21 H11. destruct H13. split. eapply Permutation_NoDup; eauto. simpl. intros. destruct H3. generalize (H17 ((Zlength (heap_items h)) + i)); intro. spec H18. rewrite Zlength_app; rep_lia. destruct H18. rewrite app_Znth2 in H18, H21. 2,3: lia. replace (Zlength (heap_items h) + i - Zlength (heap_items h)) with i in * by lia. generalize H10; intro. apply Permutation_Zlength in H22. rewrite <- H22. split; trivial. rewrite <- H11. rewrite H21. apply Permutation_Zlength in H15. rewrite <- H15. rewrite Zlength_upd_Znth. lia. repeat intro. rename H24 into Hk. rename H21 into Hkk. apply Permutation_Znth in H15. 2: apply (0, Int.zero, Int.zero). rewrite Zlength_upd_Znth in H15. destruct H15 as [? [f [? [? ?]]]]. rewrite H25 in Hk. 2: lia. specialize (H17 (Z.of_nat (f (Z.to_nat j)))). spec H17. specialize (H21 (Z.to_nat j)). spec H21. lia. rewrite Zlength_app. lia. destruct H17. rewrite app_Znth1 in H17, H26. 2,3: specialize (H21 (Z.to_nat j)); lia. rewrite <- Znth_map in Hk. 2: rewrite Zlength_upd_Znth; specialize (H21 (Z.to_nat j)); lia. rewrite <- upd_Znth_map in Hk. unfold heap_item_key in Hk at 3; simpl in Hk. rewrite upd_Znth_map in Hk. rewrite Znth_map in Hk. 2: rewrite Zlength_upd_Znth; specialize (H21 (Z.to_nat j)); lia. clear PNarr PNlookup PNpq H16. replace (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) hi) with (heap_items h) in Hk. rewrite Hk in H26. rewrite Hkk in H26. specialize (H21 (Z.to_nat j)); lia. rewrite In_Znth_iff in H. destruct H as [spot [? ?]]. generalize (H8 spot); intro. spec H27. unfold proj_keys in H. rewrite Zlength_map in H. apply H. destruct H27. unfold proj_keys in H16. rewrite Znth_map in H16. 2: { unfold proj_keys in H. rewrite Zlength_map in H. rep_lia. } rewrite H16 in H28. rewrite H28. rewrite Heqhi. rewrite H28. rewrite upd_Znth_same_Znth. 2: lia. trivial. * assert (cmp_rel hi (heap_item_key hi, newpri, heap_item_payload hi)). { unfold cmp_rel. unfold cmp. unfold heap_item_priority. simpl. apply lt_inv in H11. case_eq (Int.lt newpri (snd (fst hi))); auto. intro. apply lt_inv in H12. lia. } forward. forward_call (target, arr, upd_Znth target (heap_items h) new_hi, heap_size h, lookup, lookup_contents). { unfold linked_heap_array, heap_array, lookup_array. entailer!. * split; trivial. simpl. rewrite Zlength_upd_Znth. intros. replace (heap_item_key (Znth i (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)))) with (heap_item_key (Znth i (heap_items h))). apply H8; trivial. rewrite <- Znth_map. 2: lia. rewrite <- (Znth_map _ heap_item_key). 2: rewrite Zlength_upd_Znth; lia. rewrite <- upd_Znth_map. unfold heap_item_key at 4. simpl fst. case (eq_dec i (Znth (heap_item_key hi) lookup_contents)); intro. 2: rewrite Znth_upd_Znth_diff; auto. subst i. rewrite Znth_upd_Znth_same. rewrite Znth_map. rewrite <- Heqhi. trivial. lia. rewrite Zlength_map. lia. trivial. * rewrite <- upd_Znth_map. rewrite Zlength_upd_Znth. cancel. } { rewrite Zlength_upd_Znth. split. lia. split; trivial. split. lia. split. intros. unfold heap_size. rewrite Zlength_app in H2. rep_lia. generalize (Znth_nth_error _ _ H6); intro. rewrite <- Heqhi in H13. generalize (heapOrdered_raise_priority_weak_heapOrdered _ _ _ _ H1 _ _ H13 _ H12); intros. rewrite upd_Znth_update. 2: trivial. rewrite Heqnew_hi. rewrite H7 in H14. apply H14. } Intros vret. destruct vret as [heap_contents' lookup_contents']. Exists (fst h, heap_contents'). entailer!. + unfold heap_items. simpl snd. simpl fst in H15. symmetry in H15. transitivity (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)); trivial. replace (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) (heap_item_key hi, newpri, heap_item_payload hi)) with (update_pri_by_key (snd h) (heap_item_key hi) newpri). reflexivity. unfold update_pri_by_key. apply List_ext.list_eq_Znth; rewrite Zlength_map. { rewrite Zlength_upd_Znth. trivial. } intros. case (eq_dec i (Znth (heap_item_key hi) lookup_contents)); intro. - subst i. rewrite Znth_upd_Znth_same. 2,3: lia. rewrite Znth_map. 2: lia. change (snd h) with (heap_items h). rewrite <- Heqhi. unfold update_pri_if_key. case Z.eq_dec; auto. intro Hx; contradiction. - rewrite Znth_upd_Znth_diff; auto. rewrite Znth_map. 2: lia. unfold update_pri_if_key. case Z.eq_dec; intro; auto. destruct (H8 _ H7). unfold heap_items in H21. rewrite <- e in H21. lia. + unfold valid_pq. Exists arr junk lookup lookup_contents'. rewrite linked_heap_array_split. unfold heap_capacity, heap_size, heap_items. simpl fst in *. simpl snd in *. generalize H15; intro. apply Permutation_Zlength in H7. rewrite Zlength_upd_Znth in H7. unfold heap_items in H7. do 2 rewrite Zlength_app. rewrite H7. entailer!. split. { destruct H13. apply Permutation_Zlength in H13. rewrite <- H13. trivial. } split. { rewrite <- H7; unfold heap_items, heap_capacity in H2; rewrite <- H2; rewrite Zlength_app; trivial. } clear H17 H18 H10 H21 H11. destruct H13. split. eapply Permutation_NoDup; eauto. simpl. intros. destruct H3. generalize (H17 ((Zlength (heap_items h)) + i)); intro. spec H18. rewrite Zlength_app; rep_lia. destruct H18. rewrite app_Znth2 in H18, H21. 2,3: lia. replace (Zlength (heap_items h) + i - Zlength (heap_items h)) with i in * by lia. generalize H10; intro. apply Permutation_Zlength in H22. rewrite <- H22. split; trivial. rewrite <- H11. rewrite H21. apply Permutation_Zlength in H15. rewrite <- H15. rewrite Zlength_upd_Znth. lia. repeat intro. rename H24 into Hk. rename H21 into Hkk. apply Permutation_Znth in H15. 2: apply (0, Int.zero, Int.zero). rewrite Zlength_upd_Znth in H15. destruct H15 as [? [f [? [? ?]]]]. rewrite H25 in Hk. 2: lia. specialize (H17 (Z.of_nat (f (Z.to_nat j)))). spec H17. specialize (H21 (Z.to_nat j)). spec H21. lia. rewrite Zlength_app. lia. destruct H17. rewrite app_Znth1 in H17, H26. 2,3: specialize (H21 (Z.to_nat j)); lia. rewrite <- Znth_map in Hk. 2: rewrite Zlength_upd_Znth; specialize (H21 (Z.to_nat j)); lia. rewrite <- upd_Znth_map in Hk. unfold heap_item_key in Hk at 3; simpl in Hk. rewrite upd_Znth_map in Hk. rewrite Znth_map in Hk. 2: rewrite Zlength_upd_Znth; specialize (H21 (Z.to_nat j)); lia. clear PNarr PNlookup PNpq H16. replace (upd_Znth (Znth (heap_item_key hi) lookup_contents) (heap_items h) hi) with (heap_items h) in Hk. rewrite Hk in H26. rewrite Hkk in H26. specialize (H21 (Z.to_nat j)); lia. rewrite In_Znth_iff in H. destruct H as [spot [? ?]]. generalize (H8 spot); intro. spec H27. unfold proj_keys in H. rewrite Zlength_map in H. apply H. destruct H27. unfold proj_keys in H16. rewrite Znth_map in H16. 2: { unfold proj_keys in H. rewrite Zlength_map in H. rep_lia. } rewrite H16 in H28. rewrite H28. rewrite Heqhi. rewrite H28. rewrite upd_Znth_same_Znth. 2: lia. trivial. Time Qed. Lemma body_remove_min_nc: semax_body Vprog Gprog f_pq_remove_min_nc pq_remove_min_nc_spec. Proof. start_function. unfold valid_pq. Intros arr junk lookup lookup_contents. rename H0 into Hxx. rename H1 into H0. rename H2 into H1. rename H3 into H2. assert_PROP (linked_correctly (heap_items h ++ junk) lookup_contents). { unfold linked_heap_array. entailer!. } rename H3 into Hz. rewrite linked_heap_array_split. Intros. destruct h. destruct l. inversion H. unfold heap_items, heap_capacity, heap_size in *. simpl in H, H0, H1, Hz |-*. 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 linked_heap_array, heap_array, lookup_array. Intros. entailer!. } forward. { unfold linked_heap_array, heap_array, lookup_array. Intros. entailer!. } assert (Hl1: Zlength (root :: l) <= Int.max_unsigned). { simpl in H2. rewrite app_comm_cons in H2. rewrite Zlength_app in H2. rep_lia. } assert (Hl2: Zlength lookup_contents <= Int.max_unsigned) by (simpl in Hxx; rep_lia). forward_call (0, Zlength l, arr, root :: l, lookup, lookup_contents). { entailer!. simpl. congruence. } Intros lookup_contents'. forward. forward. unfold linked_heap_array at 1. unfold heap_array at 1. Intros. assert (Hl3: 0 <= Zlength (root :: l) - 1 <= Int.max_unsigned) by 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. rewrite <- Hx. rewrite Znth_Zexchange'; try lia. rewrite Znth_0_cons. unfold heap_item_rep. trivial. rewrite Zlength_Zexchange. lia. } forward. forward. forward. 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. } forward. forward. forward. forward. deadvars!. rewrite <- Hx. rewrite Znth_map. 2: rewrite Zlength_Zexchange; lia. rewrite Znth_Zexchange'; try lia. rewrite Znth_0_cons. change (data_at _ t_item _) with (data_at Tsh t_item (heap_item_rep root)). autorewrite with norm. rewrite <- Hx. 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, lookup, lookup_contents'); try rewrite Zlength_nil. { unfold linked_heap_array, heap_array. rewrite data_at_isptr. entailer. rewrite data_at_zero_array_eq; auto. entailer!. split. destruct H5; trivial. repeat intro. rewrite Zlength_nil in H15. lia. } { split. - apply hOwhO. apply cmp_po. apply heapOrdered_empty. - destruct H4. apply Permutation_Zlength in H. rep_lia. } Intro vret. destruct vret as [vret lookup_contents'']. Exists (n, vret) root. entailer. apply Permutation_nil in H7. simpl in H7. subst vret. clear Hy. unfold linked_heap_array. Intros. sep_apply harray_emp. rewrite emp_sepcon. rewrite Zlength_Zexchange. do 2 rewrite fold_heap_array. unfold valid_pq, hitem. apply andp_right. apply prop_right. auto. Exists arr (root :: junk) lookup lookup_contents''. simpl. unfold linked_heap_array. entailer!. 2: rewrite <- heap_array_split; apply derives_refl. split. { destruct H. apply Permutation_Zlength in H. simpl in H. rewrite <- H. destruct H4. apply Permutation_Zlength in H4. rewrite <- H4. trivial. } rewrite Zlength_nil in *. rewrite Zexchange_eq in *. simpl in Hz, H3, H6, H. change (root :: junk) with ([root] ++ junk). red. destruct H, H4. apply linked_correctly'_shuffle with lookup_contents'; trivial. apply linked_correctly_app3; trivial. apply linked_correctly'_shuffle with lookup_contents; trivial. + intros. rewrite H19; trivial. intros. rewrite Zlength_one in H21. assert (j = 0) by lia. subst j. change (Znth 0 [root]) with root. intro. clear -Hz H22 H20. destruct Hz. assert (0 <= 0 < Zlength (root :: junk)) by (rewrite Zlength_cons; rep_lia). destruct (H0 _ H1). assert (0 <= (1 + i0) < Zlength (root :: junk)) by (rewrite Zlength_cons; rep_lia). destruct (H0 _ H4). clear -H22 H3 H6 H20. rewrite Znth_0_cons, H22 in H3. change (root :: junk) with ([root] ++ junk) in H6. rewrite app_Znth2 in H6; rewrite Zlength_one in *. 2: lia. replace (1 + i0 - 1) with i0 in H6 by lia. rewrite H3 in H6. lia. + intros. rewrite H18; auto. rewrite Zlength_nil. lia. * destruct l0; inversion H. subst h0. assert (Zlength (h :: l) = Zlength (root :: l0)). { rewrite H8, Zlength_app, Zlength_one, Zlength_cons. lia. } rewrite H6, Zexchange_head_foot. rewrite fold_heap_array. sep_apply fold_linked_heap_array. { rewrite H8 in H5. replace (Zlength (l0 ++ [foot])) with (Zlength (root :: l0)) in H5 by congruence. rewrite app_comm_cons in H5. rewrite Zexchange_head_foot in H5. trivial. } rewrite linked_heap_array_split. Intros. forward_call (0, arr, (foot :: l0), Zlength (foot :: l0), lookup, lookup_contents'). { split3. - intros _. generalize (Zlength_nonneg junk); intro. simpl in H2. repeat rewrite Zlength_cons in *. rewrite Zlength_app in H2. lia. - apply weak_heapOrdered_root with root. rewrite H8, app_comm_cons in H1. apply heapOrdered_cutfoot in H1. trivial. - simpl in Hxx. destruct H4. apply Permutation_Zlength in H4. rep_lia. } Intros vret. destruct vret as [vret lookup_contents'']. Exists (n, vret) root. simpl fst. simpl snd. unfold hitem, heap_item_rep, heap_size, heap_capacity. entailer!. { split. constructor. rewrite H8. transitivity ([foot] ++ l0). apply Permutation_app_comm. destruct H4. auto. generalize (root_minimal _ _ _ _ H1 root eq_refl); intro. rewrite H8 in H16. apply Forall_inv_tail in H16. eapply forall_permutation. apply H16. transitivity ([foot] ++ l0). apply Permutation_app_comm. simpl. tauto. } unfold valid_pq. Exists arr (root :: junk) lookup lookup_contents''. unfold heap_size, heap_capacity. simpl. replace (Zlength vret) with (Zlength (root :: l0)). 2: { apply Permutation_Zlength in H11. trivial. } entailer!. { split. { destruct H9. apply Permutation_Zlength in H9. simpl in H9. rewrite <- H9. destruct H4. apply Permutation_Zlength in H4. rewrite <- H4. trivial. } simpl in *. rewrite <- H2. apply Permutation_Zlength in H11. autorewrite with sublist. rewrite <- H11. autorewrite with sublist in *. lia. } change (root :: junk) with ([root] ++ junk). rewrite app_assoc. do 2 rewrite linked_heap_array_split. generalize H11; intro Hq. apply Permutation_Zlength in H11. rewrite app_comm_cons. rewrite Zlength_app. rewrite H11. rewrite Zlength_app. assert (Zlength (root :: l0) = Zlength vret). { simpl in H11. rewrite <- H11. do 2 rewrite Zlength_cons. trivial. } do 3 rewrite app_comm_cons. do 4 rewrite Zlength_app. rewrite H16. do 2 rewrite Zlength_one. rewrite Zlength_cons. simpl fst in *. rewrite H8. replace (Z.succ (Zlength (l0 ++ [foot])) + Zlength junk) with (Zlength vret + 1 + Zlength junk). 2: { rewrite Zlength_app. rewrite <- H16. rewrite Zlength_cons, Zlength_one. rep_lia. } entailer!. simpl in *. clear H13 H14 H15. split. + apply linked_correctly'_shuffle with lookup_contents'; trivial. apply linked_correctly'_shuffle with lookup_contents; trivial. replace (Zlength vret + 1) with (Zlength (root :: h :: l)); trivial. rewrite <- H16. rewrite H8. do 2 rewrite Zlength_cons. rewrite Zlength_app, Zlength_one. lia. destruct H4; trivial. 2: destruct H9; trivial. - rewrite H8 in H4. replace (Zlength _) with (Zlength (root :: l0)) in H4. 2: rewrite Zlength_app, Zlength_cons, Zlength_one; lia. rewrite app_comm_cons in H4. rewrite Zexchange_head_foot in H4. eapply relink_tail. 3: apply H4. do 2 rewrite app_comm_cons in Hz. apply Hz. rewrite H8. transitivity (root :: (foot :: l0)). 2: apply Permutation_cons_append. constructor. transitivity ([foot] ++ l0). 2: reflexivity. apply Permutation_app_comm. - rewrite H8 in H5. replace (Zlength _) with (Zlength (root :: l0)) in H5. 2: rewrite Zlength_app, Zlength_cons, Zlength_one; lia. rewrite app_comm_cons in H5. rewrite Zexchange_head_foot in H5. intros. destruct H9. rewrite <- H14. trivial. repeat intro. destruct Hz. apply Permutation_Znth in Hq. 2: apply (0, Int.zero, Int.zero). destruct Hq as [? [f2 [? [? ?]]]]. rewrite H23 in H17. 2: lia. generalize (H19 (Zlength (root :: h :: l) + i0)); intro Hqq. spec Hqq. do 2 rewrite app_comm_cons. rewrite Zlength_app. lia. do 2 rewrite app_comm_cons in Hqq. rewrite app_Znth2 in Hqq. 2: lia. replace (Zlength (root :: h :: l) + i0 - Zlength (root :: h :: l)) with i0 in Hqq by lia. destruct Hqq. assert (Z.of_nat (f2 (Z.to_nat j)) = 0 \/ Z.of_nat (f2 (Z.to_nat j)) > 0) by lia. rewrite H8 in H25. destruct H26. ** rewrite H26, Znth_0_cons in H17. specialize (H19 (Zlength (h :: l))). spec H19. repeat rewrite Zlength_cons. rewrite Zlength_app. rep_lia. destruct H19. rewrite app_comm_cons, H8 in H27. rewrite app_comm_cons in H27. rewrite app_Znth1 in H27. 2: rewrite Zlength_cons; rep_lia. rewrite app_comm_cons in H27. rewrite app_Znth2 in H27. 2: rewrite Zlength_cons, Zlength_app, Zlength_one; rep_lia. replace (Zlength (l0 ++ [foot]) - Zlength (root :: l0)) with 0 in H27 by (rewrite Zlength_cons, Zlength_app, Zlength_one; rep_lia). change (Znth 0 [foot]) with foot in H27. rewrite H17 in H27. rewrite H25 in H27. autorewrite with sublist in H27. lia. ** specialize (H21 (Z.to_nat j)). spec H21. lia. specialize (H19 (Z.of_nat (f2 (Z.to_nat j)))). spec H19. { rewrite app_comm_cons, H8. rewrite Zlength_cons, Zlength_app. rewrite Zlength_app, Zlength_one. rewrite Zlength_cons in H21. lia. } do 2 rewrite app_comm_cons in H19. rewrite H8 in H19. rewrite app_Znth1 in H19. 2: autorewrite with sublist in *; rep_lia. rewrite app_comm_cons in H19. change (root :: l0) with ([root] ++ l0) in H19. rewrite <- app_assoc in H19. rewrite app_Znth2 in H19. 2: rewrite Zlength_one; rep_lia. change (foot :: l0) with ([foot] ++ l0) in H17. rewrite app_Znth2 in H17. 2: rewrite Zlength_one; lia. rewrite app_Znth1 in H19. 2: autorewrite with sublist in *; rep_lia. rewrite Zlength_one in H17. rewrite Zlength_one in H19. destruct H19. rewrite H17 in H27. rewrite H25 in H27. autorewrite with sublist in H27, H21. lia. + rewrite H8 in H5. replace (Zlength _) with (Zlength (root :: l0)) in H5. 2: rewrite Zlength_app, Zlength_cons, Zlength_one; lia. rewrite app_comm_cons in H5. rewrite Zexchange_head_foot in H5. split. { destruct H9. eapply Permutation_NoDup. apply H9. destruct H5. trivial. } intros. rewrite Zlength_one in H13. assert (i0 = 0) by lia. subst i0. subst loc. destruct H7. specialize (H14 _ H13). destruct H14. change (Znth 0 [root]) with root in *. destruct H9. split. { apply Permutation_Zlength in H9. lia. } destruct H5. generalize H18; intro Hqq. specialize (H18 (Zlength (foot :: l0))). spec H18. rewrite Zlength_app, Zlength_one. rep_lia. destruct H18. rewrite app_Znth2 in H19. 2: lia. replace (Zlength _ - Zlength _) with 0 in H19 by lia. change (Znth _ [root]) with root in H19. rewrite <- H17. lia. repeat intro. apply Permutation_Znth in Hq. 2: apply (0, Int.zero, Int.zero). destruct Hq as [? [f [? [? ?]]]]. specialize (Hqq (Z.of_nat (f (Z.to_nat j)))). spec Hqq. { rewrite Zlength_app, Zlength_one. specialize (H23 (Z.to_nat j)). lia. } destruct Hqq. rewrite app_Znth1 in H27. 2: specialize (H23 (Z.to_nat j)); lia. rewrite <- H25 in H27. 2: lia. rewrite H21 in H27. rewrite H19 in H27. specialize (H23 (Z.to_nat j)); lia. Time Qed. Lemma heap_item_rep_morph: forall x y, (fst (heap_item_rep x), (fst (snd (heap_item_rep y)), snd (snd (heap_item_rep x)))) = heap_item_rep (fst (fst x), snd (fst y), snd x). Proof. unfold heap_item_rep. destruct x,y; reflexivity. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.env_binary_heap_pro CertiGraph.binheap.spec_binary_heap_pro