Mathlib.Data.List.Lex

List.lex_cons_iff theorem

{r : α → α → Prop} [IsIrrefl α r] {a l₁ l₂} : Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂

Full source

theorem lex_cons_iff {r : α → α → Prop} [IsIrrefl α r] {a l₁ l₂} :
    LexLex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂ :=
  ⟨fun h => by obtain - | h | h := h; exacts [(irrefl_of r a h).elim, h], Lex.cons⟩

Lexicographic Order on Cons Lists with Common Head Element

Informal description

For any irreflexive relation $r$ on a type $\alpha$ and any element $a \in \alpha$ with lists $l_1, l_2 \in \text{List}(\alpha)$, the lexicographic order $\text{Lex}(r)$ satisfies $(a :: l_1) <_{\text{Lex}(r)} (a :: l_2)$ if and only if $l_1 <_{\text{Lex}(r)} l_2$.

List.lex_nil_or_eq_nil theorem

{r : α → α → Prop} (l : List α) : List.Lex r [] l ∨ l = []

Full source

theorem lex_nil_or_eq_nil {r : α → α → Prop} (l : List α) : List.LexList.Lex r [] l ∨ l = [] :=
  match l with
  | [] => Or.inr rfl
  | _ :: _ => .inl .nil

Empty List is Lexicographically Minimal or List is Empty

Informal description

For any relation `r` on a type `α` and any list `l` of elements of `α`, either the empty list `[]` is lexicographically less than `l` with respect to `r`, or `l` is itself the empty list.

List.lex_singleton_iff theorem

{r : α → α → Prop} (a b : α) : List.Lex r [a] [b] ↔ r a b

Full source

@[simp]
theorem lex_singleton_iff {r : α → α → Prop} (a b : α) : List.LexList.Lex r [a] [b] ↔ r a b :=
  ⟨fun | .rel h => h, .rel⟩

Lexicographic Order on Singleton Lists: $[a] <_{\text{Lex}(r)} [b] \leftrightarrow r(a, b)$

Informal description

For any binary relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, the lexicographic order $\text{Lex}(r)$ on singleton lists satisfies $[a] <_{\text{Lex}(r)} [b]$ if and only if $r(a, b)$ holds.

List.Lex.isOrderConnected instance

(r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] : IsOrderConnected (List α) (Lex r)

Full source

instance isOrderConnected (r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] :
    IsOrderConnected (List α) (Lex r) where
  conn := aux where
    aux
    | _, [], _ :: _, nil => Or.inr nil
    | _, [], _ :: _, rel _ => Or.inr nil
    | _, [], _ :: _, cons _ => Or.inr nil
    | _, _ :: _, _ :: _, nil => Or.inl nil
    | _ :: _, b :: _, _ :: _, rel h => (IsOrderConnected.conn _ b _ h).imp rel rel
    | a :: l₁, b :: l₂, _ :: l₃, cons h => by
      rcases trichotomous_of r a b with (ab | rfl | ab)
      · exact Or.inl (rel ab)
      · exact (aux _ l₂ _ h).imp cons cons
      · exact Or.inr (rel ab)

Order-Connectedness of Lexicographic Order on Lists

Informal description

For any type $\alpha$ with an order-connected and trichotomous relation $r$, the lexicographic order $\text{Lex}(r)$ on lists of $\alpha$ is also order-connected.

List.Lex.isTrichotomous instance

(r : α → α → Prop) [IsTrichotomous α r] : IsTrichotomous (List α) (Lex r)

Full source

instance isTrichotomous (r : α → α → Prop) [IsTrichotomous α r] :
    IsTrichotomous (List α) (Lex r) where
  trichotomous := aux where
    aux
    | [], [] => Or.inr (Or.inl rfl)
    | [], _ :: _ => Or.inl nil
    | _ :: _, [] => Or.inr (Or.inr nil)
    | a :: l₁, b :: l₂ => by
      rcases trichotomous_of r a b with (ab | rfl | ab)
      · exact Or.inl (rel ab)
      · exact (aux l₁ l₂).imp cons (Or.imp (congr_arg _) cons)
      · exact Or.inr (Or.inr (rel ab))

