proposition: Lemma free_pq: forall v, (data_at_ Tsh t_pq v) |-- (data_at_ Tsh (tarray tint (sizeof (Tstruct _structPQ noattr) / sizeof tint)) v).
proof: Proof. intro. saturate_local. sep_apply data_at__memory_block_cancel. rewrite <- memory_block_data_at_. apply derives_refl. destruct H as [? [? [? [? ?]]]]. split3; auto. split3; auto. hnf in H2 |- *. destruct v; auto. unfold t_pq in H2. apply align_compatible_rec_Tarray; intros. apply align_compatible_rec_by_value with (ch := Mint32); auto. simpl. apply Z.divide_add_r. 2: apply Z.divide_factor_l. eapply align_compatible_rec_Tstruct_inv with (i0 := _capacity) in H2; [|reflexivity..]. eapply align_compatible_rec_by_value_inv in H2; [|reflexivity]. simpl in H2. now rewrite Z.add_0_r in 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