proposition: Lemma free_lookup: forall v size, data_at_ Tsh (tarray tuint size) v |-- data_at_ Tsh (tarray tint (sizeof tint * 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 (Z.mul_comm _ size), Z_div_mult; trivial. lia. destruct H as [? [? [? [? ?]]]]. split3; auto. split3; auto. hnf in H1 |- *. destruct v; auto. simpl. rewrite Zaux.Zdiv_eucl_unique. rewrite (Z.mul_comm _ size), Z_div_mult; trivial. lia. hnf in H2 |- *. destruct v; auto. simpl sizeof. rewrite (Z.mul_comm _ size), Z_div_mult. 2: lia. apply align_compatible_rec_Tarray; intros. eapply align_compatible_rec_Tarray_inv in H2. 2: apply H4. eapply align_compatible_rec_by_value; try reflexivity. eapply align_compatible_rec_by_value_inv in H2. apply H2. reflexivity. 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