NoDup List Cut Function

Proposal

The current List module provides a collection of functions to manipulate lists that satisfy the NoDup predicate. While this module contains a number of functions for removing elements from these lists it does not provide the following natural function:

Lemma NoDup_cut : forall (l : list A) (x : A),
  NoDup l ->
  {y : (list A) * (list A) | l = (fst y) ++ (x :: (snd y))}.

This function takes a list that does not contain any duplicates and effectively cuts the list at a given element.

Given this function a number of functions and lemmas about the effects of deleting elements from such lists follow immediately, and the NoDup_remove* functions can be composed very nicely with this function.

This function fills an important gap in the current module. All of the NoDup_remove* functions assume that the given list can be decomposed into the form xs ++ y :: ys. For example:

Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l').

But, the current module does not provide a function to perform this decomposition. The proposed function fills this gap.

I have already written this function for my personal use and will happily submit it for inclusion into the StdLibrary if the maintainers agree that it will be a useful addition. Please let me know if this is the case and I will submit a PR.

Thanks

• Larry

Start by locating the NoDup list module and its existing NoDup_remove* functions. Implement the proposed NoDup_cut decomposition there, then verify that it supports the stated removal lemmas and the required list equality.