feat: grind support for .ctorIdx (#11652)

This PR teaches `grind` how to reduce `.ctorIdx` applied to
constructors. It can also handle tasks like
```
xs ≍ Vec.cons x xs' → xs.ctorIdx = 1
```
thanks to a `.ctorIdx.hinj` theorem (generated on demand).

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -145,6 +145,6 @@ Asserts that the `(n+1)`th least significant bit of `m` is not set.
 (This definition is used by Lean internally for compact bitmaps.)
 -/
 @[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
-  Nat.land 1 (Nat.shiftRight m n) ≠ 1
+  1 &&& (m >>> n) ≠ 1
 
 end Nat

src/Lean/Meta.lean

@@ -58,3 +58,4 @@ public import Lean.Meta.BinderNameHint
 public import Lean.Meta.TryThis
 public import Lean.Meta.Hint
 public import Lean.Meta.MethodSpecs
+public import Lean.Meta.CtorIdxHInj

src/Lean/Meta/Basic.lean

@@ -1845,6 +1845,19 @@ def withInstImplicitAsImplicit (xs : Array Expr) (k : MetaM α) : MetaM α := do
       return none
   withNewBinderInfos newBinderInfos k
 
+private def withPrimedNamesImp (xs : Array Expr) (k : MetaM α) : MetaM α := do
+  let lctx ← getLCtx
+  let lctx := lctx.modifyLocalDecls fun decl =>
+    if xs.contains (mkFVar decl.fvarId) then
+      decl.setUserName (decl.userName.appendAfter "'")
+    else
+      decl
+  withReader (fun ctx => { ctx with lctx := lctx }) k
+
+/-- Appends a `'` to the namen of the given free variables. -/
+def withPrimedNames (xs : Array Expr) (k : n α) : n α := do
+  mapMetaM (fun k => withPrimedNamesImp xs k) k
+
 private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) (nondep : Bool) (kind : LocalDeclKind) : MetaM α := do
   let fvarId ← mkFreshFVarId
   let ctx ← read

src/Lean/Meta/Constructions/CtorIdx.lean

@@ -26,6 +26,14 @@ public def mkToCtorIdxName (indName : Name) : Name :=
 public def mkCtorIdxName (indName : Name) : Name :=
   Name.mkStr indName "ctorIdx"
 
+public def isCtorIdxCore? (env : Environment) (declName : Name) : Option InductiveVal := do
+  let .str indName "ctorIdx" := declName | none
+  let indInfo ← isInductiveCore? env indName
+  return indInfo
+
+public def isCtorIdx? (declName : Name) : MetaM (Option InductiveVal) := do
+  return isCtorIdxCore? (← getEnv) declName
+
 /--
 For an inductive type `T` with more than one function builds a function `T.ctorIdx : T → Nat` that
 returns the constructor index of the given value.
@@ -85,6 +93,7 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
       if info.numCtors = 1 then
         setInlineAttribute declName .macroInline
       compileDecl decl
+      enableRealizationsForConst declName
 
       -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
       if (← isEnumType indName) then

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -18,15 +18,6 @@ namespace Lean
 
 open Meta
 
-def withPrimedNames (xs : Array Expr) (k : MetaM α) : MetaM α := do
-  let lctx ← getLCtx
-  let lctx := lctx.modifyLocalDecls fun decl =>
-    if xs.contains (mkFVar decl.fvarId) then
-      decl.setUserName (decl.userName.appendAfter "'")
-    else
-      decl
-  withLCtx lctx (← getLocalInstances) k
-
 /--
 Constructs a lambda expression that returns the argument to the `noConfusion` principle for a given
 constructor. In particular, returns

src/Lean/Meta/CtorIdxHInj.lean

@@ -0,0 +1,76 @@
+/-
+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
+public import Lean.Meta.Basic
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Assumption
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.SameCtorUtils
+import Lean.Meta.Constructions.CtorIdx
+namespace Lean.Meta
+
+def hinjSuffix := "hinj"
+
+public def mkCtorIdxHInjTheoremNameFor (indName : Name) : Name :=
+  (mkCtorIdxName indName).str hinjSuffix
+
+private partial def mkHInjectiveTheorem? (thmName : Name) (indVal : InductiveVal) : MetaM TheoremVal := do
+  let us := indVal.levelParams.map mkLevelParam
+  let thmType ←
+    forallBoundedTelescope indVal.type (indVal.numParams + indVal.numIndices) fun xs1 _ => do
+    forallBoundedTelescope indVal.type (indVal.numParams + indVal.numIndices) fun xs2 _ => do
+    withImplicitBinderInfos xs1 do
+    withImplicitBinderInfos xs2 do
+    withPrimedNames xs2 do
+    withLocalDeclD `x  (mkAppN (mkConst indVal.name us) xs1) fun x1 => do
+    withLocalDeclD `x' (mkAppN (mkConst indVal.name us) xs2) fun x2 => do
+      let ctorIdxApp1 := mkAppN (mkConst (mkCtorIdxName indVal.name) us) (xs1.push x1)
+      let ctorIdxApp2 := mkAppN (mkConst (mkCtorIdxName indVal.name) us) (xs2.push x2)
+      let mut thmType ← mkEq ctorIdxApp1 ctorIdxApp2
+      for a1 in (xs1.push x1).reverse, a2 in (xs2.push x2).reverse do
+        if (← isProof a1) then
+          continue
+        let name := (← a1.fvarId!.getUserName).appendAfter "_eq"
+        let eq ← mkEqHEq a1 a2
+        thmType := mkForall name .default eq thmType
+      mkForallFVars (xs1.push x1 ++ xs2.push x2) thmType
+
+  let thmVal ← mkFreshExprSyntheticOpaqueMVar thmType
+  let mut mvarId := thmVal.mvarId!
+  mvarId := (← mvarId.introN (2 * (indVal.numParams + indVal.numIndices + 1))).2
+  repeatIntroSubstRefl mvarId
+  let thmVal ← instantiateMVars thmVal
+  return { name := thmName, levelParams := indVal.levelParams, type := thmType, value := thmVal }
+where
+  repeatIntroSubstRefl (mvarId : MVarId) : MetaM Unit := do
+    let type ← mvarId.getType
+    if type.isForall then
+      let (h, mvarId) ← mvarId.intro1
+      let (h, mvarId) ← heqToEq mvarId h
+      let (_, mvarId) ← substEq mvarId h
+      repeatIntroSubstRefl mvarId
+    else
+      mvarId.refl
+
+
+builtin_initialize registerReservedNamePredicate fun env n =>
+  match n with
+  | .str p "hinj" => (isCtorIdxCore? env p).isSome
+  | _ => false
+
+builtin_initialize
+  registerReservedNameAction fun name => do
+    let .str p "hinj" := name | return false
+    let some indVal := isCtorIdxCore? (← getEnv) p | return false
+    MetaM.run' do
+    realizeConst p name do
+      let thmVal ← mkHInjectiveTheorem? name indVal
+      addDecl (← mkThmOrUnsafeDef thmVal)
+    return true
+
+end Lean.Meta

src/Lean/Meta/Tactic/Grind/CtorIdx.lean

@@ -0,0 +1,51 @@
+/-
+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
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Constructions.CtorIdx
+import Lean.Meta.CtorIdxHInj
+public section
+namespace Lean.Meta.Grind
+
+/--
+Propagation for `T.ctorIdx`. Cf. the `reduceCtorIdx` simproc.
+-/
+def propagateCtorIdxUp (e : Expr) : GoalM Unit := e.withApp fun f xs => do
+  let some fnName := f.constName? | return
+  let some indInfo ← isCtorIdx? fnName | return
+  unless xs.size == indInfo.numParams + indInfo.numIndices + 1 do return
+  let a := xs.back!
+  let aNode ← getRootENode a
+  unless aNode.ctor do return
+  let some conInfo ← isConstructorApp? aNode.self | return
+  if aNode.heqProofs then
+    unless (← hasSameType a aNode.self) do
+      let b := aNode.self
+      let gen := max (← getGeneration a) (← getGeneration b)
+      -- Handle heterogeneous equality case
+      -- We add a suitable invocation of the `.ctorIdx.hinj` theorem
+      let aType ← whnfD (← inferType a)
+      let bType ← whnfD (← inferType b)
+      assert! aType.isAppOfArity indInfo.name (indInfo.numParams + indInfo.numIndices)
+      -- both types should be headed by the same type former
+      unless bType.isAppOfArity indInfo.name (indInfo.numParams + indInfo.numIndices) do return
+      let us := aType.getAppFn.constLevels!
+      let hinjName := mkCtorIdxHInjTheoremNameFor indInfo.name
+      unless (← getEnv).containsOnBranch hinjName do
+        let _ ← executeReservedNameAction hinjName
+      let proof := mkConst hinjName us
+      let proof := mkApp (mkAppN proof aType.getAppArgs) a
+      let proof := mkApp (mkAppN proof bType.getAppArgs) b
+      addNewRawFact proof (← inferType proof) gen (.inj (.decl hinjName))
+      return
+  -- Homogeneous case
+  let e' ← shareCommon (mkNatLit conInfo.cidx)
+  internalize e' 0
+  pushEq e e' (← mkCongrArg e.appFn! (← mkEqProof a aNode.self))
+
+end Lean.Meta.Grind

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

@@ -17,6 +17,7 @@ import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
 import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.CtorIdx
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
@@ -62,6 +63,7 @@ def mkMethods (evalTactic? : Option EvalTactic := none) : CoreM Methods := do
       propagateReflCmp e
       let .const declName _ := e.getAppFn | return ()
       propagateProjEq e
+      propagateCtorIdxUp e
       if let some props := builtinPropagators.up[declName]? then
        props.forM fun prop => prop e
     propagateDown := fun e => do

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

@@ -7,8 +7,9 @@ Authors: Joachim Breitner
 module
 
 prelude
-import Init.Simproc
 public import Lean.Meta.Tactic.Simp.Simproc
+import Init.Simproc
+import Lean.Meta.Constructions.CtorIdx
 
 open Lean Meta Simp
 
@@ -20,8 +21,7 @@ It does not take part in simp's discrimination tree index, so can be costly on l
 -/
 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
+  let some indInfo ← isCtorIdx? fnName | 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

src/Lean/MonadEnv.lean

@@ -96,13 +96,16 @@ def getAsyncConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) (
   | some val => pure val
   | none     => throwUnknownConstant constName
 
-def isInductive? [Monad m] [MonadEnv m] (declName : Name) : m (Option InductiveVal) := do
-  match (← getEnv).findAsync? declName with
+def isInductiveCore? (env : Environment) (declName : Name) : Option InductiveVal := do
+  match env.findAsync? declName with
   | some info@{ kind := .induct, .. } =>
     match info.toConstantInfo with
-    | .inductInfo val => pure (some val)
+    | .inductInfo val => some val
     | _ => unreachable!
-  | _ => pure none
+  | _ => none
+
+def isInductive? [Monad m] [MonadEnv m] (declName : Name) : m (Option InductiveVal) :=
+  return isInductiveCore? (← getEnv) declName
 
 def isDefn? [Monad m] [MonadEnv m] (constName : Name) : m (Option DefinitionVal) := do
   match (← getEnv).findAsync? constName with

tests/lean/run/ctorIdxHInj.lean

@@ -0,0 +1,34 @@
+inductive N : Type where | z : N | s : N → N
+
+/-- info: N.ctorIdx : N → Nat -/
+#guard_msgs in
+#check N.ctorIdx
+
+/-- info: N.ctorIdx.hinj (x x' : N) (x_eq : x = x') : x.ctorIdx = x'.ctorIdx -/
+#guard_msgs in
+#check N.ctorIdx.hinj
+
+inductive Vec (α : Type) : Nat → Type where
+| nil  : Vec α 0
+| cons : {n : Nat} → α → Vec α n → Vec α (Nat.succ n)
+
+/--
+info: Vec.ctorIdx.hinj {α : Type} {a✝ : Nat} (x : Vec α a✝) {α' : Type} {a'✝ : Nat} (x' : Vec α' a'✝) (α_eq : α = α') :
+  a✝ = a'✝ → ∀ (x_eq : x ≍ x'), x.ctorIdx = x'.ctorIdx
+-/
+#guard_msgs in
+#check Vec.ctorIdx.hinj
+
+
+inductive EvenVec (α : Type) : (n : Nat) → (n % 2 = 0) → Type where
+| nil  : EvenVec α 0 (by rfl)
+| cons : α → EvenVec α n p → EvenVec α (n + 2) (by grind)
+
+-- NB: No HEq between the proof arguments (they are not needed)
+
+/--
+info: EvenVec.ctorIdx.hinj {α : Type} {n : Nat} {a✝ : n % 2 = 0} (x : EvenVec α n a✝) {α' : Type} {n' : Nat}
+  {a'✝ : n' % 2 = 0} (x' : EvenVec α' n' a'✝) (α_eq : α = α') (n_eq : n = n') (x_eq : x ≍ x') : x.ctorIdx = x'.ctorIdx
+-/
+#guard_msgs in
+#check EvenVec.ctorIdx.hinj

tests/lean/run/grind_ctorIdx.lean

@@ -0,0 +1,127 @@
+set_option warn.sorry false
+
+inductive T where
+| con1 : Nat → T
+| con2 : T
+
+opaque double (n : Nat) : T := .con2
+
+
+example (heq_1 : double n = .con1 5) : (double n).ctorIdx = 0 := by
+  grind
+
+example  (h : (double n).ctorIdx > 5) (heq_1 : double n = .con1 5) : False := by
+  grind
+
+example  (h : Nat.hasNotBit 1 0) : False := by
+  grind
+
+example  (h : Nat.hasNotBit 1 (double n).ctorIdx) (heq_1 : double n = .con1 5) : False := by
+  grind
+
+inductive IT : Nat → Type where
+| con1 n : IT n
+| con2 : IT 0
+
+-- This should not work: we cannot conclude anything about `x.ctorIdx` without knowing `m`.
+example (heq_1 : (x : IT m) ≍ (IT.con1 4)) : x.ctorIdx = 0 := by
+  fail_if_success grind
+  sorry
+
+-- But this works, thanks to the `.ctorIdx.hinj` theorem
+example (hm : m = 4) (heq_1 : (x : IT m) ≍ (IT.con1 4)) : x.ctorIdx = 0 := by
+  grind
+
+-- More dependent examples
+
+opaque Nat.double (n : Nat) : Nat := n + n
+
+inductive Vec (α : Type) : Nat → Type where
+| nil  : Vec α 0
+| cons : {n : Nat} → α → Vec α n → Vec α (Nat.succ n)
+
+example
+    (n k : Nat)
+    (hα : α = α')
+    (_ : Nat.double n = k + 1)
+    (xs : Vec α (.double n)) (x : α') (xs' : Vec α' k)
+    (heq : xs ≍ Vec.cons x xs') :
+    xs.ctorIdx = 1 := by
+  grind
+
+
+inductive EvenVec (α : Type) : (n : Nat) → (n % 2 = 0) → Type where
+| nil  : EvenVec α 0 (by rfl)
+| cons n p : α → EvenVec α n p → EvenVec α (n + 2) (by grind)
+
+example (hα : α = α') (_ : double n = double m)
+    (_ : Nat.double n = k + 2)
+    (xs : EvenVec α (.double n) p1) (x' : α') (xs' : EvenVec α' k p2)
+    (heq : xs ≍ EvenVec.cons _ p3 x' xs') :
+    xs.ctorIdx = 1 := by
+  grind
+
+-- Heteogeneous equality where the sides are not headed by the same type constructor
+
+example (h : Bool = Nat) (x : Bool) (heq : x ≍ Nat.succ n) : x.ctorIdx = 0 := by
+  fail_if_success grind
+  sorry
+
+-- Some tests provided by claude
+
+-- Test 1: Multiple ctorIdx comparisons with different constructors
+example (t1 t2 : T) (h1 : t1 = .con1 10) (h2 : t2 = .con2) : t1.ctorIdx ≠ t2.ctorIdx := by
+  grind
+
+-- Test 2: ctorIdx with transitivity through multiple equalities
+example (t1 t2 t3 : T) (h1 : t1 = t2) (h2 : t2 = t3) (h3 : t3 = .con1 7) : t1.ctorIdx = 0 := by
+  grind
+
+-- Test 3: ctorIdx inequality leading to false
+example (t : T) (h1 : t = .con1 3) (h2 : t.ctorIdx = 1) : False := by
+  grind
+
+-- Test 4: ctorIdx with Option type (simple inductive with two constructors)
+example (opt : Option Nat) (h : opt = .some 42) : opt.ctorIdx = 1 := by
+  grind
+
+example (opt : Option Nat) (h : opt = .none) : opt.ctorIdx = 0 := by
+  grind
+
+-- Test 5: ctorIdx distinguishing between constructors indirectly
+example (opt1 opt2 : Option Nat) (h1 : opt1 = .some 5) (h2 : opt2 = .none)
+    (heq : opt1.ctorIdx = opt2.ctorIdx) : False := by
+  grind
+
+-- Test 6: Dependent type with multiple index changes
+example (n m : Nat) (v1 : Vec Nat n) (v2 : Vec Nat m)
+    (hn : n = 0) (hm : m = 1)
+    (hv1 : v1 ≍ (Vec.nil : Vec Nat 0)) (hv2 : v2 ≍ (Vec.cons 0 Vec.nil : Vec Nat 1))
+    (hidx : v1.ctorIdx = v2.ctorIdx) : False := by
+  grind
+
+-- Test 7: ctorIdx with nested dependent types
+inductive Fin' : Nat → Type where
+| zero : {n : Nat} → Fin' (n + 1)
+| succ : {n : Nat} → Fin' n → Fin' (n + 1)
+
+example (n : Nat) (hn : n = 5) (f : Fin' n) (hf : f ≍ (Fin'.zero : Fin' 5)) : f.ctorIdx = 0 := by
+  grind
+
+-- Test 8: ctorIdx propagation through arithmetic
+example (t : T) (h : t = .con2) (hbad : t.ctorIdx + 1 = 1) : False := by
+  grind
+
+-- Test 9: Complex heterogeneous equality with List
+example (xs ys : List Nat)
+    (hxs : xs = List.nil)
+    (hys : ys = List.cons 0 List.nil)
+    (hidx : xs.ctorIdx = ys.ctorIdx) : False := by
+  grind
+
+-- Test 10: ctorIdx with Sum type
+example (s : Sum Nat Bool) (h : s = .inl 5) : s.ctorIdx = 0 := by
+  grind
+
+example (s : Sum Nat Bool) (h : s = .inr true) : s.ctorIdx = 1 := by
+  grind