proposition: Lemma update_pri_by_key_split: forall h key newpri start xp xd rest, keys_valid h -> h = start ++ (key, xp, xd) :: rest -> update_pri_by_key h key newpri = start ++ (key, newpri, xd) :: rest.
proof: Proof. intros h key newpri start xp xd. revert h. induction start; intros; rewrite H0. * simpl in *. subst h. rewrite update_pri_by_key_not_In. f_equal. unfold update_pri_if_key. case Z.eq_dec. trivial. contradiction. intro. red in H. simpl in H. inversion H. contradiction. * subst h. simpl in H. generalize (keys_valid_tl _ _ H); intro. specialize (IHstart (start ++ (key, xp, xd) :: rest) rest H0 (eq_refl _)). simpl. rewrite IHstart. f_equal. unfold update_pri_if_key. case Z.eq_dec; auto. intro. inversion H. subst key. rewrite map_app in H3. exfalso. apply H3. apply in_or_app. right. left. 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