From 5cd3a4ab3fa13c9f1be524f90694ff9d517228bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 7 Aug 2024 13:41:09 +0200
Subject: [PATCH 1/2] feat: upstream utilities around `Array`, `Bool` and
 `Prod` from LeanSAT

---
 src/Init/Data/Array/Lemmas.lean | 49 +++++++++++++++++++++++++++++++--
 src/Init/Data/Bool.lean         | 18 ++++++++++++
 src/Init/Data/Prod.lean         |  9 ++++++
 3 files changed, 73 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 0fea06d740f7..ccd264ba2477 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -336,6 +336,11 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
 /-- # get lemmas -/
 
+theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
+    (_h : a[idx]'hidx = x) :
+    idx < a.size := by
+  exact hidx
+
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_data_getElem]
   apply List.get_mem
@@ -505,6 +510,31 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
     simp only [mkEmpty_eq, size_push] at *
     omega
 
+theorem getElem_range {n : Nat} {x : Nat} (h : x < n) : (Array.range n)[x]'(by simp [h]) = x := by
+  induction n
+  . contradiction
+  . next n ih =>
+    rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ h with x_lt_n | x_eq_n
+    . specialize ih x_lt_n
+      simp only [Array.range, Nat.fold, flip, Array.get_push]
+      simp only [Array.range, flip] at ih
+      split
+      . exact ih
+      . next x_ge_n =>
+        exfalso
+        have h_size_range : (Array.range n).size = n := Array.size_range
+        simp only [Array.mkEmpty_eq, Array.range, flip] at h_size_range
+        simp only [Array.mkEmpty_eq, h_size_range] at x_ge_n
+        exact x_ge_n x_lt_n
+    . simp only [Array.range, Nat.fold, flip, Array.get_push]
+      split
+      . next x_lt_n =>
+        exfalso
+        have h_size_range : (Array.range n).size = n := Array.size_range
+        simp only [Array.range, Array.mkEmpty_eq] at h_size_range
+        simp only [x_eq_n, Array.mkEmpty_eq, h_size_range, Nat.lt_irrefl] at x_lt_n
+      . rw [x_eq_n]
+
 set_option linter.deprecated false in
 @[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
   let rec go (as : Array α) (i j hj)
@@ -707,13 +737,26 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
   unfold modify modifyM Id.run
   split <;> simp
 
-theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f).get ⟨i, by simp [h]⟩ =
-    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+theorem getElem_modify {arr : Array α} {x i} (h : i < arr.size) :
+    (arr.modify x f)[i]'(by simp [h]) =
+    if x = i then f (arr[i]'h) else arr[i]'h := by
   simp [modify, modifyM, Id.run]; split
   · simp [get_set _ _ _ h]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
 
+theorem getElem_modify_self {a : Array α} {i : Nat} (i_in_bounds : i < a.size) (f : α → α) :
+    (a.modify i f)[i]'(by simp[i_in_bounds]) = f a[i] := by
+  rw [getElem_modify]
+  simp only [↓reduceIte]
+  assumption
+
+theorem getElem_modify_of_ne {a : Array α} {i : Nat} {j : Nat} (j_size : j < a.size)
+    (f : α → α) (h : i ≠ j) :
+    (a.modify i f)[j]'(by rw [Array.size_modify]; exact j_size) = a[j] := by
+  rw [getElem_modify]
+  simp only [h, ↓reduceIte]
+  assumption
+
 /-! ### filter -/
 
 @[simp] theorem filter_data (p : α → Bool) (l : Array α) :
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index a2e8bb4b9f6c..f3de8ba4ad53 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -438,6 +438,24 @@ Added for confluence between `if_true_left` and `ite_false_same` on
 -/
 @[simp] theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
 
+/-! ### forall -/
+
+theorem forall_bool' {p : Bool → Prop} (b : Bool) : (∀ x, p x) ↔ p b ∧ p !b :=
+  ⟨fun h ↦ ⟨h _, h _⟩, fun ⟨h₁, h₂⟩ x ↦ by cases b <;> cases x <;> assumption⟩
+
+@[simp]
+theorem forall_bool {p : Bool → Prop} : (∀ b, p b) ↔ p false ∧ p true :=
+  forall_bool' false
+
+/-! ### exists -/
+
+theorem exists_bool' {p : Bool → Prop} (b : Bool) : (∃ x, p x) ↔ p b ∨ p !b :=
+  ⟨fun ⟨x, hx⟩ ↦ by cases x <;> cases b <;> first | exact .inl ‹_› | exact .inr ‹_›,
+    fun h ↦ by cases h <;> exact ⟨_, ‹_›⟩⟩
+
+@[simp]
+theorem exists_bool {p : Bool → Prop} : (∃ b, p b) ↔ p false ∨ p true :=
+  exists_bool' false
 
 /-! ### cond -/
 
diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean
index fd1b3814cf80..0882bde8dfdd 100644
--- a/src/Init/Data/Prod.lean
+++ b/src/Init/Data/Prod.lean
@@ -5,9 +5,18 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
+import Init.NotationExtra
 
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
   eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
     cases a; cases b
     refine congr (congrArg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
   rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]
+
+@[simp]
+protected theorem Prod.forall {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
+  ⟨fun h a b ↦ h (a, b), fun h ⟨a, b⟩ ↦ h a b⟩
+
+@[simp]
+protected theorem Prod.exists {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
+  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

From 27c32adec4b36b71d26b6d9bc3eadf91eddd19d7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 7 Aug 2024 22:20:36 +1000
Subject: [PATCH 2/2] suggestions / golfs

---
 src/Init/Data/Array/Lemmas.lean | 64 +++++++++++----------------------
 1 file changed, 21 insertions(+), 43 deletions(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index ccd264ba2477..490fce71d658 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Monadic
+import Init.Data.List.Nat.Range
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem
 import Init.TacticsExtra
@@ -336,10 +337,9 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
 
 /-- # get lemmas -/
 
-theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
-    (_h : a[idx]'hidx = x) :
-    idx < a.size := by
-  exact hidx
+theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
+    idx < a.size :=
+  hidx
 
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_data_getElem]
@@ -510,30 +510,12 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
     simp only [mkEmpty_eq, size_push] at *
     omega
 
-theorem getElem_range {n : Nat} {x : Nat} (h : x < n) : (Array.range n)[x]'(by simp [h]) = x := by
-  induction n
-  . contradiction
-  . next n ih =>
-    rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ h with x_lt_n | x_eq_n
-    . specialize ih x_lt_n
-      simp only [Array.range, Nat.fold, flip, Array.get_push]
-      simp only [Array.range, flip] at ih
-      split
-      . exact ih
-      . next x_ge_n =>
-        exfalso
-        have h_size_range : (Array.range n).size = n := Array.size_range
-        simp only [Array.mkEmpty_eq, Array.range, flip] at h_size_range
-        simp only [Array.mkEmpty_eq, h_size_range] at x_ge_n
-        exact x_ge_n x_lt_n
-    . simp only [Array.range, Nat.fold, flip, Array.get_push]
-      split
-      . next x_lt_n =>
-        exfalso
-        have h_size_range : (Array.range n).size = n := Array.size_range
-        simp only [Array.range, Array.mkEmpty_eq] at h_size_range
-        simp only [x_eq_n, Array.mkEmpty_eq, h_size_range, Nat.lt_irrefl] at x_lt_n
-      . rw [x_eq_n]
+@[simp] theorem data_range (n : Nat) : (range n).data = List.range n := by
+  induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
+
+@[simp]
+theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
+  simp [getElem_eq_data_getElem]
 
 set_option linter.deprecated false in
 @[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
@@ -737,25 +719,21 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
   unfold modify modifyM Id.run
   split <;> simp
 
-theorem getElem_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f)[i]'(by simp [h]) =
-    if x = i then f (arr[i]'h) else arr[i]'h := by
-  simp [modify, modifyM, Id.run]; split
-  · simp [get_set _ _ _ h]; split <;> simp [*]
+theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
+    (as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
+  simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
+  split
+  · simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
 
-theorem getElem_modify_self {a : Array α} {i : Nat} (i_in_bounds : i < a.size) (f : α → α) :
-    (a.modify i f)[i]'(by simp[i_in_bounds]) = f a[i] := by
-  rw [getElem_modify]
-  simp only [↓reduceIte]
-  assumption
+theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
+    (as.modify i f)[i]'(by simp [h]) = f as[i] := by
+  simp [getElem_modify h]
 
-theorem getElem_modify_of_ne {a : Array α} {i : Nat} {j : Nat} (j_size : j < a.size)
+theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
     (f : α → α) (h : i ≠ j) :
-    (a.modify i f)[j]'(by rw [Array.size_modify]; exact j_size) = a[j] := by
-  rw [getElem_modify]
-  simp only [h, ↓reduceIte]
-  assumption
+    (as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
+  simp [getElem_modify hj, h]
 
 /-! ### filter -/