From ca253ae4cfc73d57436a32fd82ca8c4f2fff753f Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Tue, 18 Feb 2025 13:19:08 +1100
Subject: [PATCH] chore: repair defeqs for List GetElem instances (#7121)

This PR repairs some defeq breakages from #7059.
---
 src/Init/Data/Array/Basic.lean   |  6 ++--
 src/Init/Data/List/Attach.lean   |  8 +----
 src/Init/Data/List/BasicAux.lean | 26 +++++++-------
 src/Init/Data/List/Lemmas.lean   | 19 ++--------
 src/Init/GetElem.lean            | 61 ++++++++++++++++++++++++++++++++
 5 files changed, 81 insertions(+), 39 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index a53f30a75f..b1fcb2a4ec 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -87,7 +87,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
-@[simp] theorem getElem?_toList {a : Array α} {i : Nat} : a.toList[i]? = a[i]? := rfl
+@[simp] theorem getElem?_toList {a : Array α} {i : Nat} : a.toList[i]? = a[i]? := by
+  simp [getElem?_def]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma
@@ -129,7 +130,8 @@ abbrev _root_.Array.size_toArray := @List.size_toArray
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 
-@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := by
+  simp [getElem?_def]
 
 @[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
     a.toArray[i]! = a[i]! := by
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index f47ac888ba..ffb7689dae 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -233,13 +233,7 @@ theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     rcases i with ⟨i⟩
     · simp only [Option.pmap]
       split <;> simp_all
-    · simp only [hl, pmap, Option.pmap, getElem?_cons_succ]
-      split <;> rename_i h₁ _ <;> split <;> rename_i h₂ _
-      · simp_all
-      · simp at h₂
-        simp_all
-      · simp_all
-      · simp_all
+    · simp only [pmap, getElem?_cons_succ, hl, Option.pmap]
 
 set_option linter.deprecated false in
 @[deprecated List.getElem?_pmap (since := "2025-02-12")]
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 814009faee..82a65493c7 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -51,19 +51,6 @@ theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n)
     have h0 : some a = some a' := h 0
     injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
 
-/-! ### getD -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `fallback`.
-See also `get?` and `get!`.
--/
-def getD (as : List α) (i : Nat) (fallback : α) : α :=
-  as[i]?.getD fallback
-
-@[simp] theorem getD_nil : getD [] n d = d := rfl
-
 /-! ### get! -/
 
 /--
@@ -89,6 +76,19 @@ set_option linter.deprecated false in
 @[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
 theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
 
+/-! ### getD -/
+
+/--
+Returns the `i`-th element in the list (zero-based).
+
+If the index is out of bounds (`i ≥ as.length`), this function returns `fallback`.
+See also `get?` and `get!`.
+-/
+def getD (as : List α) (i : Nat) (fallback : α) : α :=
+  as[i]?.getD fallback
+
+@[simp] theorem getD_nil : getD [] n d = d := rfl
+
 /-! ### getLast! -/
 
 /--
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 7f428f5833..79812938b3 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -224,28 +224,13 @@ theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
       if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
   cases i <;> simp
 
-theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by
-  simp [getElem?]
+theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := rfl
 
-@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := by
-  simp [getElem?, decidableGetElem?, Nat.succ_lt_succ_iff]
+@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := rfl
 
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp [getElem?_cons_zero]
 
-@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i :=
-  match l with
-  | [] => by simp
-  | _ :: l => by simp
-
-@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
-  simp [eq_comm (a := none)]
-
-theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
-
-@[simp] theorem getElem?_eq_getElem {l : List α} {i} (h : i < l.length) : l[i]? = some l[i] :=
-  getElem?_pos ..
-
 theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a :=
   match l with
   | [] => by simp
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 6a1012bd7d..ee287c91f4 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -247,6 +247,67 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
 @[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")]
 abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop
 
+/-! ### getElem?-/
+
+/-- Internal implementation of `as[i]?`. Do not use directly. -/
+def get?Internal : (as : List α) → (i : Nat) → Option α
+  | a::_,  0   => some a
+  | _::as, n+1 => get?Internal as n
+  | _,     _   => none
+
+/-- Internal implementation of `as[i]!`. Do not use directly. -/
+def get!Internal [Inhabited α] : (as : List α) → (i : Nat) → α
+  | a::_,  0   => a
+  | _::as, n+1 => get!Internal as n
+  | _,     _   => panic! "invalid index"
+
+/-- This instance overrides the default implementation of `a[i]?` via `decidableGetElem?`,
+giving better definitional equalities. -/
+instance : GetElem? (List α) Nat α fun as i => i < as.length where
+  getElem? as i := as.get?Internal i
+  getElem! as i := as.get!Internal i
+
+@[simp] theorem get?Internal_eq_getElem? {l : List α} {i : Nat} :
+    l.get?Internal i = l[i]? := rfl
+
+@[simp] theorem get!Internal_eq_getElem! [Inhabited α] {l : List α} {i : Nat} :
+    l.get!Internal i = l[i]! := rfl
+
+@[simp] theorem getElem?_eq_getElem {l : List α} {i} (h : i < l.length) :
+    l[i]? = some l[i] := by
+  induction l generalizing i with
+  | nil => cases h
+  | cons a l ih =>
+    cases i with
+    | zero => rfl
+    | succ i => exact ih ..
+
+@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i :=
+  match l with
+  | [] => by simp; rfl
+  | _ :: l => by
+    cases i with
+    | zero => simp
+    | succ i =>
+      simp only [length_cons, Nat.add_le_add_iff_right]
+      exact getElem?_eq_none_iff (l := l) (i := i)
+
+@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by
+  simp [eq_comm (a := none)]
+
+theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
+
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+  getElem?_def as i h := by
+    split <;> simp_all
+  getElem!_def as i := by
+    induction as generalizing i with
+    | nil => rfl
+    | cons a as ih =>
+      cases i with
+      | zero => rfl
+      | succ i => simpa using ih i
+
 end List
 
 namespace Array