Mathlib.Data.List.Pairwise

Module docstring

{"# Pairwise relations on a list

This file provides basic results about List.Pairwise and List.pwFilter (definitions are in Data.List.Defs). 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 ","### Pairwise filtering "}

List.Pairwise.forall_of_forall theorem

 (H : Symmetric R) (H₁ : ∀ x ∈ l, R x x) (H₂ : l.Pairwise R) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y

Full source

theorem Pairwise.forall_of_forall (H : Symmetric R) (H₁ : ∀ x ∈ l, R x x) (H₂ : l.Pairwise R) :
    ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y :=
  H₂.forall_of_forall_of_flip H₁ <| by rwa [H.flip_eq]

Reflexive and Pairwise Relations Imply Universal Relation on List

Informal description

Let $R$ be a symmetric relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. Suppose that: 1. $R$ is reflexive on $l$, i.e., $R(x, x)$ holds for every $x \in l$. 2. The list $l$ is pairwise $R$-related, meaning that for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds. Then for any two elements $x$ and $y$ in $l$ (not necessarily distinct), $R(x, y)$ holds.

List.Pairwise.forall theorem

(hR : Symmetric R) (hl : l.Pairwise R) : ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b

Full source

theorem Pairwise.forall (hR : Symmetric R) (hl : l.Pairwise R) :
    ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b := by
  apply Pairwise.forall_of_forall
  · exact fun a b h hne => hR (h hne.symm)
  · exact fun _ _ hx => (hx rfl).elim
  · exact hl.imp (@fun a b h _ => by exact h)

Pairwise List Implies Relation for All Distinct Pairs

Informal description

Let $R$ be a symmetric relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$, then for any two distinct elements $a$ and $b$ in $l$, the relation $R(a, b)$ holds.

List.Pairwise.set_pairwise theorem

(hl : Pairwise R l) (hr : Symmetric R) : {x | x ∈ l}.Pairwise R

Full source

theorem Pairwise.set_pairwise (hl : Pairwise R l) (hr : Symmetric R) : { x | x ∈ l }.Pairwise R :=
  hl.forall hr

Pairwise List Implies Pairwise Set for Symmetric Relation

Informal description

Let $R$ be a symmetric binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds), then the set $\{x \mid x \in l\}$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in this set, $R(x, y)$ holds).

List.pairwise_of_reflexive_of_forall_ne theorem

(hr : Reflexive R) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) : l.Pairwise R

Full source

theorem pairwise_of_reflexive_of_forall_ne (hr : Reflexive R)
    (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) : l.Pairwise R := by
  rw [pairwise_iff_forall_sublist]
  intro a b hab
  if heq : a = b then
    cases heq; apply hr
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq

Pairwise List from Reflexive Relation and Distinct Pair Condition

Informal description

Let $R$ be a reflexive binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If for every pair of distinct elements $a, b \in l$ the relation $R(a, b)$ holds, then the list $l$ is pairwise with respect to $R$.

List.Pairwise.rel_head_tail theorem

(h₁ : l.Pairwise R) (ha : a ∈ l.tail) : R (l.head <| ne_nil_of_mem <| mem_of_mem_tail ha) a

Full source

theorem Pairwise.rel_head_tail (h₁ : l.Pairwise R) (ha : a ∈ l.tail) :
    R (l.head <| ne_nil_of_mem <| mem_of_mem_tail ha) a := by
  cases l with
  | nil => simp at ha
  | cons b l => exact (pairwise_cons.1 h₁).1 a ha

Pairwise relation between head and tail elements

Informal description

Let $R$ be a binary relation on a type $\alpha$, and let $l$ be a non-empty list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds), and $a$ is an element in the tail of $l$, then $R$ holds between the head of $l$ and $a$.

List.Pairwise.rel_head_of_rel_head_head theorem

 (h₁ : l.Pairwise R) (ha : a ∈ l) (hhead : R (l.head <| ne_nil_of_mem ha) (l.head <| ne_nil_of_mem ha)) :
  R (l.head <| ne_nil_of_mem ha) a

Full source

