From e06673e200823777b114c8f1733772a95bb8d2e1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 20 Dec 2024 17:16:27 +1100 Subject: [PATCH] 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 | 2 +- src/Init/Data/Array/Lex/Lemmas.lean | 83 +++++++++++++++++--- src/Init/Data/List/Lex.lean | 113 +++++++++++++++++++++++++--- src/Init/Data/String/Lemmas.lean | 2 +- src/Init/Data/Vector/Lemmas.lean | 2 +- src/Init/Data/Vector/Lex.lean | 59 +++++++++++++-- 6 files changed, 233 insertions(+), 28 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 726fff9edebf..655b4ad609b9 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index cf4bdc379e62..7f6a1fb0c905 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean index d006105039ab..3737d082f308 100644 --- a/src/Init/Data/List/Lex.lean +++ b/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 diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean index d13cadd13ad8..ddbeface6306 100644 --- a/src/Init/Data/String/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index f9a85fd66b50..0f91c8ba9dae 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 3d4f3a296bc2..3a364334be13 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -57,6 +57,7 @@ protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] instance ltIrrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Irrefl (α := Vector α n) (· < ·) where irrefl := Vector.lt_irrefl +@[simp] theorem not_lt_empty [LT α] (l : Vector α 0) : ¬ l < #v[] := Array.not_lt_empty l.toArray @[simp] theorem empty_le [LT α] (l : Vector α 0) : #v[] ≤ l := Array.empty_le l.toArray @[simp] theorem le_empty [LT α] (l : Vector α 0) : l ≤ #v[] ↔ l = #v[] := by @@ -69,12 +70,12 @@ protected theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Pr instance [LT α] [Std.Irrefl (· < · : α → α → Prop)] : Std.Refl (· ≤ · : Vector α n → Vector α n → Prop) where refl := Vector.le_refl -protected theorem lt_trans [LT α] [DecidableLT α] +protected theorem lt_trans [LT α] [i₁ : Trans (· < · : α → α → Prop) (· < ·) (· < ·)] {l₁ l₂ l₃ : Vector α n} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := Array.lt_trans h₁ h₂ -instance [LT α] [DecidableLT α] +instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] : Trans (· < · : Vector α n → Vector α n → Prop) (· < ·) (· < ·) where trans h₁ h₂ := Vector.lt_trans h₁ h₂ @@ -103,7 +104,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α] Trans (· ≤ · : Vector α n → Vector α n → Prop) (· ≤ ·) (· ≤ ·) where trans h₁ h₂ := Vector.le_trans h₁ h₂ -protected theorem lt_asymm [DecidableEq α] [LT α] [DecidableLT α] +protected theorem lt_asymm [LT α] [i : Std.Asymm (· < · : α → α → Prop)] {l₁ l₂ : Vector α n} (h : l₁ < l₂) : ¬ l₂ < l₁ := Array.lt_asymm h @@ -113,13 +114,31 @@ instance [DecidableEq α] [LT α] [DecidableLT α] asymm _ _ := Vector.lt_asymm protected theorem le_total [DecidableEq α] [LT α] [DecidableLT α] - [i : Std.Total (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ∨ l₂ ≤ l₁ := - Array.le_total + [i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : Vector α n) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ := + Array.le_total _ _ instance [DecidableEq α] [LT α] [DecidableLT α] [Std.Total (¬ · < · : α → α → Prop)] : Std.Total (· ≤ · : Vector α n → Vector α n → Prop) where - total _ _ := Vector.le_total + total := Vector.le_total + +@[simp] protected theorem not_lt [LT α] + {l₁ l₂ : Vector α n} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl + +@[simp] protected theorem not_le [DecidableEq α] [LT α] [DecidableLT α] + {l₁ l₂ : Vector α n} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Decidable.not_not + +protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α] + [i : Std.Total (¬ · < · : α → α → Prop)] + {l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ ≤ l₂ := + Array.le_of_lt h + +theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] + [Std.Irrefl (· < · : α → α → Prop)] + [Std.Antisymm (¬ · < · : α → α → Prop)] + [Std.Total (¬ · < · : α → α → Prop)] + {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by + simpa using Array.le_iff_lt_or_eq (l₁ := l₁.toArray) (l₂ := l₂.toArray) @[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} : lex l₁ l₂ = true ↔ l₁ < l₂ := by @@ -199,4 +218,32 @@ theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] rcases l₂ with ⟨l₂, n₂⟩ simp [Array.le_iff_exists, ← n₂] +theorem append_left_lt [LT α] {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ < l₃) : + l₁ ++ l₂ < l₁ ++ l₃ := by + simpa using Array.append_left_lt h + +theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α] + [Std.Irrefl (· < · : α → α → Prop)] + [Std.Asymm (· < · : α → α → Prop)] + [Std.Antisymm (¬ · < · : α → α → Prop)] + {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ ≤ l₃) : + l₁ ++ l₂ ≤ l₁ ++ l₃ := by + simpa using Array.append_left_le h + +theorem map_lt [LT α] [LT β] + {l₁ l₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ < l₂) : + map f l₁ < map f l₂ := by + simpa using Array.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₂ : Vector α n} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) : + map f l₁ ≤ map f l₂ := by + simpa using Array.map_le w h + end Vector