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' ∈ l → R 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} : List.Pairwise R l → List.Pairwise R (List.drop n l)

theorem List.Pairwise.imp_of_mem {α : Type u_1} {l : List α} {R : α → α → Prop} {S : α → α → Prop} (H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) (p : List.Pairwise R l) : List.Pairwise S l

theorem List.Pairwise.and : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop}, List.Pairwise R l → List.Pairwise S l → List.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 b → S a b → T a b) → List.Pairwise R l → List.Pairwise S l → List.Pairwise T l

theorem List.Pairwise.iff_of_mem {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} {l : List α} (H : ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)) : List.Pairwise R l ↔ List.Pairwise S l

theorem List.Pairwise.iff {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} (H : ∀ (a b : α), R a b ↔ S a b) {l : List α} : List.Pairwise R l ↔ List.Pairwise S l

theorem List.pairwise_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} (H : ∀ (x y : α), R x y) : List.Pairwise R l

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 ∈ l → y ∈ l → R x y) l

theorem List.Pairwise.forall_of_forall_of_flip : ∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, (∀ (x : α), x ∈ l → R x x) → List.Pairwise R l → List.Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y

theorem List.pairwise_singleton {α : Type u_1} (R : α → α → Prop) (a : α) : List.Pairwise R [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 y → R 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 y → R 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)) : List.Pairwise R l

theorem List.Pairwise.map {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) (p : List.Pairwise R l) : List.Pairwise S (List.map f 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) : List.Pairwise S (List.filterMap f 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 x → p y → R x y) l

theorem List.Pairwise.filter {α : Type u_1} {R : α → α → Prop} {l : List α} (p : α → Bool) : List.Pairwise R l → List.Pairwise R (List.filter p l)

theorem List.pairwise_join {α : Type u_1} {R : α → α → Prop} {L : List (List α)} : List.Pairwise R L.join ↔ (∀ (l : List α), l ∈ L → List.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 ∈ l → List.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 l → R 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 l → r a a) (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b) : List.Pairwise r l

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 < j → R (l.get i) (l.get j)

theorem List.pairwise_replicate {α : Type u_1} {r : α → α → Prop} {x : α} (hx : r x x) (n : Nat) : List.Pairwise r (List.replicate n x)

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 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