feat: replace List.lt with List.Lex (#6379)

This PR replaces `List.lt` with `List.Lex`, from Mathlib, and adds the
new `Bool` valued lexicographic comparatory function `List.lex`. This
subtly changes the definition of `<` on Lists in some situations.

`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b`
are merely incomparable
(either neither `a < b` nor `b < a`), whereas according to `List.Lex`
this would require `a = b`.

When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then
the two relations coincide.

Mathlib was already overriding the order instances for `List α`,
so this change should not be noticed by anyone already using Mathlib.

We simultaneously add the boolean valued `List.lex` function,
parameterised by a `BEq` typeclass
and an arbitrary `lt` function. This will support the flexibility
previously provided for `List.lt`,
via a `==` function which is weaker than strict equality.

doc/examples/ICERM2022/meta.lean

@@ -29,7 +29,7 @@ def ex3 (declName : Name) : MetaM Unit := do
     for x in xs do
       trace[Meta.debug] "{x} : {← inferType x}"
 
-def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
+def myMin [LT α] [DecidableLT α] (a b : α) : α :=
   if a < b then
     a
   else

releases_drafts/list_lex.md

@@ -0,0 +1,16 @@
+We replace the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib.
+(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.)
+This subtely changes the notion of ordering on `List α`.
+
+`List.lt` was a weaker relation: in particular if `l₁ < l₂`, then
+`a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable
+(either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`.
+
+When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide.
+
+Mathlib was already overriding the order instances for `List α`,
+so this change should not be noticed by anyone already using Mathlib.
+
+We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass
+and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`,
+via a `==` function which is weaker than strict equality.

src/Init/Core.lean

@@ -2116,14 +2116,37 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
+/-- `IsRefl X r` means the binary relation `r` on `X` is reflexive. -/
+class Refl (r : α → α → Prop) : Prop where
+  /-- A reflexive relation satisfies `r a a`. -/
+  refl : ∀ a, r a a
+
 /--
 `Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
 -/
 class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
+  antisymm (a b : α) : r a b → r b a → a = b
 
 @[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
 abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
 
+/-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
+`r a b → ¬ r b a`. -/
+class Asymm (r : α → α → Prop) : Prop where
+  /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
+  asymm : ∀ a b, r a b → ¬r b a
+
+/-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
+`x y : X` we have `r x y` or `r y x`. -/
+class Total (r : α → α → Prop) : Prop where
+  /-- A total relation satisfies `r a b ∨ r b a`. -/
+  total : ∀ a b, r a b ∨ r b a
+
+/-- `Irrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
+holds). -/
+class Irrefl (r : α → α → Prop) : Prop where
+  /-- An irreflexive relation satisfies `¬ r a a`. -/
+  irrefl : ∀ a, ¬r a a
+
 end Std

src/Init/Data/Array.lean

@@ -22,3 +22,4 @@ import Init.Data.Array.Monadic
 import Init.Data.Array.FinRange
 import Init.Data.Array.Perm
 import Init.Data.Array.Find
+import Init.Data.Array.Lex

src/Init/Data/Array/Basic.lean

@@ -944,6 +944,19 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Lexicographic ordering -/
+
+instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩
+instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toList⟩
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Array α) :=
+  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList < bs.toList
+
+instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Array α) :=
+  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList ≤ bs.toList
+
+-- See `Init.Data.Array.Lex` for the boolean valued lexicographic comparator.
+
 /-! ## Auxiliary functions used in metaprogramming.
 
 We do not currently intend to provide verification theorems for these functions.

src/Init/Data/Array/Lemmas.lean

@@ -12,6 +12,7 @@ import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
+import Init.Data.Array.Lex
 import Init.TacticsExtra
 import Init.Data.List.ToArray
 
@@ -924,12 +925,26 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
+
+@[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
+  cases xs
+  simp
+
+@[simp] theorem empty_beq_iff [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty := by
+  cases xs
+  simp
+
 @[simp] theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
     (v.push a == w.push b) = (v == w && a == b) := by
   cases v
   cases w
   simp
 
+theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys.size := by
+  cases xs
+  cases ys
+  simp [List.length_eq_of_beq (by simpa using h)]
+
 @[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
     (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
   cases n with
@@ -974,6 +989,8 @@ theorem mem_or_eq_of_mem_setIfInBounds
     · intro a
       apply Array.isEqv_self_beq
 
+/-! ### Lexicographic ordering -/
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl

src/Init/Data/Array/Lex.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range
+
+namespace Array
+
+/--
+Lexicographic comparator for arrays.
+
+`lex as bs lt` is true if
+- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or
+- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
+-/
+def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
+  for h : i in [0 : min as.size bs.size] do
+    -- TODO: `omega` should be able to find this itself.
+    have : i < min as.size bs.size := Membership.get_elem_helper h rfl
+    if lt as[i] bs[i] then
+      return true
+    else if as[i] != bs[i] then
+      return false
+  return as.size < bs.size
+
+end Array

src/Init/Data/Char/Lemmas.lean

@@ -9,6 +9,9 @@ import Init.Data.UInt.Lemmas
 
 namespace Char
 
+@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
+  | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
+
 theorem le_def {a b : Char} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 theorem lt_def {a b : Char} : a < b ↔ a.1 < b.1 := .rfl
 theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
@@ -19,9 +22,44 @@ theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
 protected theorem le_trans {a b c : Char} : a ≤ b → b ≤ c → a ≤ c := UInt32.le_trans
 protected theorem lt_trans {a b c : Char} : a < b → b < c → a < c := UInt32.lt_trans
 protected theorem le_total (a b : Char) : a ≤ b ∨ b ≤ a := UInt32.le_total a.1 b.1
+protected theorem le_antisymm {a b : Char} : a ≤ b → b ≤ a → a = b :=
+  fun h₁ h₂ => Char.ext (UInt32.le_antisymm h₁ h₂)
 protected theorem lt_asymm {a b : Char} (h : a < b) : ¬ b < a := UInt32.lt_asymm h
 protected theorem ne_of_lt {a b : Char} (h : a < b) : a ≠ b := Char.ne_of_val_ne (UInt32.ne_of_lt h)
 
+instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
+  irrefl := Char.lt_irrefl
+
+instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
+  refl := Char.le_refl
+
+instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
+  trans := Char.le_trans
+
+instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·) where
+  trans := Char.lt_trans
+
+-- This instance is useful while setting up instances for `String`.
+def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
+  trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
+
+instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
+  antisymm _ _ := Char.le_antisymm
+
+-- This instance is useful while setting up instances for `String`.
+def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
+  antisymm _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
+
+instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
+  asymm _ _ := Char.lt_asymm
+
+instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
+  total := Char.le_total
+
+-- This instance is useful while setting up instances for `String`.
+def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
+  total := fun x y => by simpa using Char.le_total y x
+
 theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4 := by
   have := c.utf8Size_pos
   have := c.utf8Size_le_four
@@ -31,9 +69,6 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rw [Char.ofNat, dif_pos]
   rfl
 
-@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
-  | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
-
 end Char
 
 @[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size

src/Init/Data/List/Basic.lean

@@ -162,46 +162,74 @@ theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv)
 
 /-! ## Lexicographic ordering -/
 
-/--
-The lexicographic order on lists.
-`[] < a::as`, and `a::as < b::bs` if `a < b` or if `a` and `b` are equivalent and `as < bs`.
--/
-inductive lt [LT α] : List α → List α → Prop where
+/-- Lexicographic ordering for lists. -/
+inductive Lex (r : α → α → Prop) : List α → List α → Prop
   /-- `[]` is the smallest element in the order. -/
-  | nil  (b : α) (bs : List α) : lt [] (b::bs)
+  | nil {a l} : Lex r [] (a :: l)
+  /-- If `a` is indistinguishable from `b` and `as < bs`, then `a::as < b::bs`. -/
+  | cons {a l₁ l₂} (h : Lex r l₁ l₂) : Lex r (a :: l₁) (a :: l₂)
   /-- If `a < b` then `a::as < b::bs`. -/
-  | head {a : α} (as : List α) {b : α} (bs : List α) : a < b → lt (a::as) (b::bs)
-  /-- If `a` and `b` are equivalent and `as < bs`, then `a::as < b::bs`. -/
-  | tail {a : α} {as : List α} {b : α} {bs : List α} : ¬ a < b → ¬ b < a → lt as bs → lt (a::as) (b::bs)
-
-instance [LT α] : LT (List α) := ⟨List.lt⟩
+  | rel {a₁ l₁ a₂ l₂} (h : r a₁ a₂) : Lex r (a₁ :: l₁) (a₂ :: l₂)
 
-instance hasDecidableLt [LT α] [h : DecidableRel (α := α) (· < ·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-  | [],    []    => isFalse nofun
-  | [],    _::_  => isTrue (List.lt.nil _ _)
-  | _::_, []     => isFalse nofun
+instance decidableLex [DecidableEq α] (r : α → α → Prop) [h : DecidableRel r] :
+    (l₁ l₂ : List α) → Decidable (Lex r l₁ l₂)
+  | [], [] => isFalse nofun
+  | [], _::_ => isTrue Lex.nil
+  | _::_, [] => isFalse nofun
   | a::as, b::bs =>
     match h a b with
-    | isTrue h₁  => isTrue (List.lt.head _ _ h₁)
+    | isTrue h₁ => isTrue (Lex.rel h₁)
     | isFalse h₁ =>
-      match h b a with
-      | isTrue h₂  => isFalse (fun h => match h with
-         | List.lt.head _ _ h₁' => absurd h₁' h₁
-         | List.lt.tail _ h₂' _ => absurd h₂ h₂')
-      | isFalse h₂ =>
-        match hasDecidableLt as bs with
-        | isTrue h₃  => isTrue (List.lt.tail h₁ h₂ h₃)
+      if h₂ : a = b then
+        match decidableLex r as bs with
+        | isTrue h₃ => isTrue (h₂ ▸ Lex.cons h₃)
         | isFalse h₃ => isFalse (fun h => match h with
-           | List.lt.head _ _ h₁' => absurd h₁' h₁
-           | List.lt.tail _ _ h₃' => absurd h₃' h₃)
+          | Lex.rel h₁' => absurd h₁' h₁
+          | Lex.cons h₃' => absurd h₃' h₃)
+      else
+        isFalse (fun h => match h with
+          | Lex.rel h₁' => absurd h₁' h₁
+          | Lex.cons h₂' => h₂ rfl)
+
+@[inherit_doc Lex]
+protected abbrev lt [LT α] : List α → List α → Prop := Lex (· < ·)
+
+instance instLT [LT α] : LT (List α) := ⟨List.lt⟩
+
+/-- Decidability of lexicographic ordering. -/
+instance decidableLT [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    Decidable (l₁ < l₂) := decidableLex (· < ·) l₁ l₂
+
+@[deprecated decidableLT (since := "2024-12-13"), inherit_doc decidableLT]
+abbrev hasDecidableLt := @decidableLT
 
 /-- The lexicographic order on lists. -/
 @[reducible] protected def le [LT α] (a b : List α) : Prop := ¬ b < a
 
-instance [LT α] : LE (List α) := ⟨List.le⟩
+instance instLE [LT α] : LE (List α) := ⟨List.le⟩
+
+instance decidableLE [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
+    Decidable (l₁ ≤ l₂) :=
+  inferInstanceAs (Decidable (Not _))
+
+/--
+Lexicographic comparator for lists.
+
+* `lex lt [] (b :: bs)` is true.
+* `lex lt as []` is false.
+* `lex lt (a :: as) (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
+-/
+def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
+  match l₁, l₂ with
+  | [],      _ :: _  => true
+  | _,      []       => false
+  | a :: as, b :: bs => lt a b || (a == b && lex as bs lt)
 
-instance [LT α] [DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
-  fun _ _ => inferInstanceAs (Decidable (Not _))
+@[simp] theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
+@[simp] theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
+@[simp] theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
+@[simp] theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
+    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
 
 /-! ## Alternative getters -/
 

src/Init/Data/List/BasicAux.lean

@@ -233,25 +233,34 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
-    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
+    (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
+    {as bs : List α} (h₁ : ¬ Lex r bs as) (h₂ : ¬ Lex r as bs) : as = bs :=
   match as, bs with
   | [],    []    => rfl
-  | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
-  | _::_, []    => False.elim <| h₁ (List.lt.nil ..)
+  | [],    _::_ => False.elim <| h₂ (List.Lex.nil ..)
+  | _::_, []    => False.elim <| h₁ (List.Lex.nil ..)
   | a::as, b::bs => by
-    by_cases hab : a < b
-    · exact False.elim <| h₂ (List.lt.head _ _ hab)
-    · by_cases hba : b < a
-      · exact False.elim <| h₁ (List.lt.head _ _ hba)
-      · have h₁ : as ≤ bs := fun h => h₁ (List.lt.tail hba hab h)
-        have h₂ : bs ≤ as := fun h => h₂ (List.lt.tail hab hba h)
-        have ih : as = bs := le_antisymm h₁ h₂
-        have : a = b := s.antisymm hab hba
-        simp [this, ih]
-
-instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
+    by_cases hab : r a b
+    · exact False.elim <| h₂ (List.Lex.rel hab)
+    · by_cases eq : a = b
+      · subst eq
+        have h₁ : ¬ Lex r bs as := fun h => h₁ (List.Lex.cons h)
+        have h₂ : ¬ Lex r as bs := fun h => h₂ (List.Lex.cons h)
+        simp [not_lex_antisymm antisymm h₁ h₂]
+      · exfalso
+        by_cases hba : r b a
+        · exact h₁ (Lex.rel hba)
+        · exact eq (antisymm _ _ hab hba)
+
+protected theorem le_antisymm [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Antisymm (¬ · < · : α → α → Prop)]
+    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+  not_lex_antisymm i.antisymm h₁ h₂
+
+instance [DecidableEq α] [LT α] [DecidableLT α]
+    [s : Std.Antisymm (¬ · < · : α → α → Prop)] :
     Std.Antisymm (· ≤ · : List α → List α → Prop) where
-  antisymm h₁ h₂ := le_antisymm h₁ h₂
+  antisymm _ _ h₁ h₂ := List.le_antisymm h₁ h₂
 
 end List