From 39eaa214d464bac67696e7ee1279232f5e199164 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 20 Dec 2024 22:23:56 +1100 Subject: [PATCH] chore: protect some lemmas in List/Array/Vector namespace (#6425) --- src/Init/Data/Array/Lex/Lemmas.lean | 14 +++++++------- src/Init/Data/List/Lex.lean | 18 +++++++++--------- src/Init/Data/Vector/Lex.lean | 15 ++++++++++----- 3 files changed, 26 insertions(+), 21 deletions(-) diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 7f6a1fb0c9..d525ff4248 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -17,8 +17,8 @@ namespace Array @[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 α) : +protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl +protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) : ¬ l₁ ≤ l₂ ↔ l₂ < l₁ := Decidable.not_not @@ -135,7 +135,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} (h : l₁ < l₂) : l₁ ≤ l₂ := List.le_of_lt h -theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] [Std.Total (¬ · < · : α → α → Prop)] @@ -211,7 +211,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α cases l₂ simp_all [List.lex_eq_false_iff_exists] -theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} : +protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} : l₁ < l₂ ↔ (l₁ = l₂.take l₁.size ∧ l₁.size < l₂.size) ∨ (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size), @@ -221,7 +221,7 @@ theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Arr cases l₂ simp [List.lt_iff_exists] -theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Array α} : @@ -258,14 +258,14 @@ theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)] cases l₂ simpa using List.le_append_left -theorem map_lt [LT α] [LT β] +protected 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 β] +protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean index 3737d082f3..c4f9b63fda 100644 --- a/src/Init/Data/List/Lex.lean +++ b/src/Init/Data/List/Lex.lean @@ -14,8 +14,8 @@ namespace List @[simp] theorem lex_lt [LT α] (l₁ l₂ : List α) : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂ := Iff.rfl @[simp] theorem not_lex_lt [LT α] (l₁ l₂ : List α) : ¬ Lex (· < ·) l₁ l₂ ↔ 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 α) : +protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : List α) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl +protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) : ¬ l₁ ≤ l₂ ↔ l₂ < l₁ := Decidable.not_not @@ -260,7 +260,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α] · exfalso exact h' h -theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] [Std.Total (¬ · < · : α → α → Prop)] @@ -435,7 +435,7 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α simpa using w₁ (j + 1) (by simpa) · simpa using w₂ -theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : +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), @@ -444,7 +444,7 @@ theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Lis rw [← lex_eq_true_iff_lt, lex_eq_true_iff_exists] simp -theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} : @@ -489,7 +489,7 @@ theorem IsPrefix.le [LT α] [Std.Irrefl (· < · : α → α → Prop)] rcases h with ⟨_, rfl⟩ apply le_append_left -theorem map_lt [LT α] [LT β] +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 @@ -497,11 +497,11 @@ theorem map_lt [LT α] [LT β] | 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)] + 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] -theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] +protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] @@ -510,7 +510,7 @@ theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β [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 ⊢ + rw [List.le_iff_exists] at h ⊢ obtain (h | ⟨i, h₁, h₂, w₁, w₂⟩) := h · left rw [h] diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 3a364334be..d01075f54a 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -19,6 +19,11 @@ namespace Vector @[simp] theorem lt_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList ↔ l₁ < l₂ := Iff.rfl @[simp] theorem le_toList [LT α] (l₁ l₂ : Vector α n) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂ := Iff.rfl +protected theorem not_lt_iff_ge [LT α] (l₁ l₂ : Vector α n) : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl +protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : Vector α n) : + ¬ l₁ ≤ l₂ ↔ l₂ < l₁ := + Decidable.not_not + @[simp] theorem mk_lt_mk [LT α] : Vector.mk (α := α) (n := n) data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂ := Iff.rfl @@ -133,7 +138,7 @@ protected theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ ≤ l₂ := Array.le_of_lt h -theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] [Std.Total (¬ · < · : α → α → Prop)] @@ -200,14 +205,14 @@ theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α rcases l₂ with ⟨l₂, n₂⟩ simp_all [Array.lex_eq_false_iff_exists, n₂] -theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} : +protected theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} : l₁ < l₂ ↔ (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) := by cases l₁ cases l₂ simp_all [Array.lt_iff_exists] -theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] +protected theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} : @@ -230,12 +235,12 @@ theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α] l₁ ++ l₂ ≤ l₁ ++ l₃ := by simpa using Array.append_left_le h -theorem map_lt [LT α] [LT β] +protected 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 β] +protected theorem map_le [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl (· < · : α → α → Prop)] [Std.Asymm (· < · : α → α → Prop)] [Std.Antisymm (¬ · < · : α → α → Prop)]