feat: add cbv simprocs for arrays (#12875)

This PR adds `cbv` simprocs for getting elements out of arrays.

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.LitValues
+import Lean.Meta.Sym.InferType
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+import Init.GetElem
+
+namespace Lean.Meta.Tactic.Cbv
+
+/-- Extract elements from a `List.cons`/`List.nil` chain. -/
+private partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option <| Array Expr :=
+  match_expr e with
+  | List.nil _ => some acc
+  | List.cons _ a as => getListLitElems as <| acc.push a
+  | _ => none
+
+/-- Extract elements from an array literal (`Array.mk` applied to a list literal). -/
+private def getArrayLitElems? (e : Expr) : Option <| Array Expr :=
+  match_expr e with
+  | Array.mk _ as => getListLitElems as
+  | _ => none
+
+/-- Reduce `#[...][n]` for literal arrays and literal `Nat` indices. -/
+builtin_cbv_simproc cbv_eval simpArrayGetElem (@GetElem.getElem (Array _) Nat _ _ _ _ _ _) := fun e => do
+  let_expr GetElem.getElem _ _ _ _ _ xs n _ := e | return .rfl
+  let some elems := getArrayLitElems? xs | return .rfl
+  let some idx := Sym.getNatValue? n | return .rfl
+  if h : idx < elems.size then
+    let result := elems[idx]
+    return .step result (← Sym.mkEqRefl result)
+  else
+    return .rfl
+
+/-- Reduce `#[...][n]?` for literal arrays and literal `Nat` indices. -/
+builtin_cbv_simproc cbv_eval simpArrayGetElem? (@GetElem?.getElem? (Array _) Nat _ _ _ _ _) := fun e => do
+  let_expr GetElem?.getElem? _ _ α _ _ xs n := e | return .rfl
+  let some elems := getArrayLitElems? xs | return .rfl
+  let some idx := Sym.getNatValue? n | return .rfl
+  let sortLevel ← Sym.getLevel α
+  let .succ u := sortLevel | return .rfl
+  let result ←
+    if h : idx < elems.size then
+      Sym.share <| mkApp2 (mkConst ``Option.some [u]) α elems[idx]
+    else
+      Sym.share <| mkApp (mkConst ``Option.none [u]) α
+  return .step result (← Sym.mkEqRefl result)
+
+end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Tactic.Cbv.Opaque
 public import Lean.Meta.Tactic.Cbv.ControlFlow
 import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Core
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Array
 import Lean.Meta.Tactic.Cbv.Util
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.CbvEvalExt

tests/elab/cbv_array.lean

@@ -0,0 +1,70 @@
+import Std
+set_option cbv.warning false
+
+-- Basic indexing
+theorem test1 : #[1, 2, 3][0] = 1 := by cbv
+
+/--
+info: theorem test1 : #[1, 2, 3][0] = 1 :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl 1)) 1) (eq_self 1))
+-/
+#guard_msgs in 
+#print test1
+
+theorem test2 : #[1, 2, 3][2] = 3 := by cbv
+
+/--
+info: theorem test2 : #[1, 2, 3][2] = 3 :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl 3)) 3) (eq_self 3))
+-/
+#guard_msgs in
+#print test2
+
+-- Optional indexing (in bounds)
+theorem test3 : #[1, 2, 3][1]? = some 2 := by cbv
+
+/--
+info: theorem test3 : #[1, 2, 3][1]? = some 2 :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl (some 2))) (some 2)) (eq_self (some 2)))
+-/
+#guard_msgs in
+#print test3
+
+-- Optional indexing (out of bounds)
+theorem test4 : #[1, 2, 3][5]? = none := by cbv
+
+/--
+info: theorem test4 : #[1, 2, 3][5]? = none :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl none)) none) (eq_self none))
+-/
+#guard_msgs in
+#print test4
+
+-- Nested arrays
+theorem test5 : #[#[1, 2], #[3, 4]][1][0] = 3 := by cbv
+
+/--
+info: theorem test5 : #[#[1, 2], #[3, 4]][1][0] = 3 :=
+of_eq_true
+  (Eq.trans
+    (congrFun'
+      (congrArg Eq
+        (Eq.trans
+          (GetElem.getElem.congr_simp { toList := [{ toList := [1, 2] }, { toList := [3, 4] }] }[1] { toList := [3, 4] }
+            (Eq.refl { toList := [3, 4] }) 0 0 (Eq.refl 0) (of_decide_eq_true (id (Eq.refl true))))
+          (Eq.refl 3)))
+      3)
+    (eq_self 3))
+-/
+#guard_msgs in
+#print test5
+
+-- Array of strings/other types
+theorem test6 : #["a", "b", "c"][0] = "a" := by cbv
+
+/--
+info: theorem test6 : #["a", "b", "c"][0] = "a" :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl "a")) "a") (eq_self "a"))
+-/
+#guard_msgs in
+#print test6