Documentation

Batteries.Data.List.Pairwise

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.rel_of_pairwise_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)∀ {a' : α}, a' lR a a'
theorem List.Pairwise.of_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)List.Pairwise R l
theorem List.Pairwise.tail {α : Type u_1} {R : ααProp} {l : List α} (_p : List.Pairwise R l) :
List.Pairwise R l.tail
theorem List.Pairwise.drop {α : Type u_1} {R : ααProp} {l : List α} {n : Nat} :
theorem List.Pairwise.imp_of_mem {α : Type u_1} {l : List α} {R : ααProp} {S : ααProp} (H : ∀ {a b : α}, a lb lR a bS a b) (p : List.Pairwise R l) :
theorem List.Pairwise.and :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise R lList.Pairwise S lList.Pairwise (fun (a b : α) => R a b S a b) l
theorem List.pairwise_and_iff :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise (fun (a b : α) => R a b S a b) l List.Pairwise R l List.Pairwise S l
theorem List.Pairwise.imp₂ :
∀ {α : Type u_1} {R S T : ααProp} {l : List α}, (∀ (a b : α), R a bS a bT a b)List.Pairwise R lList.Pairwise S lList.Pairwise T l
theorem List.Pairwise.iff_of_mem {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} (H : ∀ {a b : α}, a lb l(R a b S a b)) :
theorem List.Pairwise.iff {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a b S a b) {l : List α} :
theorem List.pairwise_of_forall {α : Type u_1} {R : ααProp} {l : List α} (H : ∀ (x y : α), R x y) :
theorem List.Pairwise.and_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise R l List.Pairwise (fun (x y : α) => x l y l R x y) l
theorem List.Pairwise.imp_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise R l List.Pairwise (fun (x y : α) => x ly lR x y) l
theorem List.Pairwise.forall_of_forall_of_flip :
∀ {α : Type u_1} {l : List α} {R : ααProp}, (∀ (x : α), x lR x x)List.Pairwise R lList.Pairwise (flip R) l∀ ⦃x : α⦄, x l∀ ⦃y : α⦄, y lR x y
theorem List.pairwise_singleton {α : Type u_1} (R : ααProp) (a : α) :
theorem List.pairwise_pair {α : Type u_1} {R : ααProp} {a : α} {b : α} :
List.Pairwise R [a, b] R a b
theorem List.pairwise_append_comm {α : Type u_1} {R : ααProp} (s : ∀ {x y : α}, R x yR y x) {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ l₂) List.Pairwise R (l₂ ++ l₁)
theorem List.pairwise_middle {α : Type u_1} {R : ααProp} (s : ∀ {x y : α}, R x yR y x) {a : α} {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ a :: l₂) List.Pairwise R (a :: (l₁ ++ l₂))
theorem List.Pairwise.of_map {β : Type u_1} {α : Type u_2} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : ∀ (a b : α), S (f a) (f b)R a b) (p : List.Pairwise S (List.map f l)) :
theorem List.Pairwise.map {β : Type u_1} {α : Type u_2} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : ∀ (a b : α), R a bS (f a) (f b)) (p : List.Pairwise R l) :
theorem List.pairwise_filterMap {β : Type u_1} {α : Type u_2} {R : ααProp} (f : βOption α) {l : List β} :
List.Pairwise R (List.filterMap f l) List.Pairwise (fun (a a' : β) => ∀ (b : α), b f a∀ (b' : α), b' f a'R b b') l
theorem List.Pairwise.filter_map {β : Type u_1} {α : Type u_2} {R : ααProp} {S : ββProp} (f : αOption β) (H : ∀ (a a' : α), R a a'∀ (b : β), b f a∀ (b' : β), b' f a'S b b') {l : List α} (p : List.Pairwise R l) :
theorem List.pairwise_filter {α : Type u_1} {R : ααProp} (p : αProp) [DecidablePred p] {l : List α} :
List.Pairwise R (List.filter (fun (b : α) => decide (p b)) l) List.Pairwise (fun (x y : α) => p xp yR x y) l
theorem List.Pairwise.filter {α : Type u_1} {R : ααProp} {l : List α} (p : αBool) :
theorem List.pairwise_join {α : Type u_1} {R : ααProp} {L : List (List α)} :
List.Pairwise R L.join (∀ (l : List α), l LList.Pairwise R l) List.Pairwise (fun (l₁ l₂ : List α) => ∀ (x : α), x l₁∀ (y : α), y l₂R x y) L
theorem List.pairwise_bind {β : Type u_1} {α : Type u_2} {R : ββProp} {l : List α} {f : αList β} :
List.Pairwise R (l.bind f) (∀ (a : α), a lList.Pairwise R (f a)) List.Pairwise (fun (a₁ a₂ : α) => ∀ (x : β), x f a₁∀ (y : β), y f a₂R x y) l
theorem List.pairwise_iff_forall_sublist :
∀ {α : Type u_1} {l : List α} {R : ααProp}, List.Pairwise R l ∀ {a b : α}, [a, b].Sublist lR a b
@[deprecated List.pairwise_iff_forall_sublist]
theorem List.pairwise_of_reflexive_on_dupl_of_forall_ne {α : Type u_1} [DecidableEq α] {l : List α} {r : ααProp} (hr : ∀ (a : α), 1 < List.count a lr a a) (h : ∀ (a : α), a l∀ (b : α), b la br a b) :
theorem List.map_get_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun (x x_1 : Fin l.length) => x < x_1) is) :
(List.map l.get is).Sublist l

given a list is of monotonically increasing indices into l, getting each index produces a sublist of l.

theorem List.sublist_eq_map_get :
∀ {α : Type u_1} {l' l : List α}, l'.Sublist l∃ (is : List (Fin l.length)), l' = List.map l.get is List.Pairwise (fun (x x_1 : Fin l.length) => x < x_1) is

given a sublist l' <+ l, there exists a list of indices is such that l' = map (get l) is.

theorem List.pairwise_iff_get :
∀ {α : Type u_1} {R : ααProp} {l : List α}, List.Pairwise R l ∀ (i j : Fin l.length), i < jR (l.get i) (l.get j)
theorem List.pairwise_replicate {α : Type u_1} {r : ααProp} {x : α} (hx : r x x) (n : Nat) :

Pairwise filtering #

@[simp]
theorem List.pwFilter_nil :
∀ {α : Type u_1} {R : ααProp} [inst : 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 lR a b) :
@[simp]
theorem List.pwFilter_cons_of_neg {α : Type u_1} {R : ααProp} [DecidableRel R] {a : α} {l : List α} (h : ¬∀ (b : α), b List.pwFilter R lR a b) :
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 α) :
theorem List.pairwise_pwFilter {α : Type u_1} {R : ααProp} [DecidableRel R] (l : List α) :
theorem List.pwFilter_eq_self {α : Type u_1} {R : ααProp} [DecidableRel R] {l : List α} :
@[simp]
theorem List.pwFilter_idem {α : Type u_1} {R : ααProp} {l : List α} [DecidableRel R] :
theorem List.forall_mem_pwFilter {α : Type u_1} {R : ααProp} [DecidableRel R] (neg_trans : ∀ {x y z : α}, R x zR x y R y z) (a : α) (l : List α) :
(∀ (b : α), b List.pwFilter R lR a b) ∀ (b : α), b lR a b