suggestions from review

src/Init/Data/Array/Basic.lean

@@ -60,8 +60,6 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Lemmas.lean

@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?]
+    simp [setD, h, getElem?_def]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
     simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
-    simp only [getElem?, size_push]
+    simp only [getElem?_def, size_push]
     have h1 : ¬ (i < a.size) := by omega
     have h2 : ¬ (i < a.size + 1) := by omega
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
-  simp only [getElem?, Nat.lt_irrefl, dite_false]
+  simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 

src/Init/Data/Array/Subarray.lean

@@ -47,8 +47,6 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
-
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/ByteArray/Basic.lean

@@ -52,13 +52,9 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
-
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩

src/Init/Data/FloatArray/Basic.lean

@@ -58,13 +58,9 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
-
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
-
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/List/Lemmas.lean

@@ -154,7 +154,7 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
   ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?]; split
+  simp only [getElem?, decidableGetElem?]; split
   · exact (get?_eq_get ‹_›)
   · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
 

src/Init/GetElem.lean

@@ -7,22 +7,57 @@ prelude
 import Init.Util
 
 @[never_extract]
-private def outOfBounds [Inhabited α] : α :=
+def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
 
-/--
-The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
-Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of return
-value `elem` and side conditions `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`.
+theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
+
+/--
+The classes `GetElem` and `GetElem?` implement lookup notation,
+specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
+
+Both classes are indexed by types `coll`, `idx`, and `elem` which are
+the collection, the index, and the element types.
+A single collection may support lookups with multiple index
+types. The relation `valid` determines when the index is guaranteed to be
+valid; lookups of valid indices are guaranteed not to fail.
+
+For example, an instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
+array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
+holds, which is true when `i` is less than the size of the array. `Array`
+additionally supports indexing with `USize` instead of `Nat`.
+In either case, because the bounds are checked at compile time,
+no runtime check is required.
+
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of the return
+value `elem` and side condition `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`. The tactic `get_elem_tactic` is
+invoked to prove validity automatically. The `xs[i]'p` notation uses the
+proof `p` to satisfy the validity condition.
+If the proof `p` is long, it is often easier to place the
+proof in the context using `have`, because `get_elem_tactic` tries
+`assumption`.
 
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
 
 The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
+`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
+`get_elem_tactic_trivial` using `macro_rules`.
+
+`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
+an `Option elem`, with `none` signalling that the value isn't present, and
+the latter returns `elem` but panics if the value isn't there, returning
+`default : elem` based on the `Inhabited elem` instance.
+These are provided by the `GetElem?` class, for which there is a default instance
+generated from a `GetElem` class as long as `valid xs i` is always decidable.
+
+Important instances include:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+
 -/
 class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
               (valid : outParam (coll → idx → Prop)) where
@@ -30,33 +65,10 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
   The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
   are proof side conditions to the application, they will be automatically
   inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent, but here are some
-  important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
-    `default : α` if the index is not valid.
-  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
-    is not valid.
-  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
-    index is valid.
   -/
   getElem (xs : coll) (i : idx) (h : valid xs i) : elem
 
-  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
-    if h : _ then some (getElem xs i h) else none
-
-  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem (getElem getElem! getElem?)
+export GetElem (getElem)
 
 @[inherit_doc getElem]
 syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -66,6 +78,30 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
+/-- Helper function for implementation of `GetElem?.getElem?`. -/
+abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
+    Option elem :=
+  if h : valid xs i then some xs[i] else none
+
+@[inherit_doc GetElem]
+class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
+  /--
+  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
+  if it is present (and wraps it in `some`), and otherwise returns `none`.
+  -/
+  getElem? : coll → idx → Option elem
+
+  /--
+  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
+  if it is present, and otherwise panics at runtime and returns the `default` term
+  from `Inhabited elem`.
+  -/
+  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem? (getElem? getElem!)
+
 /--
 The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
 returns `none` if `i` is out of bounds.
@@ -78,32 +114,43 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    GetElem? coll idx elem valid where
+  getElem? xs i := decidableGetElem? xs i
+
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
 
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+      c[i]? = if h : dom c i then some (c[i]'h) else none := by
+    intros
+    try simp only [getElem?] <;> congr
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
+      c[i]! = match c[i]? with | some e => e | none => default := by
+    intros
+    simp only [getElem!, getElem?, outOfBounds_eq_default]
 
 export LawfulGetElem (getElem?_def getElem!_def)
 
-theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    LawfulGetElem coll idx elem valid where
+
+theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
-theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
-theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
   simp only [getElem!_def, getElem?_def, h]
 
-theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp only [getElem!_def, getElem?_def, h]
 
@@ -111,22 +158,23 @@ namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
   getElem xs i h := getElem xs i.1 h
+
+instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
   getElem? xs i := getElem? xs i.val
   getElem! xs i := getElem! xs i.val
 
-instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
       LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-
   getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i _d := h.getElem!_def ..
+  getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
@@ -139,8 +187,6 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
-instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
-
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
@@ -163,8 +209,6 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
-
 end Array
 
 namespace Lean.Syntax
@@ -172,6 +216,4 @@ namespace Lean.Syntax
 instance : GetElem Syntax Nat Syntax fun _ _ => True where
   getElem stx i _ := stx.getArg i
 
-instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
-
 end Lean.Syntax

src/Lean/Data/HashMap.lean

@@ -223,8 +223,6 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
-instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/PersistentArray.lean

@@ -72,8 +72,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
-instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
-
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -161,8 +161,6 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
-instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 

tests/lean/run/1299.lean

@@ -1,6 +1,9 @@
 @[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
+@[simp] theorem getElem?_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) :
+    a[i]? = a[i.1]? := rfl
+
 example (a : Array α) (i : Fin a.size) : a[i] = a[i.1] := by
   simp
 

tests/lean/run/constructor_as_variable.lean

@@ -97,7 +97,7 @@ Suggestions:
   'Array.Mem.mk',
   'Array.mk',
   'BEq.mk',
-   (or 200 others)
+   (or 201 others)
 -/
 #guard_msgs in
 def ctorSuggestion1 (pair : α × β) : β :=