proposition: Lemma find_item_by_key_finds_item: forall h item, In item h -> NoDup (map heap_item_key h) -> find_item_by_key h (heap_item_key item) = [item].
proof: Proof. intros. unfold find_item_by_key. induction h; [inversion H|]. destruct H. - subst a. simpl. destruct (Z.eq_dec (heap_item_key item) (heap_item_key item)). 2: exfalso; apply n; trivial. simpl. simpl in H0. apply NoDup_cons_2 in H0. replace (filter (fun item0 : heap_item => Z.eq_dec (heap_item_key item0) (heap_item_key item)) h) with (@nil heap_item); trivial. rewrite filter_false_nil; trivial. intros. rewrite <- not_true_iff_false. intro. apply (in_map heap_item_key) in H. replace (heap_item_key a) with (heap_item_key item) in H. apply H0; trivial. destruct (Z.eq_dec (heap_item_key a) (heap_item_key item)). + lia. + simpl in H1. inversion H1. - simpl. destruct (Z.eq_dec (heap_item_key a) (heap_item_key item)). + exfalso. simpl in H0. apply NoDup_cons_2 in H0. apply H0. rewrite e. apply in_map; trivial. + simpl. apply IHh; trivial. simpl in H0. apply (NoDup_cons_1 _ (heap_item_key a)); 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