Module docstring
{"### Lexicographic ordering "}
List.lex_lt
theorem
[LT α] {l₁ l₂ : List α} : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂
Informal description
For any type $\alpha$ with a "less than" relation and for any two lists $l_1, l_2$ of elements of $\alpha$, the lexicographic order relation `Lex (· < ·) l₁ l₂` holds if and only if $l_1$ is lexicographically less than $l_2$.
List.not_lex_lt
theorem
[LT α] {l₁ l₂ : List α} : ¬Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁
Full source
@[simp] theorem not_lex_lt [LT α] {l₁ l₂ : List α} : ¬ Lex (· < ·) l₁ l₂¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rflInformal description
For any type $\alpha$ with a "less than" relation and for any two lists $l_1, l_2$ of elements of $\alpha$, the statement that $l_1$ is not lexicographically less than $l_2$ is equivalent to $l_2$ being lexicographically less than or equal to $l_1$.
List.not_lt_iff_ge
theorem
[LT α] {l₁ l₂ : List α} : ¬l₁ < l₂ ↔ l₂ ≤ l₁
Full source
protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rflInformal description
For any type $\alpha$ with a "less than" relation and for any two lists $l_1, l_2$ of elements of $\alpha$, the statement that $l_1$ is not lexicographically less than $l_2$ is equivalent to $l_2$ being lexicographically less than or equal to $l_1$.
List.not_le_iff_gt
theorem
[DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : ¬l₁ ≤ l₂ ↔ l₂ < l₁
Full source
protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
¬ l₁ ≤ l₂¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
Decidable.not_notInformal description
For any type $\alpha$ with decidable equality and a decidable "less than" relation, and for any two lists $l_1, l_2$ of elements of $\alpha$, the negation of $l_1 \leq l_2$ (in the lexicographic order) is equivalent to $l_2 < l_1$.
List.lex_irrefl
theorem
{r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l
Full source
theorem lex_irrefl {r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l := by
induction l with
| nil => nofun
| cons a l ih => intro
| .rel h => exact irrefl _ h
| .cons h => exact ih hInformal description
For any irreflexive relation $r$ on a type $\alpha$ (i.e., $\forall x, \neg r(x, x)$) and any list $l$ of elements of $\alpha$, the lexicographic order induced by $r$ is also irreflexive on $l$, meaning $\neg \text{Lex}(r, l, l)$.
List.lt_irrefl
theorem
[LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : List α) : ¬l < l
Full source
protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (l : List α) : ¬ l < l :=
lex_irrefl Std.Irrefl.irrefl lInformal description
For any type $\alpha$ equipped with a strict order relation $<$ that is irreflexive (i.e., $\forall x \in \alpha, \neg (x < x)$), and for any list $l$ of elements of $\alpha$, the lexicographic order induced by $<$ is also irreflexive on $l$, meaning $\neg (l < l)$.
List.ltIrrefl
instance
[LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := List α) (· < ·)
Full source
instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := List α) (· < ·) where
irrefl := List.lt_irreflInformal description
For any type $\alpha$ with a strict order relation $<$ that is irreflexive, the lexicographic order on lists of $\alpha$ is also irreflexive.
List.not_lex_nil
theorem
: ¬Lex r l []
Full source
@[simp] theorem not_lex_nil : ¬Lex r l [] := fun h => nomatch hInformal description
For any relation $r$ and any list $l$, the empty list is not lexicographically less than $l$ under $r$.
List.not_lt_nil
theorem
[LT α] (l : List α) : ¬l < []
Full source
@[simp] theorem not_lt_nil [LT α] (l : List α) : ¬ l < [] := fun h => nomatch hInformal description
For any list $l$ of elements of type $\alpha$ equipped with a "less than" relation, the list $l$ is not less than the empty list.
List.nil_le
theorem
[LT α] (l : List α) : [] ≤ l
Informal description
For any list $l$ of elements of type $\alpha$ with a "less than" relation, the empty list is less than or equal to $l$.
List.not_nil_lex_iff
theorem
: ¬Lex r [] l ↔ l = []
Full source
@[simp] theorem not_nil_lex_iff : ¬Lex r [] l¬Lex r [] l ↔ l = [] := by
constructor
· rintro h
match l, h with
| [], h => rfl
| a :: _, h => exact False.elim (h Lex.nil)
· rintro rfl
exact not_lex_nilInformal description
For any relation $r$ and any list $l$, the empty list is not lexicographically less than $l$ under $r$ if and only if $l$ is the empty list. In other words, $\neg(\text{Lex } r\ []\ l) \leftrightarrow l = []$.
List.le_nil
theorem
[LT α] {l : List α} : l ≤ [] ↔ l = []
Full source
@[simp] theorem le_nil [LT α] {l : List α} : l ≤ [] ↔ l = [] := not_nil_lex_iffInformal description
For any list $l$ of elements of a type $\alpha$ equipped with a 'less than' relation, $l$ is less than or equal to the empty list if and only if $l$ is the empty list itself, i.e., $l \leq [] \leftrightarrow l = []$.
List.nil_lex_cons'
theorem
: Lex r [] (a :: l)
Full source
@[simp] theorem nil_lex_cons' : Lex r [] (a :: l) := Lex.nilInformal description
For any relation $r$ on a type $\alpha$ and any elements $a \in \alpha$ and list $l$ of elements of $\alpha$, the empty list is lexicographically less than the list $a :: l$ under the relation $r$.
List.nil_lt_cons
theorem
[LT α] (a : α) (l : List α) : [] < a :: l
Informal description
For any type $\alpha$ with a 'less than' relation and any elements $a \in \alpha$ and list $l$ of elements of $\alpha$, the empty list is strictly less than the list constructed by prepending $a$ to $l$.
List.cons_lex_cons_iff
theorem
: Lex r (a :: l₁) (b :: l₂) ↔ r a b ∨ a = b ∧ Lex r l₁ l₂
Informal description
For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$ with lists $l_1, l_2$ of elements of $\alpha$, the lexicographic order relation $\text{Lex}\,r$ holds between the lists $a :: l_1$ and $b :: l_2$ if and only if either $r\,a\,b$ holds, or $a = b$ and $\text{Lex}\,r\,l_1\,l_2$ holds.
List.cons_lt_cons_iff
theorem
[LT α] {a b} {l₁ l₂ : List α} : (a :: l₁) < (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ < l₂
Full source
theorem cons_lt_cons_iff [LT α] {a b} {l₁ l₂ : List α} :
(a :: l₁) < (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ < l₂ := by
dsimp only [instLT, List.lt]
simp [cons_lex_cons_iff]Informal description
For any type $\alpha$ with a 'less than' relation and any elements $a, b \in \alpha$ and lists $l_1, l_2$ of elements of $\alpha$, the list $a :: l_1$ is lexicographically less than $b :: l_2$ if and only if either $a < b$, or $a = b$ and $l_1$ is lexicographically less than $l_2$.
List.cons_lt_cons_self
theorem
[LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} : (a :: l₁) < (a :: l₂) ↔ l₁ < l₂
Full source
@[simp] theorem cons_lt_cons_self [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} :
(a :: l₁) < (a :: l₂) ↔ l₁ < l₂ := by
simp [cons_lt_cons_iff, i₀.irrefl]Informal description
For any type $\alpha$ with a strict order relation $<$, if the relation is irreflexive (i.e., $x < x$ never holds for any $x \in \alpha$), then for any lists $l_1, l_2$ of elements of $\alpha$ and any element $a \in \alpha$, the list $a :: l_1$ is lexicographically less than $a :: l_2$ if and only if $l_1$ is lexicographically less than $l_2$.
List.not_cons_lex_cons_iff
theorem
[DecidableEq α] [DecidableRel r] {a b} {l₁ l₂ : List α} :
¬Lex r (a :: l₁) (b :: l₂) ↔ (¬r a b ∧ a ≠ b) ∨ (¬r a b ∧ ¬Lex r l₁ l₂)
Full source
theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂ : List α} :
¬ Lex r (a :: l₁) (b :: l₂)¬ Lex r (a :: l₁) (b :: l₂) ↔ (¬ r a b ∧ a ≠ b) ∨ (¬ r a b ∧ ¬ Lex r l₁ l₂) := by
rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]Informal description
For a type $\alpha$ with decidable equality and a decidable relation $r$, and for any elements $a, b \in \alpha$ and lists $l_1, l_2$ of elements of $\alpha$, the negation of the lexicographic order relation $\text{Lex}\,r$ between the lists $a :: l_1$ and $b :: l_2$ holds if and only if either both $\neg r(a, b)$ and $a \neq b$ hold, or both $\neg r(a, b)$ and $\neg \text{Lex}\,r\,l_1\,l_2$ hold.
In symbols:
\[
\neg \text{Lex}\,r\,(a :: l_1)\,(b :: l_2) \leftrightarrow (\neg r(a, b) \land a \neq b) \lor (\neg r(a, b) \land \neg \text{Lex}\,r\,l_1\,l_2).
\]
List.cons_le_cons_iff
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] [i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬· < · : α → α → Prop)] {a b} {l₁ l₂ : List α} : (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂
Full source
theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
[i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
{a b} {l₁ l₂ : List α} :
(a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
dsimp only [instLE, instLT, List.le, List.lt]
simp only [not_cons_lex_cons_iff, ne_eq]
constructor
· rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
· left
apply Decidable.byContradiction
intro h₃
apply h₂
exact i₂.antisymm _ _ h₁ h₃
· if h₃ : a < b then
exact .inl h₃
else
right
exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩
· rintro (h | ⟨h₁, h₂⟩)
· left
exact ⟨i₁.asymm _ _ h, fun w => i₀.irrefl _ (w ▸ h)⟩
· right
exact ⟨fun w => i₀.irrefl _ (h₁ ▸ w), h₂⟩Informal description
For a type $\alpha$ with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive, asymmetric, and its negation $\not<$ is antisymmetric, and for any elements $a, b \in \alpha$ and lists $l_1, l_2$ of elements of $\alpha$, the lexicographic order relation $(a :: l_1) \leq_{\text{lex}} (b :: l_2)$ holds if and only if either $a < b$ or $a = b$ and $l_1 \leq_{\text{lex}} l_2$.
In symbols:
\[
(a :: l_1) \leq_{\text{lex}} (b :: l_2) \leftrightarrow a < b \lor (a = b \land l_1 \leq_{\text{lex}} l_2).
\]
List.not_lt_of_cons_le_cons
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] [i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬· < · : α → α → Prop)] {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬b < a
Full source
theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
[i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
{a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a := by
rw [cons_le_cons_iff] at h
rcases h with h | ⟨rfl, h⟩
· exact i₁.asymm _ _ h
· exact i₀.irrefl _Informal description
For a type $\alpha$ with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive, asymmetric, and its negation $\not<$ is antisymmetric, and for any elements $a, b \in \alpha$ and lists $l_1, l_2$ of elements of $\alpha$, if the lexicographic order relation $(a :: l_1) \leq_{\text{lex}} (b :: l_2)$ holds, then it is not the case that $b < a$.
In symbols:
\[
(a :: l_1) \leq_{\text{lex}} (b :: l_2) \implies \neg (b < a).
\]
List.le_of_cons_le_cons
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] [i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬· < · : α → α → Prop)] {a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂
Full source
theorem le_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
[i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
{a} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂ := by
rw [cons_le_cons_iff] at h
rcases h with h | ⟨_, h⟩
· exact False.elim (i₀.irrefl _ h)
· exact hInformal description
For a type $\alpha$ with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive, asymmetric, and its negation $\not<$ is antisymmetric, and for any element $a \in \alpha$ and lists $l_1, l_2$ of elements of $\alpha$, if the lexicographic order relation $(a :: l_1) \leq_{\text{lex}} (a :: l_2)$ holds, then $l_1 \leq_{\text{lex}} l_2$.
In symbols:
\[
(a :: l_1) \leq_{\text{lex}} (a :: l_2) \implies l_1 \leq_{\text{lex}} l_2.
\]
List.le_refl
theorem
[LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] (l : List α) : l ≤ l
Informal description
For any type $\alpha$ equipped with a strict order relation $<$ that is irreflexive (i.e., $\forall x \in \alpha, \neg (x < x)$), and for any list $l$ of elements of type $\alpha$, the lexicographic order $\leq$ on lists is reflexive, meaning $l \leq l$.
List.instReflLeOfIrreflLt
instance
[LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : List α → List α → Prop)
Full source
instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : List α → List α → Prop) where
refl := List.le_reflInformal description
For any type $\alpha$ equipped with a strict order relation $<$ that is irreflexive (i.e., $\forall x \in \alpha, \neg (x < x)$), the lexicographic order $\leq$ on lists of elements of type $\alpha$ is reflexive, meaning $l \leq l$ for any list $l \in \text{List } \alpha$.
List.lex_trans
theorem
{r : α → α → Prop} (lt_trans : ∀ {x y z : α}, r x y → r y z → r x z) (h₁ : Lex r l₁ l₂) (h₂ : Lex r l₂ l₃) :
Lex r l₁ l₃
Full source
theorem lex_trans {r : α → α → Prop}
(lt_trans : ∀ {x y z : α}, r x y → r y z → r x z)
(h₁ : Lex r l₁ l₂) (h₂ : Lex r l₂ l₃) : Lex r l₁ l₃ := by
induction h₁ generalizing l₃ with
| nil => let _::_ := l₃; exact List.Lex.nil ..
| @rel a l₁ b l₂ ab =>
match h₂ with
| .rel bc => exact List.Lex.rel (lt_trans ab bc)
| .cons ih =>
exact List.Lex.rel ab
| @cons a l₁ l₂ h₁ ih2 =>
match h₂ with
| .rel bc =>
exact List.Lex.rel bc
| .cons ih =>
exact List.Lex.cons (ih2 ih)Informal description
Let $α$ be a type with a relation $r : α → α → \text{Prop}$ that is transitive (i.e., for any $x, y, z \in α$, if $r(x,y)$ and $r(y,z)$ hold, then $r(x,z)$ holds). Then for any lists $l₁, l₂, l₃$ in $\text{List }α$, if $l₁$ is lexicographically less than $l₂$ with respect to $r$ (denoted $\text{Lex }r\ l₁\ l₂$) and $l₂$ is lexicographically less than $l₃$ with respect to $r$ ($\text{Lex }r\ l₂\ l₃$), then $l₁$ is lexicographically less than $l₃$ with respect to $r$ ($\text{Lex }r\ l₁\ l₃$).
List.lt_trans
theorem
[LT α] [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)] {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃
Informal description
Let $\alpha$ be a type equipped with a strict order relation $<$. If $<$ is transitive on $\alpha$ (i.e., for any $x, y, z \in \alpha$, $x < y$ and $y < z$ implies $x < z$), then the lexicographic order on lists $\text{List } \alpha$ is also transitive. Specifically, for any lists $l_1, l_2, l_3 \in \text{List } \alpha$, if $l_1 < l_2$ and $l_2 < l_3$, then $l_1 < l_3$.
List.instTransLt
instance
[LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] : Trans (· < · : List α → List α → Prop) (· < ·) (· < ·)
Informal description
For any type $\alpha$ equipped with a strict order relation $<$ that is transitive, the lexicographic order on lists $\text{List } \alpha$ is also transitive. Specifically, for any lists $l_1, l_2, l_3 \in \text{List } \alpha$, if $l_1 < l_2$ and $l_2 < l_3$, then $l_1 < l_3$.
List.lt_antisymm
abbrev
Full source
@[deprecated List.le_antisymm (since := "2024-12-13")]
protected abbrev lt_antisymm := @List.le_antisymmInformal description
Let $\alpha$ be a type with decidable equality and a decidable "less than" relation $<$, such that the relation $\neg(x < y)$ is antisymmetric (i.e., if $\neg(x < y)$ and $\neg(y < x)$ both hold, then $x = y$). Then for any two lists $l_1$ and $l_2$ of elements of $\alpha$, if $l_1 < l_2$ and $l_2 < l_1$ with respect to the lexicographic order, it follows that $l_1 = l_2$.
List.lt_of_le_of_lt
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] [i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬· < · : α → α → Prop)] [i₃ : Trans (¬· < · : α → α → Prop) (¬· < ·) (¬· < ·)] {l₁ l₂ l₃ : List α}
(h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃
Full source
protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
[i₀ : Std.Irrefl (· < · : α → α → Prop)]
[i₁ : Std.Asymm (· < · : α → α → Prop)]
[i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
[i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
induction h₂ generalizing l₁ with
| nil => simp_all
| rel hab =>
rename_i a xs
cases l₁ with
| nil => simp_all
| cons c l₁ =>
apply Lex.rel
replace h₁ := not_lt_of_cons_le_cons h₁
apply Decidable.byContradiction
intro h₂
have := i₃.trans h₁ h₂
contradiction
| cons w₃ ih =>
rename_i a as bs
cases l₁ with
| nil => simp_all
| cons c l₁ =>
have w₄ := not_lt_of_cons_le_cons h₁
by_cases w₅ : a = c
· subst w₅
exact Lex.cons (ih (le_of_cons_le_cons h₁))
· exact Lex.rel (Decidable.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))Informal description
For a type $\alpha$ with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive, asymmetric, and its negation $\not<$ is antisymmetric and transitive, and for any lists $l_1, l_2, l_3$ of elements of $\alpha$, if $l_1 \leq_{\text{lex}} l_2$ and $l_2 <_{\text{lex}} l_3$, then $l_1 <_{\text{lex}} l_3$.
In symbols:
\[
l_1 \leq_{\text{lex}} l_2 \text{ and } l_2 <_{\text{lex}} l_3 \implies l_1 <_{\text{lex}} l_3.
\]
List.le_trans
theorem
[DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬· < · : α → α → Prop)] [Trans (¬· < · : α → α → Prop) (¬· < ·) (¬· < ·)] {l₁ l₂ l₃ : List α}
(h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃
Full source
protected theorem le_trans [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)]
[Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
{l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)Informal description
Let $\alpha$ be a type with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive and asymmetric, and its negation $\not<$ is antisymmetric and transitive. For any lists $l_1, l_2, l_3$ of elements of $\alpha$, if $l_1 \leq_{\text{lex}} l_2$ and $l_2 \leq_{\text{lex}} l_3$ with respect to the lexicographic order, then $l_1 \leq_{\text{lex}} l_3$.
In symbols:
\[
l_1 \leq_{\text{lex}} l_2 \text{ and } l_2 \leq_{\text{lex}} l_3 \implies l_1 \leq_{\text{lex}} l_3.
\]
List.instTransLeOfDecidableEqOfDecidableLTOfIrreflOfAsymmOfAntisymmOfNotLt
instance
[DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬· < · : α → α → Prop)] [Trans (¬· < · : α → α → Prop) (¬· < ·) (¬· < ·)] :
Trans (· ≤ · : List α → List α → Prop) (· ≤ ·) (· ≤ ·)
Full source
instance [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)]
[Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
Trans (· ≤ · : List α → List α → Prop) (· ≤ ·) (· ≤ ·) where
trans h₁ h₂ := List.le_trans h₁ h₂Informal description
For any type $\alpha$ with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive and asymmetric, and its negation $\not<$ is antisymmetric and transitive, the lexicographic order $\leq$ on lists of elements of $\alpha$ is transitive. That is, for any lists $l_1, l_2, l_3$ of elements of $\alpha$, if $l_1 \leq l_2$ and $l_2 \leq l_3$, then $l_1 \leq l_3$.
In symbols:
\[
l_1 \leq l_2 \text{ and } l_2 \leq l_3 \implies l_1 \leq l_3.
\]
List.lex_asymm
theorem
{r : α → α → Prop} (h : ∀ {x y : α}, r x y → ¬r y x) : ∀ {l₁ l₂ : List α}, Lex r l₁ l₂ → ¬Lex r l₂ l₁
Full source
theorem lex_asymm {r : α → α → Prop}
(h : ∀ {x y : α}, r x y → ¬ r y x) : ∀ {l₁ l₂ : List α}, Lex r l₁ l₂ → ¬ Lex r l₂ l₁
| nil, _, .nil => by simp
| x :: l₁, y :: l₂, .rel h₁ =>
fun
| .rel h₂ => h h₁ h₂
| .cons h₂ => h h₁ h₁
| x :: l₁, _ :: l₂, .cons h₁ =>
fun
| .rel h₂ => h h₂ h₂
| .cons h₂ => lex_asymm h h₁ h₂Informal description
For any binary relation $r$ on a type $\alpha$ that is asymmetric (i.e., for any $x, y \in \alpha$, if $r(x, y)$ holds then $r(y, x)$ does not hold), the lexicographic order $\text{Lex}(r)$ on lists of elements of $\alpha$ is also asymmetric. That is, for any lists $l_1, l_2$ of elements of $\alpha$, if $\text{Lex}(r)(l_1, l_2)$ holds, then $\text{Lex}(r)(l_2, l_1)$ does not hold.
List.lt_asymm
theorem
[LT α] [i : Std.Asymm (· < · : α → α → Prop)] {l₁ l₂ : List α} (h : l₁ < l₂) : ¬l₂ < l₁
Informal description
For any type $\alpha$ with a strict order relation $<$ that is asymmetric (i.e., for any $x, y \in \alpha$, if $x < y$ then $\neg (y < x)$), and for any two lists $l_1, l_2$ of elements of $\alpha$, if $l_1 < l_2$ holds under the lexicographic order induced by $<$, then $l_2 < l_1$ does not hold.
List.instAsymmLt
instance
[LT α] [Std.Asymm (· < · : α → α → Prop)] : Std.Asymm (· < · : List α → List α → Prop)
Informal description
For any type $\alpha$ with a strict order relation $<$ that is asymmetric (i.e., $x < y$ implies $\neg (y < x)$ for all $x, y \in \alpha$), the lexicographic order on lists of elements of $\alpha$ is also asymmetric.
List.not_lex_total
theorem
[DecidableEq α] {r : α → α → Prop} [DecidableRel r] (h : ∀ x y : α, ¬r x y ∨ ¬r y x) (l₁ l₂ : List α) :
¬Lex r l₁ l₂ ∨ ¬Lex r l₂ l₁
Full source
theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
(h : ∀ x y : α, ¬ r x y¬ r x y ∨ ¬ r y x) (l₁ l₂ : List α) : ¬ Lex r l₁ l₂¬ Lex r l₁ l₂ ∨ ¬ Lex r l₂ l₁ := by
rw [Decidable.or_iff_not_imp_left, Decidable.not_not]
intro w₁ w₂
match l₁, l₂, w₁, w₂ with
| nil, _ :: _, .nil, w₂ => simp at w₂
| x :: _, y :: _, .rel _, .rel _ =>
obtain (_ | _) := h x y <;> contradiction
| x :: _, _ :: _, .rel _, .cons _ =>
obtain (_ | _) := h x x <;> contradiction
| x :: _, _ :: _, .cons _, .rel _ =>
obtain (_ | _) := h x x <;> contradiction
| _ :: l₁, _ :: l₂, .cons _, .cons _ =>
obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradictionInformal description
Let $\alpha$ be a type with decidable equality and let $r : \alpha \to \alpha \to \mathrm{Prop}$ be a decidable binary relation on $\alpha$. Suppose that for any two elements $x, y \in \alpha$, either $\neg r(x, y)$ or $\neg r(y, x)$ holds. Then for any two lists $l_1, l_2$ of elements of $\alpha$, either $\neg \mathrm{Lex}(r, l_1, l_2)$ or $\neg \mathrm{Lex}(r, l_2, l_1)$ holds, where $\mathrm{Lex}(r)$ denotes the lexicographic order on lists induced by $r$.
List.le_total
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i : Std.Total (¬· < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁
Full source
protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
[i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
not_lex_total i.total l₂ l₁Informal description
Let $\alpha$ be a type with decidable equality and a decidable "less than" relation $<$, and suppose that for any two elements $x, y \in \alpha$, either $\neg (x < y)$ or $\neg (y < x)$ holds. Then, for any two lists $l_1, l_2$ of elements of $\alpha$, either $l_1 \leq l_2$ or $l_2 \leq l_1$ holds, where $\leq$ denotes the lexicographic order on lists induced by $<$.
List.instTotalLeOfDecidableEqOfDecidableLTOfNotLt
instance
[DecidableEq α] [LT α] [DecidableLT α] [Std.Total (¬· < · : α → α → Prop)] : Std.Total (· ≤ · : List α → List α → Prop)
Full source
instance [DecidableEq α] [LT α] [DecidableLT α]
[Std.Total (¬ · < · : α → α → Prop)] :
Std.Total (· ≤ · : List α → List α → Prop) where
total := List.le_totalInformal description
For any type $\alpha$ with decidable equality and a decidable "less than" relation $<$, if the relation $\neg (x < y)$ is total on $\alpha$ (i.e., for any $x, y \in \alpha$, either $\neg (x < y)$ or $\neg (y < x)$ holds), then the lexicographic order $\leq$ on lists of elements of $\alpha$ is also total.
List.not_lt
theorem
[LT α] {l₁ l₂ : List α} : ¬l₁ < l₂ ↔ l₂ ≤ l₁
Informal description
For any type $\alpha$ with a "less than" relation and for any two lists $l_1, l_2$ of elements of $\alpha$, the negation of $l_1 < l_2$ is equivalent to $l_2 \leq l_1$.
List.not_le
theorem
[DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : ¬l₂ ≤ l₁ ↔ l₁ < l₂
Full source
@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : List α} : ¬ l₂ ≤ l₁¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_notInformal description
For any type $\alpha$ with decidable equality and a decidable "less than" relation, and for any two lists $l_1, l_2$ of elements of $\alpha$, the negation of $l_2 \leq l_1$ is equivalent to $l_1 < l_2$.
List.le_of_lt
theorem
[DecidableEq α] [LT α] [DecidableLT α] [i : Std.Total (¬· < · : α → α → Prop)] {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂
Full source
protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
[i : Std.Total (¬ · < · : α → α → Prop)]
{l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂ := by
obtain (h' | h') := List.le_total l₁ l₂
· exact h'
· exfalso
exact h' hInformal description
Let $\alpha$ be a type with decidable equality and a decidable "less than" relation $<$, and suppose that for any two elements $x, y \in \alpha$, either $\neg (x < y)$ or $\neg (y < x)$ holds. Then, for any two lists $l_1, l_2$ of elements of $\alpha$, if $l_1 < l_2$ holds, then $l_1 \leq l_2$ also holds, where $\leq$ denotes the lexicographic order on lists induced by $<$.
List.le_iff_lt_or_eq
theorem
[DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Antisymm (¬· < · : α → α → Prop)]
[Std.Total (¬· < · : α → α → Prop)] {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂
Full source
protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)]
[Std.Total (¬ · < · : α → α → Prop)]
{l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by
constructor
· intro h
by_cases h' : l₂ ≤ l₁
· right
apply List.le_antisymm h h'
· left
exact Decidable.not_not.mp h'
· rintro (h | rfl)
· exact List.le_of_lt h
· exact List.le_refl l₁Informal description
Let $\alpha$ be a type with decidable equality and a decidable strict order relation $<$, where $<$ is irreflexive, and the relation $\neg(x < y)$ is antisymmetric and total. Then for any two lists $l_1, l_2$ of elements of $\alpha$, the lexicographic order $l_1 \leq l_2$ holds if and only if either $l_1 < l_2$ or $l_1 = l_2$.
List.lex_eq_decide_lex
theorem
[DecidableEq α] (lt : α → α → Bool) : lex l₁ l₂ lt = decide (Lex (fun x y => lt x y) l₁ l₂)
Full source
theorem lex_eq_decide_lex [DecidableEq α] (lt : α → α → Bool) :
lex l₁ l₂ lt = decide (Lex (fun x y => lt x y) l₁ l₂) := by
induction l₁ generalizing l₂ with
| nil =>
cases l₂ with
| nil => simp [lex]
| cons b bs => simp [lex]
| cons a l₁ ih =>
cases l₂ with
| nil => simp [lex]
| cons b bs =>
simp [lex, ih, cons_lex_cons_iff, Bool.beq_eq_decide_eq]Informal description
For any type $\alpha$ with decidable equality and any boolean-valued comparison function $\mathrm{lt} : \alpha \to \alpha \to \mathrm{Bool}$, the lexicographic comparison of two lists $l_1$ and $l_2$ using $\mathrm{lt}$ is equal to the boolean evaluation of the proposition that $l_1$ is lexicographically less than $l_2$ with respect to the relation $\lambda x y, \mathrm{lt}\,x\,y$.
List.lex_eq_true_iff_lex
theorem
[DecidableEq α] (lt : α → α → Bool) : lex l₁ l₂ lt = true ↔ Lex (fun x y => lt x y) l₁ l₂
Full source
/-- Variant of `lex_eq_true_iff` using an arbitrary comparator. -/
@[simp] theorem lex_eq_true_iff_lex [DecidableEq α] (lt : α → α → Bool) :
lexlex l₁ l₂ lt = true ↔ Lex (fun x y => lt x y) l₁ l₂ := by
simp [lex_eq_decide_lex]Informal description
For any type $\alpha$ with decidable equality and any boolean-valued comparison function $\mathrm{lt} : \alpha \to \alpha \to \mathrm{Bool}$, the lexicographic comparison $\mathrm{lex}(l_1, l_2, \mathrm{lt})$ returns $\mathrm{true}$ if and only if the list $l_1$ is lexicographically less than $l_2$ with respect to the relation $\lambda x y, \mathrm{lt}(x, y)$.
List.lex_eq_false_iff_not_lex
theorem
[DecidableEq α] (lt : α → α → Bool) : lex l₁ l₂ lt = false ↔ ¬Lex (fun x y => lt x y) l₁ l₂
Full source
/-- Variant of `lex_eq_false_iff` using an arbitrary comparator. -/
@[simp] theorem lex_eq_false_iff_not_lex [DecidableEq α] (lt : α → α → Bool) :
lexlex l₁ l₂ lt = false ↔ ¬ Lex (fun x y => lt x y) l₁ l₂ := by
simp [Bool.eq_false_iff, lex_eq_true_iff_lex]Informal description
For any type $\alpha$ with decidable equality and any boolean-valued comparison function $\mathrm{lt} : \alpha \to \alpha \to \mathrm{Bool}$, the lexicographic comparison of two lists $l_1$ and $l_2$ using $\mathrm{lt}$ returns $\mathrm{false}$ if and only if the lists are not in lexicographic order with respect to the relation $\lambda x y, \mathrm{lt}\,x\,y$.
List.lex_eq_true_iff_lt
theorem
[DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : lex l₁ l₂ = true ↔ l₁ < l₂
Full source
@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : List α} : lexlex l₁ l₂ = true ↔ l₁ < l₂ := by
simp only [lex_eq_true_iff_lex, decide_eq_true_eq]
exact Iff.rflInformal description
For a type $\alpha$ with decidable equality and a decidable "less than" relation, and for any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic comparison function `lex` returns `true` if and only if $l_1$ is lexicographically less than $l_2$.
List.lex_eq_false_iff_ge
theorem
[DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : lex l₁ l₂ = false ↔ l₂ ≤ l₁
Full source
@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
{l₁ l₂ : List α} : lexlex l₁ l₂ = false ↔ l₂ ≤ l₁ := by
simp only [lex_eq_false_iff_not_lex, decide_eq_true_eq]
exact Iff.rflInformal description
For a type $\alpha$ with decidable equality and a decidable less-than relation, and for any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic comparison function `lex` returns `false` if and only if $l_2$ is less than or equal to $l_1$ in the lexicographic order.
List.lex_eq_true_iff_exists
theorem
[BEq α] (lt : α → α → Bool) :
lex l₁ l₂ lt = true ↔
(l₁.isEqv (l₂.take l₁.length) (· == ·) ∧ l₁.length < l₂.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) → l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i])
Full source
/--
`l₁` is lexicographically less than `l₂` if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length`,
and `l₁` is shorter than `l₂` or
- there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₁[i] < l₂[i]`
-/
theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
lexlex l₁ l₂ lt = true ↔
(l₁.isEqv (l₂.take l₁.length) (· == ·) ∧ l₁.length < l₂.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) →
l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i]) := by
induction l₁ generalizing l₂ with
| nil =>
cases l₂ with
| nil => simp [lex]
| cons b bs => simp [lex]
| cons a l₁ ih =>
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [cons_lex_cons, Bool.or_eq_true, Bool.and_eq_true, ih, isEqv, length_cons]
constructor
· rintro (hab | ⟨hab, ⟨h₁, h₂⟩ | ⟨i, h₁, h₂, w₁, w₂⟩⟩)
· exact .inr ⟨0, by simp [hab]⟩
· exact .inl ⟨⟨hab, h₁⟩, by simpa using h₂⟩
· refine .inr ⟨i + 1, by simp [h₁],
by simp [h₂], ?_, ?_⟩
· intro j hj
cases j with
| zero => simp [hab]
| succ j =>
simp only [getElem_cons_succ]
rw [w₁]
simpa using hj
· simpa using w₂
· rintro (⟨⟨h₁, h₂⟩, h₃⟩ | ⟨i, h₁, h₂, w₁, w₂⟩)
· exact .inr ⟨h₁, .inl ⟨h₂, by simpa using h₃⟩⟩
· cases i with
| zero =>
left
simpa using w₂
| succ i =>
right
refine ⟨by simpa using w₁ 0 (by simp), ?_⟩
right
refine ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
· intro j hj
simpa using w₁ (j + 1) (by simpa)
· simpa using w₂Informal description
For a type $\alpha$ with a boolean equality relation `==` and a boolean-valued comparison function `lt`, and for any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic comparison function `lex` returns `true` if and only if either:
1. $l_1$ is pairwise equivalent under `==` to the first $|l_1|$ elements of $l_2$ (i.e., $l_2.\text{take}(|l_1|)$), and $l_1$ is shorter than $l_2$, or
2. There exists an index $i$ such that:
- For all $j < i$, the $j$-th elements of $l_1$ and $l_2$ are equal under `==`, and
- The $i$-th element of $l_1$ is less than the $i$-th element of $l_2$ under `lt`.
List.lex_eq_false_iff_exists
theorem
[BEq α] [PartialEquivBEq α] (lt : α → α → Bool) (lt_irrefl : ∀ x y, x == y → lt x y = false)
(lt_asymm : ∀ x y, lt x y = true → lt y x = false) (lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y) :
lex l₁ l₂ lt = false ↔
(l₂.isEqv (l₁.take l₂.length) (· == ·)) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) → l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₂[i] l₁[i])
Full source
/--
`l₁` is *not* lexicographically less than `l₂`
(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length` or
- there exists an index `i` such that
- for all `j < i`, `l₁[j] == l₂[j]` and
- `l₂[i] < l₁[i]`
This formulation requires that `==` and `lt` are compatible in the following senses:
- `==` is symmetric
(we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
- `lt` is irreflexive with respect to `==` (i.e. if `x == y` then `lt x y = false`
- `lt` is asymmmetric (i.e. `lt x y = true → lt y x = false`)
- `lt` is antisymmetric with respect to `==` (i.e. `lt x y = false → lt y x = false → x == y`)
-/
theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α → Bool)
(lt_irrefl : ∀ x y, x == y → lt x y = false)
(lt_asymm : ∀ x y, lt x y = true → lt y x = false)
(lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y) :
lexlex l₁ l₂ lt = false ↔
(l₂.isEqv (l₁.take l₂.length) (· == ·)) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) →
l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₂[i] l₁[i]) := by
induction l₁ generalizing l₂ with
| nil =>
cases l₂ with
| nil => simp [lex]
| cons b bs => simp [lex]
| cons a l₁ ih =>
cases l₂ with
| nil => simp [lex]
| cons b l₂ =>
simp [cons_lex_cons, Bool.or_eq_false_iff, Bool.and_eq_false_imp, ih, isEqv,
Bool.and_eq_true, length_cons]
constructor
· rintro ⟨hab, h⟩
if eq : b == a then
specialize h (BEq.symm eq)
obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h
· exact .inl ⟨eq, h⟩
· refine .inr ⟨i + 1, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
· intro j hj
cases j with
| zero => simpa using BEq.symm eq
| succ j =>
simp only [getElem_cons_succ]
rw [w₁]
simpa using hj
· simpa using w₂
else
right
have hba : lt b a :=
Decidable.byContradiction fun hba => eq (lt_antisymm _ _ (by simpa using hba) hab)
exact ⟨0, by simp, by simp, by simpa⟩
· rintro (⟨eq, h⟩ | ⟨i, h₁, h₂, w₁, w₂⟩)
· exact ⟨lt_irrefl _ _ (BEq.symm eq), fun _ => .inl h⟩
· cases i with
| zero =>
simp at w₂
refine ⟨lt_asymm _ _ w₂, ?_⟩
intro eq
exfalso
simp [lt_irrefl _ _ (BEq.symm eq)] at w₂
| succ i =>
refine ⟨lt_irrefl _ _ (by simpa using w₁ 0 (by simp)), ?_⟩
refine fun _ => .inr ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
· intro j hj
simpa using w₁ (j + 1) (by simpa)
· simpa using w₂Informal description
Let $\alpha$ be a type with a boolean equality relation `==` that forms a partial equivalence relation (symmetric and transitive), and a boolean less-than relation `lt` that is irreflexive with respect to `==` (i.e., if $x == y$ then $\text{lt}(x, y) = \text{false}$), asymmetric (i.e., if $\text{lt}(x, y) = \text{true}$ then $\text{lt}(y, x) = \text{false}$), and antisymmetric with respect to `==` (i.e., if $\text{lt}(x, y) = \text{false}$ and $\text{lt}(y, x) = \text{false}$ then $x == y$).
For any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic comparison function $\text{lex}(l_1, l_2, \text{lt})$ returns $\text{false}$ if and only if either:
1. $l_2$ is pairwise equivalent under `==` to the initial segment of $l_1$ of length $l_2.\text{length}$, or
2. There exists an index $i$ such that:
- For all $j < i$, the $j$-th elements of $l_1$ and $l_2$ are equivalent under `==`, and
- The $i$-th element of $l_2$ is less than the $i$-th element of $l_1$ under `lt$.
List.lt_iff_exists
theorem
[DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
l₁ < l₂ ↔
(l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) → l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i])
Full source
protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
l₁ < l₂ ↔
(l₁ = l₂.take l₁.length ∧ l₁.length < l₂.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) →
l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists]
simpInformal description
Let $\alpha$ be a type with decidable equality and a decidable strict order $<$. For any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic order satisfies $l_1 < l_2$ if and only if either:
1. $l_1$ is equal to the initial segment of $l_2$ of length $|l_1|$ (i.e., $l_1 = l_2.\text{take}(|l_1|)$) and $|l_1| < |l_2|$, or
2. There exists an index $i$ such that:
- For all $j < i$, the $j$-th elements of $l_1$ and $l_2$ are equal, and
- The $i$-th element of $l_1$ is strictly less than the $i$-th element of $l_2$.
List.le_iff_exists
theorem
[DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬· < · : α → α → Prop)] {l₁ l₂ : List α} :
l₁ ≤ l₂ ↔
(l₁ = l₂.take l₁.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) → l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i])
Full source
protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
l₁ ≤ l₂ ↔
(l₁ = l₂.take l₁.length) ∨
(∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
(∀ j, (hj : j < i) →
l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i]) := by
rw [← lex_eq_false_iff_ge, lex_eq_false_iff_exists]
· simp only [isEqv_eq, beq_iff_eq, decide_eq_true_eq]
simp only [eq_comm]
conv => lhs; simp +singlePass [exists_comm]
· simpa using Std.Irrefl.irrefl
· simpa using Std.Asymm.asymm
· simpa using Std.Antisymm.antisymmInformal description
Let $\alpha$ be a type with decidable equality and a decidable strict order relation $<$ that is irreflexive, asymmetric, and whose negation is antisymmetric. For any two lists $l_1$ and $l_2$ of elements of $\alpha$, the lexicographic order satisfies $l_1 \leq l_2$ if and only if either:
1. $l_1$ is equal to the initial segment of $l_2$ of length $l_1.\text{length}$, or
2. There exists an index $i$ such that:
- For all $j < i$, the $j$-th elements of $l_1$ and $l_2$ are equal, and
- The $i$-th element of $l_1$ is less than the $i$-th element of $l_2$ under $<$.
List.append_left_lt
theorem
[LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) : l₁ ++ l₂ < l₁ ++ l₃
Full source
theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
l₁ ++ l₂ < l₁ ++ l₃ := by
induction l₁ with
| nil => simp [h]
| cons a l₁ ih => simp [cons_lt_cons_iff, ih]Informal description
For any type $\alpha$ with a strict order relation $<$, and for any lists $l_1, l_2, l_3$ of elements of $\alpha$, if $l_2 < l_3$ in the lexicographic order, then the concatenated list $l_1 ++ l_2$ is lexicographically less than $l_1 ++ l_3$.
List.append_left_le
theorem
[DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬· < · : α → α → Prop)] {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) : l₁ ++ l₂ ≤ l₁ ++ l₃
Full source
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)]
{l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) :
l₁ ++ l₂ ≤ l₁ ++ l₃ := by
induction l₁ with
| nil => simp [h]
| cons a l₁ ih => simp [cons_le_cons_iff, ih]Informal description
Let $\alpha$ be a type with a decidable equality and a decidable strict order relation $<$ that is irreflexive, asymmetric, and whose negation is antisymmetric. For any lists $l_1, l_2, l_3$ of elements of $\alpha$, if $l_2 \leq l_3$ in the lexicographic order, then the concatenated list $l_1 ++ l_2$ is lexicographically less than or equal to $l_1 ++ l_3$.
List.le_append_left
theorem
[LT α] [Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} : l₁ ≤ l₁ ++ l₂
Full source
theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)]
{l₁ l₂ : List α} : l₁ ≤ l₁ ++ l₂ := by
intro h
match l₁, h with
| nil, h => simp at h
| cons a l₁, h => exact le_append_left (by simpa using h)Informal description
For any type $\alpha$ with a strict order relation $<$ that is irreflexive, and for any lists $l_1, l_2$ of elements of $\alpha$, the list $l_1$ is lexicographically less than or equal to the concatenated list $l_1 ++ l_2$.
List.IsPrefix.le
theorem
[LT α] [Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁ ≤ l₂
Full source
theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : α → α → Prop)]
{l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁ ≤ l₂ := by
rcases h with ⟨_, rfl⟩
apply le_append_leftInformal description
For any type $\alpha$ with a strict order relation $<$ that is irreflexive, and for any lists $l_1, l_2$ of elements of $\alpha$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then $l_1$ is lexicographically less than or equal to $l_2$ (denoted $l_1 \leq l_2$).
List.map_lt
theorem
[LT α] [LT β] {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) : map f l₁ < map f l₂
Full source
protected theorem map_lt [LT α] [LT β]
{l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
map f l₁ < map f l₂ := by
match l₁, l₂, h with
| nil, nil, h => simp at h
| nil, cons b l₂, h => simp
| cons a l₁, nil, h => simp at h
| cons a l₁, cons _ l₂, .cons h =>
simp [cons_lt_cons_iff, List.map_lt w (by simpa using h)]
| cons a l₁, cons b l₂, .rel h =>
simp [cons_lt_cons_iff, w, h]Informal description
Let $\alpha$ and $\beta$ be types equipped with a "less than" relation, and let $f : \alpha \to \beta$ be a function that preserves the strict order (i.e., for any $x, y \in \alpha$, if $x < y$ then $f(x) < f(y)$). If $l_1$ and $l_2$ are lists over $\alpha$ such that $l_1$ is lexicographically less than $l_2$, then the list obtained by applying $f$ to each element of $l_1$ is lexicographically less than the list obtained by applying $f$ to each element of $l_2$.
List.map_le
theorem
[DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬· < · : α → α → Prop)] [Std.Irrefl (· < · : β → β → Prop)]
[Std.Asymm (· < · : β → β → Prop)] [Std.Antisymm (¬· < · : β → β → Prop)] {l₁ l₂ : List α} {f : α → β}
(w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) : map f l₁ ≤ map f l₂
Full source
protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β]
[Std.Irrefl (· < · : α → α → Prop)]
[Std.Asymm (· < · : α → α → Prop)]
[Std.Antisymm (¬ · < · : α → α → Prop)]
[Std.Irrefl (· < · : β → β → Prop)]
[Std.Asymm (· < · : β → β → Prop)]
[Std.Antisymm (¬ · < · : β → β → Prop)]
{l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
map f l₁ ≤ map f l₂ := by
rw [List.le_iff_exists] at h ⊢
obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h
· left
rw [h]
simp
· right
refine ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩
· simp +contextual [w₁]
· simpa using w _ _ w₂Informal description
Let $\alpha$ and $\beta$ be types with decidable equality and decidable strict order relations $<_\alpha$ and $<_\beta$ that are irreflexive, asymmetric, and whose negations are antisymmetric. Given two lists $l_1, l_2$ of elements of $\alpha$ and a function $f : \alpha \to \beta$ that preserves the strict order (i.e., for any $x, y \in \alpha$, if $x <_\alpha y$ then $f(x) <_\beta f(y)$), if $l_1$ is lexicographically less than or equal to $l_2$ under $<_\alpha$, then the mapped lists $f(l_1)$ and $f(l_2)$ are lexicographically less than or equal under $<_\beta$.