feat: reduceCtorIdx simproc (#10440)

This PR adds the `reduceCtorIdx` simproc which recognizes and reduces
`ctorIdx` applications. This is not on by default yet because it does
not use the discrimination tree (yet).

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -18,5 +18,6 @@ public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs
+public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.CtorIdx
 
 public section

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+
+prelude
+import Init.Simproc
+public import Lean.Meta.Tactic.Simp.Simproc
+
+open Lean Meta Simp
+
+public section
+
+/--
+This simproc reduces `T.ctorIdx (T.con …)` to the constructor index.
+It does not take part in simp's discrimination tree index, so can be costly on large goals.
+-/
+builtin_dsimproc_decl reduceCtorIdx (_) := fun e => e.withApp fun f xs => do
+  let some fnName := f.constName? | return .continue
+  let .str indName "ctorIdx" := fnName | return .continue
+  let some indInfo ← isInductive? indName | return .continue
+  unless xs.size == indInfo.numParams + indInfo.numIndices + 1 do return .continue
+  let some conInfo ← isConstructorApp? xs.back! | return .continue
+  let e' := mkNatLit conInfo.cidx
+  return .done e'
+
+end

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/reduceCtorIdxSimproc.lean

@@ -0,0 +1,44 @@
+set_option warn.sorry false
+
+axiom P : Nat → Prop
+axiom aP n : P n
+
+/-- trace: ⊢ P 0 -/
+#guard_msgs in
+example : P (Nat.ctorIdx Nat.zero) := by
+  fail_if_success simp only []
+  simp only [reduceCtorIdx]
+  trace_state
+  exact aP 0
+
+/-- trace: ⊢ P 0 -/
+#guard_msgs in
+example : P (List.ctorIdx (List.nil : List Int)) := by
+  fail_if_success simp only []
+  simp only [reduceCtorIdx]
+  trace_state
+  exact aP 0
+
+/-- trace: ⊢ P 1 -/
+#guard_msgs in
+example : P (List.ctorIdx [1,2,3]) := by
+  fail_if_success simp only []
+  simp only [reduceCtorIdx]
+  trace_state
+  exact aP 1
+
+/-- trace: ⊢ P 1 -/
+#guard_msgs in
+example : P (Option.ctorIdx (.some true)) := by
+  fail_if_success simp only []
+  simp only [reduceCtorIdx]
+  trace_state
+  exact aP 1
+
+/-- trace: ⊢ P 0 -/
+#guard_msgs in
+example : P (Option.ctorIdx (.none : Option Bool)) := by
+  fail_if_success simp only []
+  simp only [reduceCtorIdx]
+  trace_state
+  exact aP 0