doc-next-gen

Mathlib.Data.List.NodupEquivFin

Module docstring

{"# Equivalence between Fin (length l) and elements of a list

Given a list l,

  • if l has no duplicates, then List.Nodup.getEquiv is the equivalence between Fin (length l) and {x // x ∈ l} sending i to ⟨get l i, _⟩ with the inverse sending ⟨x, hx⟩ to ⟨indexOf x l, _⟩;

  • if l has no duplicates and contains every element of a type α, then List.Nodup.getEquivOfForallMemList defines an equivalence between Fin (length l) and α; if α does not have decidable equality, then there is a bijection List.Nodup.getBijectionOfForallMemList;

  • if l is sorted w.r.t. (<), then List.Sorted.getIso is the same bijection reinterpreted as an OrderIso.

"}

List.Nodup.getBijectionOfForallMemList definition
(l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : { f : Fin l.length → α // Function.Bijective f }
Full source 
/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
a bijection `Fin l.length → α`.  See `List.Nodup.getEquivOfForallMemList`
for a version giving an equivalence when there is decidable equality. -/
@[simps]
def getBijectionOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) :
    { f : Fin l.length → α // Function.Bijective f } :=
  ⟨fun i => l.get i, fun _ _ h => nd.get_inj_iff.1 h,
   fun x =>
    let ⟨i, hl⟩ := List.mem_iff_get.1 (h x)
    ⟨i, hl⟩⟩
Bijection between `Fin l.length` and `α` via list indexing
Informal description
Given a list `l` of type `α` with no duplicates (`l.Nodup`) and containing every element of `α` (`∀ x : α, x ∈ l`), the function `List.get` defines a bijection between the finite type `Fin l.length` and `α`. Specifically, the bijection maps an index `i : Fin l.length` to the element `l.get i`, and its inverse maps an element `x : α` to the index `i` such that `l.get i = x`.
List.Nodup.getEquiv definition
(l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l }
Full source 
/-- If `l` has no duplicates, then `List.get` defines an equivalence between `Fin (length l)` and
the set of elements of `l`. -/
@[simps]
def getEquiv (l : List α) (H : Nodup l) : FinFin (length l) ≃ { x // x ∈ l } where
  toFun i := ⟨get l i, get_mem _ _⟩
  invFun x := ⟨idxOf (↑x) l, idxOf_lt_length_iff.2 x.2⟩
  left_inv i := by simp only [List.get_idxOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
  right_inv x := by simp
Equivalence between indices and list elements (for duplicate-free lists)
Informal description
Given a list `l` of type `α` with no duplicates (`l.Nodup`), the function `List.get` defines an equivalence (bijection with inverse) between the finite type `Fin (length l)` and the subtype `{x // x ∈ l}` consisting of elements of `l`. Specifically: - The forward map sends an index `i : Fin (length l)` to the element `⟨l.get i, proof_that_it's_in_l⟩`. - The inverse map sends an element `⟨x, hx⟩` (where `hx` proves `x ∈ l`) to the index `⟨indexOf x l, proof_that_it's_valid⟩`.
List.Nodup.getEquivOfForallMemList definition
(l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : Fin l.length ≃ α
Full source 
/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
an equivalence between `Fin l.length` and `α`.

See `List.Nodup.getBijectionOfForallMemList` for a version without
decidable equality. -/
@[simps]
def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) :
    FinFin l.length ≃ α where
  toFun i := l.get i
  invFun a := ⟨_, idxOf_lt_length_iff.2 (h a)⟩
  left_inv i := by simp [List.idxOf_getElem, nd]
  right_inv a := by simp
Equivalence between `Fin l.length` and `α` via list indexing
Informal description
Given a list `l` of type `α` with no duplicates (`l.Nodup`) and containing every element of `α` (`∀ x : α, x ∈ l`), the function `List.get` defines an equivalence (bijection with inverse) between the finite type `Fin l.length` and `α`. Specifically, the equivalence maps an index `i : Fin l.length` to the element `l.get i`, and its inverse maps an element `x : α` to the index `i` such that `l.get i = x`.
List.Sorted.get_mono theorem
(h : l.Sorted (· ≤ ·)) : Monotone l.get
Full source 
theorem get_mono (h : l.Sorted (· ≤ ·)) : Monotone l.get := fun _ _ => h.rel_get_of_le
Monotonicity of List Indexing in a Sorted List
Informal description
Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to the non-strict order relation $\leq$. Then the function $l.\text{get} : \text{Fin } l.\text{length} \to \alpha$ is monotone, meaning that for any two indices $i, j \in \text{Fin } l.\text{length}$, if $i \leq j$, then $l.\text{get}(i) \leq l.\text{get}(j)$.
List.Sorted.get_strictMono theorem
(h : l.Sorted (· < ·)) : StrictMono l.get
Full source 
theorem get_strictMono (h : l.Sorted (· < ·)) : StrictMono l.get := fun _ _ => h.rel_get_of_lt
Strict Monotonicity of List Indexing in a Strictly Sorted List
Informal description
Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to the strict order relation $<$. Then the function $l.\text{get} : \text{Fin } l.\text{length} \to \alpha$ is strictly monotone, meaning that for any two indices $i, j \in \text{Fin } l.\text{length}$, if $i < j$, then $l.\text{get}(i) < l.\text{get}(j)$.
List.Sorted.getIso definition
(l : List α) (H : Sorted (· < ·) l) : Fin (length l) ≃o { x // x ∈ l }
Full source 
/-- If `l` is a list sorted w.r.t. `(<)`, then `List.get` defines an order isomorphism between
`Fin (length l)` and the set of elements of `l`. -/
def getIso (l : List α) (H : Sorted (· < ·) l) : FinFin (length l) ≃o { x // x ∈ l } where
  toEquiv := H.nodup.getEquiv l
  map_rel_iff' := H.get_strictMono.le_iff_le
Order isomorphism between indices and elements of a strictly sorted list
Informal description
Given a list `l` of type `α` that is sorted with respect to the strict order relation `<`, the function `List.Sorted.getIso` defines an order isomorphism between the finite type `Fin (length l)` and the subtype `{x // x ∈ l}` consisting of elements of `l`. Specifically: - The forward map sends an index `i : Fin (length l)` to the element `⟨l.get i, proof_that_it's_in_l⟩`. - The inverse map sends an element `⟨x, hx⟩` (where `hx` proves `x ∈ l`) to the index `⟨indexOf x l, proof_that_it's_valid⟩`. - The isomorphism preserves the order structure, meaning that for any two indices `i, j : Fin (length l)`, we have `i ≤ j` if and only if `l.get i ≤ l.get j`.
List.Sorted.coe_getIso_apply theorem
: (H.getIso l i : α) = get l i
Full source 
@[simp]
theorem coe_getIso_apply : (H.getIso l i : α) = get l i :=
  rfl
Equality of Projected Order Isomorphism and List Indexing in a Sorted List
Informal description
Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to the strict order relation $<$, and let $H$ be a proof of this fact. For any index $i \in \text{Fin}(\text{length } l)$, the element obtained by applying the order isomorphism $\text{getIso}$ to $i$ (and then projecting to $\alpha$) is equal to the $i$-th element of $l$ via $\text{get}$. In symbols: if $\text{getIso}_H : \text{Fin}(\text{length } l) \simeq_o \{x \in \alpha \mid x \in l\}$ is the order isomorphism, then for any $i \in \text{Fin}(\text{length } l)$, we have $(\text{getIso}_H(i) : \alpha) = \text{get } l \ i$.
List.Sorted.coe_getIso_symm_apply theorem
: ((H.getIso l).symm x : ℕ) = idxOf (↑x) l
Full source 
@[simp]
theorem coe_getIso_symm_apply : ((H.getIso l).symm x : ℕ) = idxOf (↑x) l :=
  rfl
Index Correspondence via Inverse Order Isomorphism for Sorted Lists
Informal description
Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to the strict order relation $<$, and let $H$ be a proof of this fact. For any element $x \in l$, the natural number obtained by applying the inverse of the order isomorphism $\text{getIso}_H$ to $x$ (and then projecting to $\mathbb{N}$) is equal to the index of $x$ in $l$ via $\text{idxOf}$. In symbols: if $\text{getIso}_H : \text{Fin}(\text{length } l) \simeq_o \{x \in \alpha \mid x \in l\}$ is the order isomorphism, then for any $x \in l$, we have $(\text{getIso}_H^{-1}(x) : \mathbb{N}) = \text{idxOf } x \ l$.
List.sublist_of_orderEmbedding_getElem?_eq theorem
{l l' : List α} (f : ℕ ↪o ℕ) (hf : ∀ ix : ℕ, l[ix]? = l'[f ix]?) : l <+ l'
Full source 
/-- If there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`,
then `Sublist l l'`.
-/
theorem sublist_of_orderEmbedding_getElem?_eq {l l' : List α} (f : ℕℕ ↪o ℕ)
    (hf : ∀ ix : ℕ, l[ix]? = l'[f ix]?) : l <+ l' := by
  induction' l with hd tl IH generalizing l' f
  · simp
  have : some hd = l'[f 0]? := by simpa using hf 0
  rw [eq_comm, List.getElem?_eq_some_iff] at this
  obtain ⟨w, h⟩ := this
  let f' : ℕℕ ↪o ℕ :=
    OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
      dsimp only
      rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos
  have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
    intro ix
    rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
    simp only [getElem?_cons_succ]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos
  rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
  apply List.Sublist.append _ (IH _ this)
  rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
  exact List.getElem_mem _
Sublist Criterion via Order-Preserving Index Mapping
Informal description
Let $l$ and $l'$ be lists of elements of type $\alpha$. If there exists an order embedding $f : \mathbb{N} \hookrightarrow \mathbb{N}$ such that for every index $i \in \mathbb{N}$, the $i$-th element of $l$ (if it exists) is equal to the $f(i)$-th element of $l'$ (if it exists), then $l$ is a sublist of $l'$. In symbols: if $\forall i \in \mathbb{N}, l[i]? = l'[f(i)]?$, then $l \subseteq l'$.
List.sublist_iff_exists_orderEmbedding_getElem?_eq theorem
{l l' : List α} : l <+ l' ↔ ∃ f : ℕ ↪o ℕ, ∀ ix : ℕ, l[ix]? = l'[f ix]?
Full source 
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_orderEmbedding_getElem?_eq {l l' : List α} :
    l <+ l'l <+ l' ↔ ∃ f : ℕ ↪o ℕ, ∀ ix : ℕ, l[ix]? = l'[f ix]? := by
  constructor
  · intro H
    induction H with
    | slnil => simp
    | cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf
    | cons₂ _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _
  · rintro ⟨f, hf⟩
    exact sublist_of_orderEmbedding_getElem?_eq f hf
Sublist Characterization via Order-Preserving Index Mapping
Informal description
For two lists $l$ and $l'$ of elements of type $\alpha$, $l$ is a sublist of $l'$ if and only if there exists an order-preserving embedding $f : \mathbb{N} \hookrightarrow \mathbb{N}$ such that for every index $i \in \mathbb{N}$, the $i$-th element of $l$ (if it exists) is equal to the $f(i)$-th element of $l'$ (if it exists). In symbols: $l \subseteq l' \iff \exists f : \mathbb{N} \hookrightarrow \mathbb{N}, \forall i \in \mathbb{N}, l[i]? = l'[f(i)]?$.
List.sublist_iff_exists_fin_orderEmbedding_get_eq theorem
{l l' : List α} : l <+ l' ↔ ∃ f : Fin l.length ↪o Fin l'.length, ∀ ix : Fin l.length, l.get ix = l'.get (f ix)
Full source 
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `Fin l.length` into `Fin l'.length` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_fin_orderEmbedding_get_eq {l l' : List α} :
    l <+ l'l <+ l' ↔
      ∃ f : Fin l.length ↪o Fin l'.length,
        ∀ ix : Fin l.length, l.get ix = l'.get (f ix) := by
  rw [sublist_iff_exists_orderEmbedding_getElem?_eq]
  constructor
  · rintro ⟨f, hf⟩
    have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
      intro i hi
      specialize hf i
      rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
      obtain ⟨h, -⟩ := hf
      exact h
    refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
    · simp
    · intro i
      apply Option.some_injective
      simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i
  · rintro ⟨f, hf⟩
    refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩
    · intro i j h
      dsimp only
      split_ifs with hi hj hj
      · rwa [Fin.val_fin_lt, f.lt_iff_lt]
      · omega
      · exact absurd (h.trans hj) hi
      · simpa using h
    · intro i
      simp only [OrderEmbedding.coe_ofStrictMono]
      split_ifs with hi
      · specialize hf ⟨i, hi⟩
        simp_all
      · rw [getElem?_eq_none_iff.mpr, getElem?_eq_none_iff.mpr]
        · simp
        · simpa using hi
Sublist Characterization via Finite Order-Preserving Index Mapping
Informal description
For two lists $l$ and $l'$ of elements of type $\alpha$, $l$ is a sublist of $l'$ if and only if there exists an order-preserving embedding $f$ from the finite type $\text{Fin } l.\text{length}$ to $\text{Fin } l'.\text{length}$ such that for every index $i \in \text{Fin } l.\text{length}$, the element of $l$ at position $i$ equals the element of $l'$ at position $f(i)$. In symbols: $l \subseteq l' \iff \exists f : \text{Fin } l.\text{length} \hookrightarrow \text{Fin } l'.\text{length}, \forall i \in \text{Fin } l.\text{length}, l[i] = l'[f(i)]$.
List.duplicate_iff_exists_distinct_get theorem
{l : List α} {x : α} : l.Duplicate x ↔ ∃ (n m : Fin l.length) (_ : n < m), x = l.get n ∧ x = l.get m
Full source 
/-- An element `x : α` of `l : List α` is a duplicate iff it can be found
at two distinct indices `n m : ℕ` inside the list `l`.
-/
theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
    l.Duplicate x ↔
      ∃ (n m : Fin l.length) (_ : n < m),
        x = l.get n ∧ x = l.get m := by
  classical
    rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
    constructor
    · rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp
    · rintro ⟨n, m, hnm, h, h'⟩
      refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'
Characterization of Duplicate Elements via Distinct Indices in a List
Informal description
An element $x$ is a duplicate in a list $l$ if and only if there exist two distinct indices $n$ and $m$ (with $n < m$) in the finite set of valid indices for $l$ such that $x$ is equal to both the $n$-th and $m$-th elements of $l$. In symbols: $x$ is a duplicate in $l$ $\iff$ $\exists n, m \in \text{Fin } l.\text{length}, n < m \land x = l[n] \land x = l[m]$.