Trichotomy of Lexicographic Order on Lists

Informal description

For any type $\alpha$ with a trichotomous relation $r$, the lexicographic order on lists of $\alpha$ is also trichotomous.

List.Lex.isAsymm instance

(r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Lex r)

Full source

instance isAsymm (r : α → α → Prop) [IsAsymm α r] : IsAsymm (List α) (Lex r) where
  asymm := aux where
    aux
    | _, _, Lex.rel h₁, Lex.rel h₂ => asymm h₁ h₂
    | _, _, Lex.rel h₁, Lex.cons _ => asymm h₁ h₁
    | _, _, Lex.cons _, Lex.rel h₂ => asymm h₂ h₂
    | _, _, Lex.cons h₁, Lex.cons h₂ => aux _ _ h₁ h₂

Asymmetry of Lexicographic Order on Lists

Informal description

For any type $\alpha$ with an asymmetric relation $r$, the lexicographic order on lists of $\alpha$ is also asymmetric.

List.Lex.decidableRel instance

[DecidableEq α] (r : α → α → Prop) [DecidableRel r] : DecidableRel (Lex r)

Full source

instance decidableRel [DecidableEq α] (r : α → α → Prop) [DecidableRel r] : DecidableRel (Lex r)
  | l₁, [] => isFalse fun h => by cases h
  | [], _ :: _ => isTrue Lex.nil
  | a :: l₁, b :: l₂ => by
    haveI := decidableRel r l₁ l₂
    refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩
    · rcases h with (h | ⟨rfl, h⟩)
      · exact Lex.rel h
      · exact Lex.cons h
    · rcases h with (_ | h | h)
      · exact Or.inl h
      · exact Or.inr ⟨rfl, h⟩

Decidability of Lexicographic Order on Lists

Informal description

For any type $\alpha$ with a decidable equality relation and a decidable relation $r$ on $\alpha$, the lexicographic order on lists of $\alpha$ is also decidable.

List.Lex.append_right theorem

(r : α → α → Prop) : ∀ {s₁ s₂} (t), Lex r s₁ s₂ → Lex r s₁ (s₂ ++ t)

Full source

theorem append_right (r : α → α → Prop) : ∀ {s₁ s₂} (t), Lex r s₁ s₂ → Lex r s₁ (s₂ ++ t)
  | _, _, _, nil => nil
  | _, _, _, cons h => cons (append_right r _ h)
  | _, _, _, rel r => rel r

Lexicographic Order Preserved Under Right Concatenation

Informal description

For any relation $r$ on a type $\alpha$, and for any lists $s_1, s_2$ in $\alpha$, if $s_1$ is lexicographically less than $s_2$ with respect to $r$, then for any list $t$ in $\alpha$, $s_1$ remains lexicographically less than the concatenation $s_2 \mathbin{+\!\!\!+} t$ with respect to $r$.

List.Lex.append_left theorem

(R : α → α → Prop) {t₁ t₂} (h : Lex R t₁ t₂) : ∀ s, Lex R (s ++ t₁) (s ++ t₂)

Full source

theorem append_left (R : α → α → Prop) {t₁ t₂} (h : Lex R t₁ t₂) : ∀ s, Lex R (s ++ t₁) (s ++ t₂)
  | [] => h
  | _ :: l => cons (append_left R h l)

Lexicographic Order Preserved by Left Concatenation

Informal description

Let $R$ be a binary relation on a type $\alpha$, and let $t_1, t_2$ be lists of elements of $\alpha$ such that $t_1$ is lexicographically less than $t_2$ with respect to $R$ (denoted $\text{Lex } R\ t_1\ t_2$). Then for any list $s$ of elements of $\alpha$, the concatenation $s \mathbin{+\!\!+} t_1$ is lexicographically less than $s \mathbin{+\!\!+} t_2$ with respect to $R$.

