proposition: Lemma In_update_pri_by_key: forall i L k np, In i (update_pri_by_key L k np) -> (In i L /\ heap_item_key i <> k) \/ (exists oi, In oi L /\ heap_item_key i = k /\ heap_item_payload i = heap_item_payload oi /\ heap_item_key i = heap_item_key oi /\ heap_item_priority i = np).
proof: Proof. intros. unfold update_pri_by_key in H. rewrite in_map_iff in H. destruct H as [oi [? ?]]. revert H. unfold update_pri_if_key. case Z.eq_dec; intros. 2: left; subst; auto. right. exists oi. split; trivial. subst i. unfold heap_item_key, heap_item_payload, heap_item_priority in *. simpl. tauto. 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