proposition: Lemma valid_pq_NoDup: forall p h, valid_pq p h |-- !! NoDup (heap_items h).
proof: Proof. intros. unfold valid_pq, linked_heap_array, linked_correctly, linked_correctly'. Intros arr junk lookup lookup'. entailer!. clear H5 H6. apply NoDup_nth_error. rewrite NoDup_nth_error in H3. intros. rewrite <- (Nat2Z.id i) in H6. rewrite Znth_nth_error in H6. 2: rewrite Zlength_correct; rep_lia. remember (nth_error (heap_items h) j). destruct o. 2: discriminate. assert (j < length (heap_items h))%nat. { eapply nth_error_Some. intro. congruence. } assert (0 <= Z.of_nat j < Zlength (heap_items h)) by (rewrite Zlength_correct; lia). rewrite <- (Nat2Z.id j) in Heqo. rewrite Znth_nth_error in Heqo; auto. inversion Heqo. subst h0. clear Heqo. inversion H6. clear H6. generalize (H4 (Z.of_nat i)); generalize (H4 (Z.of_nat j)); intros. clear H4. rewrite Zlength_app in *. spec H6. rep_lia. spec H9. rewrite Zlength_correct; rep_lia. rewrite Znth_app1 in H6. 2: lia. rewrite Znth_app1 in H9. 2: rewrite Zlength_correct; lia. destruct H6, H9. rewrite H10 in H11. rewrite H11 in H6. lia. 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