List.Lex.imp theorem

{r s : α → α → Prop} (H : ∀ a b, r a b → s a b) : ∀ l₁ l₂, Lex r l₁ l₂ → Lex s l₁ l₂

Full source

theorem imp {r s : α → α → Prop} (H : ∀ a b, r a b → s a b) : ∀ l₁ l₂, Lex r l₁ l₂ → Lex s l₁ l₂
  | _, _, nil => nil
  | _, _, cons h => cons (imp H _ _ h)
  | _, _, rel r => rel (H _ _ r)

Monotonicity of Lexicographic Order under Relation Implication

Informal description

Let $r$ and $s$ be binary relations on a type $\alpha$, and suppose that for all $a, b \in \alpha$, $r(a, b)$ implies $s(a, b)$. Then for any lists $l_1, l_2$ in $\alpha$, if $l_1$ is lexicographically less than $l_2$ with respect to $r$, then $l_1$ is also lexicographically less than $l_2$ with respect to $s$.

List.Lex.to_ne theorem

: ∀ {l₁ l₂ : List α}, Lex (· ≠ ·) l₁ l₂ → l₁ ≠ l₂

Full source

theorem to_ne : ∀ {l₁ l₂ : List α}, Lex (· ≠ ·) l₁ l₂ → l₁ ≠ l₂
  | _, _, cons h, e => to_ne h (List.cons.inj e).2
  | _, _, rel r, e => r (List.cons.inj e).1

Lexicographic Inequality Implies List Inequality

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is lexicographically less than $l_2$ with respect to the relation $\neq$ (not equal), then $l_1$ is not equal to $l_2$.

Decidable.List.Lex.ne_iff theorem

[DecidableEq α] {l₁ l₂ : List α} (H : length l₁ ≤ length l₂) : Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂

Full source

theorem _root_.Decidable.List.Lex.ne_iff [DecidableEq α] {l₁ l₂ : List α}
    (H : length l₁ ≤ length l₂) : LexLex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂ :=
  ⟨to_ne, fun h => by
    induction' l₁ with a l₁ IH generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩
    · contradiction
    · apply nil
    · exact (not_lt_of_ge H).elim (succ_pos _)
    · by_cases ab : a = b
      · subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact .rel ab ⟩

Lexicographic Inequality Equivalence for Lists of Bounded Length

Informal description

For any two lists $l_1$ and $l_2$ of elements of a type $\alpha$ with decidable equality, if the length of $l_1$ is less than or equal to the length of $l_2$, then $l_1$ is lexicographically less than $l_2$ with respect to the relation $\neq$ if and only if $l_1$ is not equal to $l_2$.

List.Lex.ne_iff theorem

{l₁ l₂ : List α} (H : length l₁ ≤ length l₂) : Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂

Full source

theorem ne_iff {l₁ l₂ : List α} (H : length l₁ ≤ length l₂) : LexLex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂ := by
  classical
  exact Decidable.List.Lex.ne_iff H

Lexicographic Inequality Characterization for Lists of Bounded Length

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if the length of $l_1$ is less than or equal to the length of $l_2$, then $l_1$ is lexicographically less than $l_2$ with respect to the inequality relation if and only if $l_1$ is not equal to $l_2$.

List.instLinearOrder instance

[LinearOrder α] : LinearOrder (List α)

Full source

instance [LinearOrder α] : LinearOrder (List α) :=
  have : ∀ {r} [IsStrictTotalOrder α r], IsStrictTotalOrder (List α) (Lex r) :=
    { isStrictWeakOrder_of_isOrderConnected with }
  linearOrderOfSTO (Lex (· < ·))

Lexicographic Order on Lists

Informal description

