proposition: Lemma Permutation_Znth {A : Type} `{iA: Inhabitant A}: forall (l l' : list A) (d : A), Permutation l l' <-> (let n := Zlength l in Zlength l' = n /\ (exists f : nat -> nat, FinFun.bFun (Z.to_nat n) f /\ FinFun.bInjective (Z.to_nat n) f /\ (forall z : Z, (0 <= z < n) -> Znth z l' = Znth (Z.of_nat (f (Z.to_nat z))) l))).
proof: Proof. intros. rewrite Permutation_nth. instantiate (1 := iA). do 2 rewrite Zlength_correct. split; intros; subst n; destruct H as [? [? [? [? ?]]]]; rename x into f. * split. congruence. exists f. rewrite Nat2Z.id. split; trivial. split; trivial. intros. repeat rewrite <- nth_Znth. 3: rewrite Zlength_correct; lia. rewrite H2. 2: rep_lia. rewrite Nat2Z.id. trivial. rewrite Zlength_correct. specialize (H0 (Z.to_nat z)). rep_lia. * split. rep_lia. exists f. rewrite Nat2Z.id in *. split; trivial. split; trivial. intros. specialize (H2 (Z.of_nat x)). do 2 rewrite <- nth_Znth in H2. repeat rewrite Nat2Z.id in *. apply H2. lia. 1,2,3: rewrite Zlength_correct. 2,3: lia. specialize (H0 x). rewrite Nat2Z.id. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model