proposition: Lemma linked_correctly_Zexchange: forall L1 L2 j k, 0 <= j < Zlength L1 -> 0 <= k < Zlength L1 -> linked_correctly L1 L2 -> linked_correctly (Zexchange L1 j k) (Zexchange L2 (heap_item_key (Znth j L1)) (heap_item_key (Znth k L1))).
proof: Proof. repeat intro. destruct H1 as [Hz ?]. split. * eapply Permutation_NoDup. 2: apply Hz. apply Zexchange_Permutation. * intros. subst loc. rewrite Zlength_Zexchange in H2. rewrite Zlength_Zexchange. destruct (H1 _ H). destruct (H1 _ H0). destruct (H1 _ H2). clear H1. case (Z.eq_dec i j); intro. - subst j. rewrite Znth_Zexchange; auto. rewrite Znth_Zexchange'; auto. - case (Z.eq_dec i k); intro. + subst i. rewrite Znth_Zexchange'; auto. rewrite Znth_Zexchange; auto. + rewrite Znth_Zexchange''; auto. rewrite Znth_Zexchange''; auto. intro. rewrite H1 in H8. rewrite H4 in H8. lia. intro. rewrite H1 in H8. rewrite H6 in H8. 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