For any type $\alpha$ with a linear order, the set of lists over $\alpha$ can be equipped with a linear order structure via the lexicographic ordering. This ordering is defined by: 1. The empty list is less than any non-empty list. 2. For non-empty lists $(a :: L)$ and $(b :: M)$, $(a :: L) < (b :: M)$ if either $a < b$ or $a = b$ and $L < M$ in the lexicographic order.

List.LE' instance

[LinearOrder α] : LE (List α)

Full source

instance LE' [LinearOrder α] : LE (List α) :=
  Preorder.toLE

Lexicographic Order on Lists

Informal description

For any type $\alpha$ with a linear order, the set of lists over $\alpha$ can be equipped with a canonical linear order structure via the lexicographic ordering. This ordering is defined by: 1. The empty list is less than any non-empty list. 2. For non-empty lists $(a :: L)$ and $(b :: M)$, $(a :: L) < (b :: M)$ if either $a < b$ or $a = b$ and $L < M$ in the lexicographic order.

List.lt_iff_lex_lt theorem

[LT α] (l l' : List α) : List.lt l l' ↔ Lex (· < ·) l l'

Full source

theorem lt_iff_lex_lt [LT α] (l l' : List α) : List.ltList.lt l l' ↔ Lex (· < ·) l l' := by
  rw [List.lt]

Lexicographic Order on Lists via Element-wise Comparison

Informal description

For any two lists `l` and `l'` of elements of type `α` equipped with a 'less than' relation `<`, the lexicographic order `List.lt` on lists is equivalent to the lexicographic order `Lex` induced by the relation `<` on elements of `α`. That is, `l < l'` if and only if `Lex (<) l l'`.

List.head_le_of_lt theorem

[Preorder α] {a a' : α} {l l' : List α} (h : (a' :: l') < (a :: l)) : a' ≤ a

Full source

theorem head_le_of_lt [Preorder α] {a a' : α} {l l' : List α} (h : (a' :: l') < (a :: l)) :
    a' ≤ a :=
  match h with
  | .cons _ => le_rfl
  | .rel h => h.le

Head Element Comparison in Lexicographic Order on Lists

Informal description

Let $\alpha$ be a type equipped with a preorder $\leq$. For any elements $a, a' \in \alpha$ and lists $l, l'$ of elements of $\alpha$, if the list $(a' :: l')$ is lexicographically less than $(a :: l)$, then $a' \leq a$.

List.head!_le_of_lt theorem

[Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) : l'.head! ≤ l.head!

Full source

theorem head!_le_of_lt [Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) :
    l'.head! ≤ l.head! := by
  replace h : List.Lex (· < ·) l' l := h
  by_cases hl : l = []
  · simp [hl] at h
  · rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h
    exact head_le_of_lt h

Head Element Comparison in Lexicographic Order for Nonempty Lists

Informal description

Let $\alpha$ be a type with a preorder $\leq$ and an inhabited instance. For any nonempty lists $l, l'$ of elements of $\alpha$, if $l'$ is lexicographically less than $l$, then the head element of $l'$ is less than or equal to the head element of $l$. That is, if $l' < l$ and $l' \neq []$, then $\text{head!}(l') \leq \text{head!}(l)$.

List.cons_le_cons theorem

[LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) : a :: l' ≤ a :: l

Full source

theorem cons_le_cons [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) :
    a :: l' ≤ a :: l := by
  rw [le_iff_lt_or_eq] at h ⊢
  exact h.imp .cons (congr_arg _)

Lexicographic Order Preserved by Cons: $l' \leq l \Rightarrow (a :: l') \leq (a :: l)$

Informal description

Let $\alpha$ be a type with a linear order. For any element $a \in \alpha$ and lists $l, l'$ of elements of $\alpha$, if $l' \leq l$ in the lexicographic order, then the list $(a :: l')$ is less than or equal to $(a :: l)$ in the lexicographic order.

See also