theorem Pairwise.rel_head_of_rel_head_head (h₁ : l.Pairwise R) (ha : a ∈ l)
    (hhead : R (l.head <| ne_nil_of_mem ha) (l.head <| ne_nil_of_mem ha)) :
    R (l.head <| ne_nil_of_mem ha) a := by
  cases l with
  | nil => simp at ha
  | cons b l => exact (mem_cons.mp ha).elim (· ▸ hhead) ((pairwise_cons.1 h₁).1 _)

Relation Between Head and Element in Pairwise List

Informal description

Let $R$ be a binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. Suppose that: 1. The list $l$ is pairwise $R$, meaning that for any two distinct elements $x$ and $y$ in $l$ where $x$ appears before $y$, the relation $R(x, y)$ holds. 2. The element $a$ is in the list $l$. 3. The relation $R$ holds between the head of $l$ (assuming $l$ is non-empty) and itself. Then, the relation $R$ holds between the head of $l$ and the element $a$.

List.Pairwise.rel_head theorem

[IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) : R (l.head <| ne_nil_of_mem ha) a

Full source

theorem Pairwise.rel_head [IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) :
    R (l.head <| ne_nil_of_mem ha) a :=
  h₁.rel_head_of_rel_head_head ha (refl_of ..)

Pairwise Relation Between Head and Any Element in Reflexive Context

Informal description

Let $R$ be a reflexive binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ where $x$ appears before $y$, the relation $R(x, y)$ holds), and $a$ is an element of $l$, then $R$ holds between the head of $l$ (assuming $l$ is non-empty) and $a$.

List.Pairwise.rel_dropLast_getLast theorem

(h : l.Pairwise R) (ha : a ∈ l.dropLast) : R a (l.getLast <| ne_nil_of_mem <| dropLast_subset _ ha)

Full source

theorem Pairwise.rel_dropLast_getLast (h : l.Pairwise R) (ha : a ∈ l.dropLast) :
    R a (l.getLast <| ne_nil_of_mem <| dropLast_subset _ ha) := by
  rw [← pairwise_reverse] at h
  rw [getLast_eq_head_reverse]
  exact h.rel_head_tail (by rwa [tail_reverse, mem_reverse])

Pairwise Relation Between Elements and Last Element in Dropped List

Informal description

Let $R$ be a binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds), and $a$ is an element in the list obtained by removing the last element of $l$, then $R$ holds between $a$ and the last element of $l$.

List.Pairwise.rel_getLast_of_rel_getLast_getLast theorem

 (h₁ : l.Pairwise R) (ha : a ∈ l) (hlast : R (l.getLast <| ne_nil_of_mem ha) (l.getLast <| ne_nil_of_mem ha)) :
  R a (l.getLast <| ne_nil_of_mem ha)

Full source

theorem Pairwise.rel_getLast_of_rel_getLast_getLast (h₁ : l.Pairwise R) (ha : a ∈ l)
    (hlast : R (l.getLast <| ne_nil_of_mem ha) (l.getLast <| ne_nil_of_mem ha)) :
    R a (l.getLast <| ne_nil_of_mem ha) := by
  rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha
  exact ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

Pairwise Relation Between Elements and Last Element Given Reflexivity at Last Element

Informal description

Let $R$ be a binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds), $a$ is an element of $l$, and $R$ holds between the last element of $l$ and itself, then $R$ holds between $a$ and the last element of $l$.

List.Pairwise.rel_getLast theorem

[IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) : R a (l.getLast <| ne_nil_of_mem ha)

Full source

theorem Pairwise.rel_getLast [IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) :
    R a (l.getLast <| ne_nil_of_mem ha) :=
  h₁.rel_getLast_of_rel_getLast_getLast ha (refl_of ..)

Pairwise Relation Between Elements and Last Element in Reflexive Context

Informal description

Let $R$ be a reflexive binary relation on a type $\alpha$, and let $l$ be a list of elements of $\alpha$. If $l$ is pairwise with respect to $R$ (i.e., for any two distinct elements $x$ and $y$ in $l$ appearing in order, $R(x, y)$ holds), and $a$ is an element of $l$, then $R$ holds between $a$ and the last element of $l$.