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 α✝} : 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] : pwFilter R [] = []

@[simp]

theorem List.pwFilter_cons_of_pos {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} {l : List α} (h : ∀ (b : α), b ∈ pwFilter R l → R a b) : pwFilter R (a :: l) = a :: pwFilter R l

@[simp]

theorem List.pwFilter_cons_of_neg {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} {l : List α} (h : ¬∀ (b : α), b ∈ pwFilter R l → R a b) : pwFilter R (a :: l) = pwFilter R l

theorem List.pwFilter_map {α : Type u_1} {R : α → α → Prop} {β : Type u_2} [DecidableRel R] (f : β → α) (l : List β) : pwFilter R (map f l) = map f (pwFilter (fun (x y : β) => R (f x) (f y)) l)

theorem List.pwFilter_sublist {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) : (pwFilter R l).Sublist l

theorem List.pwFilter_subset {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) : pwFilter R l ⊆ l

theorem List.pairwise_pwFilter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) : Pairwise R (pwFilter R l)

theorem List.pwFilter_eq_self {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {l : List α} : pwFilter R l = l ↔ Pairwise R l

@[simp]

theorem List.pwFilter_idem {α : Type u_1} {R : α → α → Prop} {l : List α} [DecidableRel R] : pwFilter R (pwFilter R l) = 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 ∈ pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b