proposition: Theorem arrayLookup_allNats_eq : forall (B : Set)(ls : list (nat * B)) i, fst (split ls) = allNatsLt (length ls) -> arrayLookup _ ls i = match nth_option ls i with | Some (_, v) => Some v | None => None end.
proof: Proof. induction ls using rev_ind; intuition; simpl in *. rewrite app_length in H. rewrite fst_split_app_eq in H. simpl in *. rewrite Nat.add_comm in H. simpl in *. eapply app_inj_tail in H. intuition. subst. case_eq (nth_option ls i); intuition. erewrite nth_option_app_Some ; eauto. destruct p. case_eq (arrayLookup nat_EqDec ls i); intuition. erewrite arrayLookup_app_Some; eauto. rewrite IHls. rewrite H. trivial. trivial. eapply arrayLookup_None_not_In in H1. intuition. rewrite H0. eapply allNatsLt_lt_if. eapply nth_option_Some_lt. eauto. rewrite nth_option_app_None. simpl. case_eq (i - length ls); intuition. eapply nth_option_None_ge in H. assert (i = length ls). lia. subst. case_eq (arrayLookup _ ls (length ls)); intuition. exfalso. eapply arrayLookup_Some_impl_In in H2. eapply in_split_l in H2. simpl in *. rewrite H0 in H2. eapply allNatsLt_lt in H2. lia. rewrite arrayLookup_app_None; eauto. simpl. rewrite eqb_refl. trivial. case_eq (arrayLookup _ ls i); intuition. eapply arrayLookup_Some_impl_In in H2. eapply in_split_l in H2. simpl in *. rewrite H0 in H2. eapply allNatsLt_lt in H2. lia. rewrite arrayLookup_app_None; eauto. simpl. case_eq ( eqb i (length ls)); intuition. rewrite eqb_leibniz in H3. subst. lia. trivial. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold