proposition: Lemma find_index_gen: forall (l: list Z) i ans, 0 <= i < Zlength l -> ~ In (Znth i l) (sublist 0 i l) -> find l (Znth i l) ans = i + ans.
proof: Proof. intros. generalize dependent i. generalize dependent ans. induction l. 1: intros; rewrite Zlength_nil in H; exfalso; lia. unfold find. intros. destruct (Z_EqDec a (Znth i (a :: l))). - rewrite <- e in H0. clear - H H0. destruct (Z.eq_dec 0 i). 1: lia. destruct H. assert (0 < i) by lia. exfalso. apply H0. unfold sublist. replace (i-0) with i by lia. simpl. replace (Z.to_nat i) with (Z.to_nat (Z.succ (i-1))) by rep_lia. rewrite Z2Nat.inj_succ by lia. rewrite firstn_cons. simpl; left; trivial. - destruct (Z.eq_dec 0 i). 1: rewrite <- e in c; rewrite Znth_0_cons in c; exfalso. apply c. reflexivity. assert (0 <= i - 1 < Zlength l) by (rewrite Zlength_cons in H; rep_lia). assert (~ In (Znth (i - 1) l) (sublist 0 (i - 1) l)). { rewrite <- (Znth_pos_cons i l a) by lia. rewrite <- (sublist_1_cons l a i). intro. apply H0. apply (sublist_In 1 i). rewrite sublist_sublist0 by lia. assumption. } pose proof (IHl (1 + ans) (i - 1) H1 H2). replace (i - 1 + (1 + ans)) with (i + ans) in H3 by lia. replace (Znth i (a :: l)) with (Znth (i - 1) l). 2: { symmetry. apply Znth_pos_cons; lia. } rewrite <- H3. unfold find. trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext