Pairwise relations on a list #
This file provides basic results about
List.pwFilter (definitions are in
Pairwise r [a 0, ..., a (n - 1)] means
∀ i j, i < j → r (a i) (a j). For example,
Pairwise (≠) l means that all elements of
l are distinct, and
Pairwise (<) l means that
is strictly increasing.
pwFilter r l is the list obtained by iteratively adding each element of
l that doesn't break
the pairwiseness of the list we have so far. It thus yields
l' a maximal sublist of
l such that
Pairwise r l'.