proposition: Lemma can_split: forall (h: heap) (key: key_type), (~In key (map heap_item_key (heap_items h))) \/ exists start xp xd rest, (heap_items h) = start ++ (key, xp, xd) :: rest.
proof: Proof. destruct h. simpl. induction l. left. intro. inversion H. intro key. case (Z.eq_dec key (heap_item_key a)); intro. * right. destruct a as [[? ?] ?]. unfold heap_item_key in e. simpl in e. subst k. exists nil, p, p0, l. trivial. * specialize (IHl key). destruct IHl. left. intro. apply H. simpl in H0. destruct H0; [symmetry in H0|]; contradiction. destruct H as [start [xp [xd [rest ?]]]]. right. exists (a :: start), xp, xd, rest. rewrite H. trivial. 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