Init.Data.List.Nat.Pairwise

Module docstring

{"# Lemmas about List.Pairwise "}

List.map_getElem_sublist theorem

{l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) : is.map (l[·]) <+ l

Full source

/-- Given a list `is` of monotonically increasing indices into `l`, getting each index
  produces a sublist of `l`.  -/
theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) :
    is.map (l[·]) <+ l := by
  suffices ∀ j l', l' = l.drop j → (∀ i ∈ is, j ≤ i) → mapmap (l[·]) is <+ l'
    from this 0 l (by simp) (by simp)
  rintro j l' rfl his
  induction is generalizing j with
  | nil => simp
  | cons hd tl IH =>
    simp only [Fin.getElem_fin, map_cons]
    have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1
    specialize his hd (.head _)
    have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
    have := Sublist.append (nil_sublist (take hd l |>.drop j)) this
    rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
    simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]

Sublist Property of Mapped Increasing Indices: $\text{map}\ (l[\cdot])\ i_s <+ l$ for pairwise-increasing $i_s$

Informal description

For any list $l$ of elements of type $\alpha$ and any list $i_s$ of indices into $l$ (where each index is of type $\mathrm{Fin}\,l.\mathrm{length}$), if the indices in $i_s$ are strictly increasing (i.e., $i_s$ satisfies the pairwise relation $<$), then the sublist of $l$ obtained by mapping each index in $i_s$ to its corresponding element in $l$ is a sublist of $l$.

List.sublist_eq_map_getElem theorem

{l l' : List α} (h : l' <+ l) : ∃ is : List (Fin l.length), l' = is.map (l[·]) ∧ is.Pairwise (· < ·)

Full source

/-- Given a sublist `l' <+ l`, there exists an increasing list of indices `is` such that
  `l' = is.map fun i => l[i]`. -/
theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (Fin l.length),
    l' = is.map (l[·]) ∧ is.Pairwise (· < ·) := by
  induction h with
  | slnil => exact ⟨[], by simp⟩
  | cons _ _ IH =>
    let ⟨is, IH⟩ := IH
    refine ⟨is.map (·.succ), ?_⟩
    simpa [Function.comp_def, pairwise_map]
  | cons₂ _ _ IH =>
    rcases IH with ⟨is,IH⟩
    refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
    simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']

Sublist Characterization via Increasing Indices

Informal description

For any lists $l$ and $l'$ of elements of type $\alpha$, if $l'$ is a sublist of $l$ (denoted $l' <+ l$), then there exists a list of indices $i_s$ (each of type $\mathrm{Fin}\,l.\mathrm{length}$) such that $l'$ is equal to the list obtained by mapping each index in $i_s$ to its corresponding element in $l$, and the indices in $i_s$ are strictly increasing (i.e., $i_s$ is pairwise with respect to $<$).

List.pairwise_iff_getElem theorem

: Pairwise R l ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j]

Full source

theorem pairwise_iff_getElem : PairwisePairwise R l ↔
    ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
  rw [pairwise_iff_forall_sublist]
  constructor <;> intro h
  · intros i j hi hj h'
    apply h
    simpa [h'] using map_getElem_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
  · intros a b h'
    have ⟨is, h', hij⟩ := sublist_eq_map_getElem h'
    rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
    rcases h' with ⟨rfl, rfl⟩
    apply h; simpa using hij

Characterization of Pairwise Relation via List Indices: $R$-Pairwise iff $R$ Holds on All Ordered Pairs in $l$

Informal description

For any list $l$ and binary relation $R$, the list $l$ satisfies the pairwise relation $R$ if and only if for all natural numbers $i$ and $j$ such that $i < j$ and both are valid indices of $l$, the relation $R(l[i], l[j])$ holds.