proposition: Lemma find_item_by_key_update_pri_by_key: forall L k op v np, find_item_by_key L k = [(k, op, v)] -> find_item_by_key (update_pri_by_key L k np) k = [(k, np, v)].
proof: Proof. intros. unfold find_item_by_key, update_pri_by_key in *. rewrite filter_map_comm'. 2: { unfold update_pri_if_key. intros. destruct x as [[kk ?] ?]. unfold heap_item_key. simpl. case (Z.eq_dec kk); case (Z.eq_dec _ kk); simpl; case (Z.eq_dec _ k); simpl; intros; auto; exfalso; auto. } change (key_type * priority_type * payload_type)%type with heap_item. rewrite H. unfold update_pri_if_key, heap_item_key. simpl. case Z.eq_dec; trivial. destruct 1; 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