From d76752ffb89be62064b29b71b1368fdc300957bb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 13 Dec 2025 14:32:19 +0100 Subject: [PATCH] feat: grind support for `.ctorIdx` (#11652) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 2 +- src/Lean/Meta.lean | 1 + src/Lean/Meta/Basic.lean | 13 ++ src/Lean/Meta/Constructions/CtorIdx.lean | 9 ++ src/Lean/Meta/Constructions/NoConfusion.lean | 9 -- src/Lean/Meta/CtorIdxHInj.lean | 76 +++++++++++ src/Lean/Meta/Tactic/Grind/CtorIdx.lean | 51 +++++++ src/Lean/Meta/Tactic/Grind/Main.lean | 2 + .../Tactic/Simp/BuiltinSimprocs/CtorIdx.lean | 6 +- src/Lean/MonadEnv.lean | 11 +- tests/lean/run/ctorIdxHInj.lean | 34 +++++ tests/lean/run/grind_ctorIdx.lean | 127 ++++++++++++++++++ 12 files changed, 324 insertions(+), 17 deletions(-) create mode 100644 src/Lean/Meta/CtorIdxHInj.lean create mode 100644 src/Lean/Meta/Tactic/Grind/CtorIdx.lean create mode 100644 tests/lean/run/ctorIdxHInj.lean create mode 100644 tests/lean/run/grind_ctorIdx.lean diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 7b1b088ea6..850b7f8954 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/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 diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 063b930ea8..c564e98331 100644 --- a/src/Lean/Meta.lean +++ b/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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 7bb081b0d1..3d088bc7b6 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean index fef1e27cdd..66fc700afe 100644 --- a/src/Lean/Meta/Constructions/CtorIdx.lean +++ b/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 diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean index 98cdf01afc..038a97e8a6 100644 --- a/src/Lean/Meta/Constructions/NoConfusion.lean +++ b/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 diff --git a/src/Lean/Meta/CtorIdxHInj.lean b/src/Lean/Meta/CtorIdxHInj.lean new file mode 100644 index 0000000000..69c24a65bb --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/CtorIdx.lean b/src/Lean/Meta/Tactic/Grind/CtorIdx.lean new file mode 100644 index 0000000000..02af4da97d --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 862d9835d5..01ee043db8 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean index 7e9f977de6..d615889d1c 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/CtorIdx.lean +++ b/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 diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 7075b78fc7..c24b3d6038 100644 --- a/src/Lean/MonadEnv.lean +++ b/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 diff --git a/tests/lean/run/ctorIdxHInj.lean b/tests/lean/run/ctorIdxHInj.lean new file mode 100644 index 0000000000..cc65c46031 --- /dev/null +++ b/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 diff --git a/tests/lean/run/grind_ctorIdx.lean b/tests/lean/run/grind_ctorIdx.lean new file mode 100644 index 0000000000..8e096f778a --- /dev/null +++ b/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