wip

src/Init.lean

@@ -44,3 +44,5 @@ public import Init.Internal
 public import Init.Try
 public import Init.BinderNameHint
 public import Init.Task
+public import Init.GetElem
+public import Init.GetElemV

src/Init/Classical.lean

@@ -16,6 +16,10 @@ universe u v
 
 namespace Classical
 
+/-- Using `Classical.choice`, extracts a term from a `Nonempty` type. -/
+protected noncomputable abbrev arbitrary (α) [h : Nonempty α] : α :=
+  Classical.choice h
+
 noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
   choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
 

src/Init/Data/List/Lemmas.lean

@@ -13,6 +13,7 @@ public import all Init.Data.List.BasicAux
 public import all Init.Data.List.Control
 public import Init.Control.Lawful.Basic
 public import Init.BinderPredicates
+public import Init.GetElemV
 
 public section
 
@@ -3729,6 +3730,20 @@ set_option linter.deprecated false in
 theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
   simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
 
+/-! ### `getElemV` -/
+
+noncomputable instance : GetElemV (List α) Nat α where
+  getElemV xs i := if h : i < xs.length then xs[i] else Classical.arbitrary α
+
+instance : LawfulGetElemV (List α) Nat α (fun xs i => i < xs.length) where
+  getElemV_def xs i := by
+    simp [getElemV]
+    split <;> simp_all
+
+theorem getElemV_map [Nonempty α] [Nonempty β] {xs : List α} {f : α → β} (h : i < xs.length) :
+    (xs.map f)[i]ᵛ = f xs[i]ᵛ := by
+  simp_all [LawfulGetElemV.getElemV_def]
+
 /-! ### Deprecations -/
 
 @[deprecated _root_.isSome_getElem? (since := "2024-12-09")]

src/Init/GetElemV.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.GetElem
+public import Init.Classical
+
+public section
+
+@[inherit_doc GetElem]
+class GetElemV (coll : Type u) (idx : Type v) (elem : outParam (Type w)) where
+  /--
+  The syntax `arr[i]ᵛ` gets the `i`'th element of the collection `arr`,
+  if it is present, and otherwise returns a (noncomputable) default value.
+  -/
+  getElemV [Nonempty elem] : coll → idx → elem
+
+export GetElemV (getElemV)
+
+/--
+The syntax `arr[i]ᵛ` gets the `i`'th element of the collection `arr` or
+a (noncomputable) default value if `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]ᵛ" : term => `(getElemV $x $i)
+
+recommended_spelling "getElemV" for "xs[i]ᵛ" in [GetElemV.getElemV, «term__[_]ᵛ»]
+
+open Classical
+
+noncomputable instance (priority := low) [GetElem coll idx elem valid] : GetElemV coll idx elem where
+  getElemV xs i := if h : valid xs i then xs[i]'h else choice ‹Nonempty elem›
+
+class LawfulGetElemV (cont : Type u) (idx : Type v) (elem : outParam (Type w))
+   (dom : outParam (cont → idx → Prop)) [GetElem cont idx elem dom] [GetElemV cont idx elem] : Prop where
+  /-- The "verification only" getter notation `xs[i]ᵛ` coincides with the usual `xs[i]`. -/
+  getElemV_def [Nonempty elem] (c : cont) (i : idx) :
+      c[i]ᵛ = if h : dom c i then c[i]'h else choice ‹Nonempty elem›
+
+theorem getElem_eq_getElemV
+    [GetElem coll idx elem valid] [GetElemV coll idx elem]
+    [LawfulGetElemV coll idx elem valid] {xs : coll} {i : idx} (h : valid xs i) :
+    xs[i] = @GetElemV.getElemV _ _ _ _ ⟨xs[i]⟩ xs i := by
+  have : Nonempty elem := ⟨xs[i]⟩
+  rw [LawfulGetElemV.getElemV_def, dif_pos h]