proposition: Lemma free_items: forall v size, data_at_ Tsh (tarray t_item size) v |-- data_at_ Tsh (tarray tint (sizeof (Tstruct _structItem noattr) * size / sizeof tint)) v.
proof: Proof. intros. saturate_local. sep_apply data_at__memory_block_cancel. rewrite <- memory_block_data_at_. simpl. rewrite Zaux.Zdiv_eucl_unique. rewrite simpl_size_t_item. apply derives_refl'. f_equal. lia. destruct H as [? [? [? [? ?]]]]. split3; auto. split3; auto. hnf in H1 |- *. destruct v; auto. simpl. simpl sizeof. rewrite Zaux.Zdiv_eucl_unique. rewrite simpl_size_t_item. simpl in H1. lia. hnf in H2 |- *. destruct v; auto. simpl sizeof. rewrite simpl_size_t_item. apply align_compatible_rec_Tarray; intros. assert (exists k, 0 <= k < size /\ (i0 = 3 * k + 0 \/ i0 = 3 * k + 1 \/ i0 = 3 * k + 2)). { exists (i0 / 3). generalize (Z_div_mod_eq i0 3); intro. spec H5. lia. generalize (Z.mod_pos_bound i0 3); intro. spec H6. lia. split. 2: lia. destruct H4. split. apply Z.div_pos; lia. apply Z.div_lt_upper_bound; lia. } destruct H5 as [k [? ?]]. eapply align_compatible_rec_Tarray_inv in H2. 2: apply H5. destruct H6 as [? | [? | ?]]; subst i0; [ eapply align_compatible_rec_Tstruct_inv with (i0 := _key) in H2 | eapply align_compatible_rec_Tstruct_inv with (i0 := _priority) in H2 | eapply align_compatible_rec_Tstruct_inv with (i0 := _data) in H2 ] ; try reflexivity; eapply align_compatible_rec_by_value; try reflexivity; eapply align_compatible_rec_by_value_inv in H2; try reflexivity; simpl in *; rewrite (Z.mul_add_distr_l 4), Z.mul_assoc, Z.add_assoc; simpl; apply H2. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel