Pairwise relations on a list #
This file provides basic results about List.Pairwise and List.pwFilter (definitions are in
Batteries.Data.List.Basic).
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 l
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'.
Tags #
sorted, nodup
Pairwise #
theorem
List.pairwise_iff_get
{α✝ : Type u_1}
{R : α✝ → α✝ → Prop}
{l : List α✝}
:
List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
Pairwise filtering #
@[simp]
theorem
List.pwFilter_nil
{α✝ : Type u_1}
{R : α✝ → α✝ → Prop}
[DecidableRel R]
:
List.pwFilter R [] = []
@[simp]
theorem
List.pwFilter_cons_of_pos
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
{a : α}
{l : List α}
(h : ∀ (b : α), b ∈ List.pwFilter R l → R a b)
:
List.pwFilter R (a :: l) = a :: List.pwFilter R l
@[simp]
theorem
List.pwFilter_cons_of_neg
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
{a : α}
{l : List α}
(h : ¬∀ (b : α), b ∈ List.pwFilter R l → R a b)
:
List.pwFilter R (a :: l) = List.pwFilter R l
theorem
List.pwFilter_map
{α : Type u_1}
{R : α → α → Prop}
{β : Type u_2}
[DecidableRel R]
(f : β → α)
(l : List β)
:
List.pwFilter R (List.map f l) = List.map f (List.pwFilter (fun (x y : β) => R (f x) (f y)) l)
theorem
List.pwFilter_sublist
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
(List.pwFilter R l).Sublist l
theorem
List.pwFilter_subset
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
List.pwFilter R l ⊆ l
theorem
List.pairwise_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
List.Pairwise R (List.pwFilter R l)
theorem
List.pwFilter_eq_self
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
{l : List α}
:
List.pwFilter R l = l ↔ List.Pairwise R l
@[simp]
theorem
List.pwFilter_idem
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
[DecidableRel R]
:
List.pwFilter R (List.pwFilter R l) = List.pwFilter R l
theorem
List.forall_mem_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z)
(a : α)
(l : List α)
:
(∀ (b : α), b ∈ List.pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b