From 257c347f9f2b78ed5aaf47c3247d6db4edc9aada Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 18 Sep 2025 15:05:14 +0200
Subject: [PATCH] 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).
---
 .../Meta/Tactic/Simp/BuiltinSimprocs.lean     |  1 +
 .../Tactic/Simp/BuiltinSimprocs/CtorIdx.lean  | 30 +++++++++++++
 stage0/src/stdlib_flags.h                     |  2 +
 tests/lean/run/reduceCtorIdxSimproc.lean      | 44 +++++++++++++++++++
 4 files changed, 77 insertions(+)
 create mode 100644 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean
 create mode 100644 tests/lean/run/reduceCtorIdxSimproc.lean

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
index 3d9ec72b0c..f333212d11 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean
new file mode 100644
index 0000000000..7e9f977de6
--- /dev/null
+++ b/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
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..f4d5f7ddae 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/reduceCtorIdxSimproc.lean b/tests/lean/run/reduceCtorIdxSimproc.lean
new file mode 100644
index 0000000000..7f4226c02d
--- /dev/null
+++ b/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