Shortlex ordering of lists.

Given a relation r on α, the shortlex order on List α is defined by L < M iff

• L.length < M.length
• L.length = M.length and L < M under the lexicographic ordering over r on lists

Main results

We show that if r is well-founded, so too is the shortlex order over r

See also

Related files are:

• Mathlib/Data/List/Lex.lean: Lexicographic order on List α.
• Mathlib/Data/DFinsupp/WellFounded.lean: Well-foundedness of lexicographic orders on DFinsupp and Pi.

shortlex ordering

def List.Shortlex {α : Type u_1} (r : α → α → Prop) : List α → List α → Prop

Given a relation r on α, the shortlex order on List α, for which [a0, ..., an] < [b0, ..., b_k] if n < k or n = k and [a0, ..., an] < [b0, ..., bk] under the lexicographic order induced by r.

Equations

• List.Shortlex r = InvImage (Prod.Lex (fun (x1 x2 : ℕ) => x1 < x2) (List.Lex r)) fun (a : List α) => (a.length, a)

theorem List.Shortlex.of_length_lt {α : Type u_1} {r : α → α → Prop} {s t : List α} (h : s.length < t.length) : Shortlex r s t

If a list s is shorter than a list t, then s is smaller than t under any shortlex order.

theorem List.Shortlex.of_lex {α : Type u_1} {r : α → α → Prop} {s t : List α} (len_eq : s.length = t.length) (h_lex : Lex r s t) : Shortlex r s t

If two lists s and t have the same length, s is smaller than t under the shortlex order over a relation r when s is smaller than t under the lexicographic order over r

theorem List.shortlex_def {α : Type u_1} {r : α → α → Prop} {s t : List α} : Shortlex r s t ↔ s.length < t.length ∨ s.length = t.length ∧ Lex r s t

theorem List.shortlex_iff_lex {α : Type u_1} {r : α → α → Prop} {s t : List α} (h : s.length = t.length) : Shortlex r s t ↔ Lex r s t

If two lists s and t have the same length, s is smaller than t under the shortlex order over a relation r exactly when s is smaller than t under the lexicographic order over r.

theorem List.shortlex_cons_iff {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {a : α} {s t : List α} : Shortlex r (a :: s) (a :: t) ↔ Shortlex r s t

theorem List.Shortlex.cons {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {a : α} {s t : List α} : Shortlex r s t → Shortlex r (a :: s) (a :: t)

Alias of the reverse direction of List.shortlex_cons_iff.

theorem List.Shortlex.of_cons {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {a : α} {s t : List α} : Shortlex r (a :: s) (a :: t) → Shortlex r s t

Alias of the forward direction of List.shortlex_cons_iff.

@[simp]

theorem List.not_shortlex_nil_right {α : Type u_1} {r : α → α → Prop} {s : List α} : ¬Shortlex r s []

theorem List.shortlex_nil_or_eq_nil {α : Type u_1} {r : α → α → Prop} (s : List α) : Shortlex r [] s ∨ s = []

@[simp]

theorem List.shortlex_singleton_iff {α : Type u_1} {r : α → α → Prop} (a b : α) : Shortlex r [a] [b] ↔ r a b

instance List.Shortlex.isTrichotomous {α : Type u_1} {r : α → α → Prop} [IsTrichotomous α r] : IsTrichotomous (List α) (Shortlex r)

instance List.Shortlex.isAsymm {α : Type u_1} {r : α → α → Prop} [IsAsymm α r] : IsAsymm (List α) (Shortlex r)

theorem List.Shortlex.append_right {α : Type u_1} {r : α → α → Prop} {s₁ s₂ : List α} (t : List α) (h : Shortlex r s₁ s₂) : Shortlex r s₁ (s₂ ++ t)

theorem List.Shortlex.append_left {α : Type u_1} {r : α → α → Prop} {t₁ t₂ : List α} (h : Shortlex r t₁ t₂) (s : List α) : Shortlex r (s ++ t₁) (s ++ t₂)

theorem List.Shortlex.wf {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : WellFounded (Shortlex r)