max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: protect some lemmas in List/Array/Vector namespace (#6425)

Browse source
This commit is contained in:
Kim Morrison 2024-12-20 22:23:56 +11:00 • committed by GitHub
parent 9a53c88ecf
commit 39eaa214d4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 26 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Data/Array/Lex/Lemmas.lean
View file

@ -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)]

18
src/Init/Data/List/Lex.lean
View file

@ -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]

15
src/Init/Data/Vector/Lex.lean
View file

@ -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)]