proposition: Lemma collect_Z_indices_spec: forall {A} {d: Inhabitant A} eqdec (target: A) (l: list A) (ind: Z) c, l = skipn (Z.to_nat ind) c -> 0 <= ind -> forall j, In j (collect_Z_indices eqdec target l ind) <-> ind <= j < Zlength c /\ Znth j c = target.
proof: Proof. intros. revert ind H H0 j. induction l; intros. - simpl. split; intros. 1: exfalso; assumption. pose proof (Zlength_skipn ind c). destruct H1. rewrite <- H, Zlength_nil, (Z.max_r _ _ H0) in H2. symmetry in H2. rewrite Z.max_l_iff in H2. lia. - assert (l = skipn (Z.to_nat (ind + 1)) c). { clear -H H0. rewrite Z2Nat.inj_add by lia. simpl Z.to_nat at 2. remember (Z.to_nat ind). clear ind Heqn H0. replace (n + 1)%nat with (S n) by lia. revert a l c H. induction n; intros; simpl in H; destruct c; [inversion H | | inversion H|]. - simpl. inversion H; reflexivity. - apply IHn in H. rewrite H. simpl. destruct c; reflexivity. } assert (0 <= ind + 1) by lia. specialize (IHl _ H1 H2). simpl. assert (Znth ind c = a). { clear -H H0. apply Z2Nat.id in H0. remember (Z.to_nat ind). rewrite <- H0. clear ind Heqn H0. revert a l c H. induction n; intros; simpl in H; destruct c; [inversion H | | inversion H|]. - simpl. inversion H. rewrite Znth_0_cons. reflexivity. - rewrite Nat2Z.inj_succ, Znth_pos_cons by lia. apply IHn in H. replace (Z.succ (Z.of_nat n) - 1) with (Z.of_nat n) by lia. assumption. } destruct (eqdec target a). + simpl. rewrite IHl. clear IHl. split; intros; destruct H4; [|intuition auto with *| ]. * subst j. split; [split|]; [lia | | rewrite <- e in H3; assumption]. pose proof (Zlength_skipn ind c). rewrite <- H in H4. rewrite Zlength_cons in H4. pose proof (Zlength_nonneg l). destruct (Z.max_spec 0 (Zlength c - Z.max 0 ind)). 2: exfalso; lia. destruct H6 as [? _]. rewrite Z.max_r in H6; lia. * assert (ind = j \/ ind + 1 <= j < Zlength c) by lia. destruct H6; [left | right; split]; assumption. + rewrite IHl; split; intros; destruct H4; split; [lia | assumption | | assumption]. assert (ind = j \/ ind + 1 <= j < Zlength c) by lia. clear H4. destruct H6. 2: assumption. exfalso; subst j. rewrite H5 in H3. rewrite H3 in n. apply n; reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen