feat: lemmas about List/Array/Vector lexicographic order (#6423)

This PR adds missing lemmas about lexicographic order on
List/Array/Vector.

src/Init/Data/Array/Lemmas.lean

@@ -27,7 +27,7 @@ namespace Array
 
 /-! ### toList -/
 
-theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
+@[simp] theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
   cases a; cases b; simp
 
 @[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by

src/Init/Data/Array/Lex/Lemmas.lean

@@ -11,8 +11,11 @@ namespace Array
 
 /-! ### Lexicographic ordering -/
 
-@[simp] theorem lt_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
-@[simp] theorem le_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+@[simp] theorem _root_.List.lt_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem _root_.List.le_toArray [LT α] (l₁ l₂ : List α) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+
+@[simp] theorem lt_toList [LT α] (l₁ l₂ : Array α) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem le_toList [LT α] (l₁ l₂ : Array α) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl
 
 theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
@@ -59,6 +62,7 @@ protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)]
 instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := Array α) (· < ·) where
   irrefl := Array.lt_irrefl
 
+@[simp] theorem not_lt_empty [LT α] (l : Array α) : ¬ l < #[] := List.not_lt_nil l.toList
 @[simp] theorem empty_le [LT α] (l : Array α) : #[] ≤ l := List.nil_le l.toList
 
 @[simp] theorem le_empty [LT α] (l : Array α) : l ≤ #[] ↔ l = #[] := by
@@ -74,13 +78,12 @@ protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Pr
 instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : Array α → Array α → Prop) where
   refl := Array.le_refl
 
-protected theorem lt_trans [LT α] [DecidableLT α]
+protected theorem lt_trans [LT α]
     [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
     {l₁ l₂ l₃ : Array α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
   List.lt_trans h₁ h₂
 
-instance [LT α] [DecidableLT α]
-    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
+instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
     Trans (· < · : Array α → Array α → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := Array.lt_trans h₁ h₂
 
@@ -108,7 +111,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     Trans (· ≤ · : Array α → Array α → Prop) (· ≤ ·) (· ≤ ·) where
   trans h₁ h₂ := Array.le_trans h₁ h₂
 
-protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem lt_asymm [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : Array α} (h : l₁ < l₂) : ¬ l₂ < l₁ := List.lt_asymm h
 
@@ -118,13 +121,31 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
   asymm _ _ := Array.lt_asymm
 
 protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : Array α} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
-  List.le_total
+    [i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : Array α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  List.le_total _ _
+
+@[simp] protected theorem not_lt [LT α]
+    {l₁ l₂ : Array α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+
+@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : Array α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not
+
+protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
+    [i : Std.Total (¬ · < · : α → α → Prop)]
+    {l₁ l₂ : Array α} (h : l₁ < l₂) : l₁ ≤ l₂ :=
+  List.le_of_lt h
+
+theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Std.Total (¬ · < · : α → α → Prop)]
+    {l₁ l₂ : Array α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by
+  simpa using List.le_iff_lt_or_eq (l₁ := l₁.toList) (l₂ := l₂.toList)
 
 instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Total (¬ · < · : α → α → Prop)] :
     Std.Total (· ≤ · : Array α → Array α → Prop) where
-  total _ _ := Array.le_total
+  total := Array.le_total
 
 @[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
     {l₁ l₂ : Array α} : lex l₁ l₂ = true ↔ l₁ < l₂ := by
@@ -213,4 +234,48 @@ theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
   cases l₂
   simp [List.le_iff_exists]
 
+theorem append_left_lt [LT α] {l₁ l₂ l₃ : Array α} (h : l₂ < l₃) :
+    l₁ ++ l₂ < l₁ ++ l₃ := by
+  cases l₁
+  cases l₂
+  cases l₃
+  simpa using List.append_left_lt h
+
+theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
+    [Std.Irrefl (· < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    {l₁ l₂ l₃ : Array α} (h : l₂ ≤ l₃) :
+    l₁ ++ l₂ ≤ l₁ ++ l₃ := by
+  cases l₁
+  cases l₂
+  cases l₃
+  simpa using List.append_left_le h
+
+theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)]
+    {l₁ l₂ : Array α} : l₁ ≤ l₁ ++ l₂ := by
+  cases l₁
+  cases l₂
+  simpa using List.le_append_left
+
+theorem map_lt [LT α] [LT β]
+    {l₁ l₂ : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) :
+    map f l₁ < map f l₂ := by
+  cases l₁
+  cases l₂
+  simpa using List.map_lt w h
+
+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₂ : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :
+    map f l₁ ≤ map f l₂ := by
+  cases l₁
+  cases l₂
+  simpa using List.map_le w h
+
 end Array

src/Init/Data/List/Lex.lean

@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 prelude
 import Init.Data.List.Lemmas
+import Init.Data.List.Nat.TakeDrop
 
 namespace List
 
@@ -33,6 +34,7 @@ instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irre
 
 @[simp] theorem not_lex_nil : ¬Lex r l [] := fun h => nomatch h
 
+@[simp] theorem not_lt_nil [LT α] (l : List α) : ¬ l < [] := fun h => nomatch h
 @[simp] theorem nil_le [LT α] (l : List α) : [] ≤ l := fun h => nomatch h
 
 @[simp] theorem not_nil_lex_iff : ¬Lex r [] l ↔ l = [] := by
@@ -59,6 +61,10 @@ theorem cons_lt_cons_iff [LT α] {a b} {l₁ l₂ : List α} :
   dsimp only [instLT, List.lt]
   simp [cons_lex_cons_iff]
 
+@[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]
+
 theorem not_cons_lex_cons_iff [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₂) := by
   rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]
@@ -120,7 +126,7 @@ protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Pr
 instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : List α → List α → Prop) where
   refl := List.le_refl
 
-theorem lex_trans {r : α → α → Prop} [DecidableRel r]
+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
@@ -137,14 +143,13 @@ theorem lex_trans {r : α → α → Prop} [DecidableRel r]
     | .cons ih =>
       exact List.Lex.cons (ih2 ih)
 
-protected theorem lt_trans [LT α] [DecidableLT α]
+protected theorem lt_trans [LT α]
     [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
   simp only [instLT, List.lt] at h₁ h₂ ⊢
   exact lex_trans (fun h₁ h₂ => i₁.trans h₁ h₂) h₁ h₂
 
-instance [LT α] [DecidableLT α]
-    [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
+instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
     Trans (· < · : List α → List α → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := List.lt_trans h₁ h₂
 
@@ -197,7 +202,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     Trans (· ≤ · : List α → List α → Prop) (· ≤ ·) (· ≤ ·) where
   trans h₁ h₂ := List.le_trans h₁ h₂
 
-theorem lex_asymm {r : α → α → Prop} [DecidableRel r]
+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₁ =>
@@ -209,12 +214,11 @@ theorem lex_asymm {r : α → α → Prop} [DecidableRel r]
     | .rel h₂ => h h₂ h₂
     | .cons h₂ => lex_asymm h h₁ h₂
 
-protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α]
+protected theorem lt_asymm [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} (h : l₁ < l₂) : ¬ l₂ < l₁ := lex_asymm (i.asymm _ _) h
 
-instance [DecidableEq α] [LT α] [DecidableLT α]
-    [Std.Asymm (· < · : α → α → Prop)] :
+instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
     Std.Asymm (· < · : List α → List α → Prop) where
   asymm _ _ := List.lt_asymm
 
@@ -234,13 +238,43 @@ theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
     obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction
 
 protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+    [i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
   not_lex_total i.total l₂ l₁
 
 instance [DecidableEq α] [LT α] [DecidableLT α]
     [Std.Total (¬ · < · : α → α → Prop)] :
     Std.Total (· ≤ · : List α → List α → Prop) where
-  total _ _ := List.le_total
+  total := List.le_total
+
+@[simp] protected theorem not_lt [LT α]
+    {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+
+@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α]
+    {l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not
+
+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' h
+
+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₁
 
 theorem lex_eq_decide_lex [DecidableEq α] (lt : α → α → Bool) :
     lex l₁ l₂ lt = decide (Lex (fun x y => lt x y) l₁ l₂) := by
@@ -427,4 +461,63 @@ theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
   · simpa using Std.Asymm.asymm
   · simpa using Std.Antisymm.antisymm
 
+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]
+
+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]
+
+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)
+
+theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : α → α → Prop)]
+    {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁ ≤ l₂ := by
+  rcases h with ⟨_, rfl⟩
+  apply le_append_left
+
+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, map_lt w (by simpa using h)]
+  | cons a l₁, cons b l₂, .rel h =>
+    simp [cons_lt_cons_iff, w, h]
+
+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 [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₂
+
 end List

src/Init/Data/String/Lemmas.lean

@@ -23,7 +23,7 @@ attribute [local instance] Char.notLTTrans Char.notLTAntisymm Char.notLTTotal
 
 protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
 protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
-protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total
+protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
 protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.data) (bs := b.data) h₁ h₂)
 protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
 protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by

src/Init/Data/Vector/Lemmas.lean

@@ -247,7 +247,7 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
 
-theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
+@[simp] theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
   cases v
   cases w
   simp