From d436619c6d5eaa08abbad345349de0972b55661b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Oct 2025 21:16:10 -0400 Subject: [PATCH] feat: add anchor support for restricting search space in `grind only` (#11003) This PR adds support for specifying anchors to restrict the search space in `grind` when using `grind only`. Anchors can limit which case splits are performed and which local lemmas are instantiated. --- src/Init/Grind/Interactive.lean | 8 +- src/Lean/Elab/Tactic/Grind/Anchor.lean | 20 ++ src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 35 ++-- src/Lean/Elab/Tactic/Grind/Main.lean | 150 ++------------- src/Lean/Elab/Tactic/Grind/Param.lean | 172 ++++++++++++++++++ src/Lean/Meta/Tactic/Grind/Anchor.lean | 17 +- src/Lean/Meta/Tactic/Grind/ForallProp.lean | 13 ++ src/Lean/Meta/Tactic/Grind/Main.lean | 20 +- src/Lean/Meta/Tactic/Grind/Split.lean | 65 ++++--- src/Lean/Meta/Tactic/Grind/Types.lean | 24 +++ tests/lean/run/grind_finish_trace.lean | 73 ++++++++ 11 files changed, 393 insertions(+), 204 deletions(-) create mode 100644 src/Lean/Elab/Tactic/Grind/Anchor.lean create mode 100644 src/Lean/Elab/Tactic/Grind/Param.lean diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean index 3764fb2f8c..20a3c3404c 100644 --- a/src/Init/Grind/Interactive.lean +++ b/src/Init/Grind/Interactive.lean @@ -9,6 +9,8 @@ public import Init.Grind.Attr public section namespace Lean.Parser.Tactic +syntax anchor := "#" noWs hexnum + syntax grindLemma := ppGroup((Attr.grindMod ppSpace)? ident) /-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions @@ -16,15 +18,12 @@ when selecting patterns. -/ syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident) -/-! -`grind` tactic and related tactics. --/ syntax grindErase := "-" ident /-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions when selecting patterns. -/ -syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin +syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin <|> anchor namespace Grind declare_syntax_cat grind_filter (behavior := both) @@ -73,7 +72,6 @@ syntax (name := linarith) "linarith" : grind /-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/ syntax (name := «sorry») "sorry" : grind -syntax anchor := "#" noWs hexnum syntax thm := anchor <|> grindLemma <|> grindLemmaMin /-- diff --git a/src/Lean/Elab/Tactic/Grind/Anchor.lean b/src/Lean/Elab/Tactic/Grind/Anchor.lean new file mode 100644 index 0000000000..a8dfb9b7c2 --- /dev/null +++ b/src/Lean/Elab/Tactic/Grind/Anchor.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Lean.Meta.Tactic.Grind.Types +namespace Lean.Elab.Tactic.Grind +open Meta Grind + +public def elabAnchorRef (anchor : TSyntax `hexnum) : CoreM AnchorRef := do + let numDigits := anchor.getHexNumSize + let val := anchor.getHexNumVal + if val >= UInt64.size then + throwError "invalid anchor, value is too big" + let anchorPrefix := val.toUInt64 + return { numDigits, anchorPrefix } + +end Lean.Elab.Tactic.Grind diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean index 70ece6591e..2800cd32a7 100644 --- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean @@ -24,6 +24,7 @@ import Lean.Meta.Tactic.ExposeNames import Lean.Elab.Tactic.Basic import Lean.Elab.Tactic.RenameInaccessibles import Lean.Elab.Tactic.Grind.Filter +import Lean.Elab.Tactic.Grind.Anchor import Lean.Elab.Tactic.Grind.ShowState import Lean.Elab.Tactic.Grind.Config import Lean.Elab.SetOption @@ -139,14 +140,6 @@ def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit := getGoal replaceMainGoal [goal] -def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do - let numDigits := anchor.getHexNumSize - let val := anchor.getHexNumVal - if val >= UInt64.size then - throwError "invalid anchor, value is too big" - let val := val.toUInt64 - return (numDigits, val) - @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do let `(grind| instantiate $[ only%$only ]? $[ approx ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax let goal ← getMainGoal @@ -162,14 +155,14 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do | _ => throwErrorAt thmRef "unexpected theorem reference" ematchThms only thms where - collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do + collectThms (anchorRef : AnchorRef) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do let mut found : Std.HashSet Expr := {} for thm in thms do -- **Note**: `anchors` are cached using pointer addresses, if this is a performance issue, we should -- cache the theorem types. let type ← inferType thm.proof let anchor ← liftGrindM <| getAnchor type - if isAnchorPrefix numDigits anchorPrefix anchor then + if anchorRef.matches anchor then -- **Note**: We display the anchor term at most once. unless found.contains type do logTheoremAnchor thm.proof @@ -177,11 +170,11 @@ where modify (·.push thm) elabLocalEMatchTheorem (anchor : TSyntax `hexnum) : GrindTacticM (Array EMatchTheorem) := withRef anchor do - let (numDigits, anchorPrefix) ← elabAnchor anchor + let anchorRef ← elabAnchorRef anchor let goal ← getMainGoal let thms ← StateT.run' (s := #[]) do - collectThms numDigits anchorPrefix goal.ematch.thms - collectThms numDigits anchorPrefix goal.ematch.newThms + collectThms anchorRef goal.ematch.thms + collectThms anchorRef goal.ematch.newThms get if thms.isEmpty then throwError "no local theorems" @@ -246,7 +239,8 @@ where | .cases _ | .intro | .inj | .ext | .symbol _ => throwError "invalid modifier" -def logAnchor (e : Expr) : TermElabM Unit := do +def logAnchor (c : SplitInfo) : TermElabM Unit := do + let e := c.getExpr let stx ← getRef if e.isFVar || e.isConst then /- @@ -270,19 +264,18 @@ def logAnchor (e : Expr) : TermElabM Unit := do @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax - let (numDigits, val) ← elabAnchor anchor + let anchorRef ← elabAnchorRef anchor let goal ← getMainGoal let candidates := goal.split.candidates - let (e, goals, genNew) ← liftSearchM do + let (c, goals, genNew) ← liftSearchM do for c in candidates do - let e := c.getExpr - let anchor ← getAnchor c.getExpr - if isAnchorPrefix numDigits val anchor then + let anchor ← c.getAnchor + if anchorRef.matches anchor then let some result ← split? c | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}" - return (e, result) + return (c, result) throwError "`cases` tactic failed, invalid anchor" - goal.withContext <| withRef anchor <| logAnchor e + goal.withContext <| withRef anchor <| logAnchor c let goals ← goals.filterMapM fun goal => do let goal := { goal with ematch.num := 0 } let (goal, _) ← liftGrindM <| SearchM.run goal do diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean index 606648566a..7393cdcfa9 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/src/Lean/Elab/Tactic/Grind/Main.lean @@ -13,9 +13,9 @@ public import Lean.PremiseSelection.Basic import Lean.Meta.Tactic.Grind.SimpUtil import Lean.Meta.Tactic.Grind.EMatchTheoremParam import Lean.Elab.Tactic.Grind.Basic +import Lean.Elab.Tactic.Grind.Param import Lean.Elab.MutualDef meta import Lean.Meta.Tactic.Grind.Parser - public section namespace Lean.Elab.Tactic open Meta @@ -71,18 +71,6 @@ def elabInitGrindNorm : CommandElab := fun stx => Grind.registerNormTheorems pre post | _ => throwUnsupportedSyntax -private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do - let minIndexable := false -- TODO: infer it - let kinds ← match s.getKindsFor (.decl declName) with - | [] => return () - | [k] => pure m!"@{k.toAttribute minIndexable}" - | [.eqLhs gen, .eqRhs _] - | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}" - | ks => - let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}" - pure m!"{ks}" - logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`" - private def parseModifier (s : String) : CoreM Grind.AttrKind := do let stx := Parser.runParserCategory (← getEnv) `Lean.Parser.Attr.grindMod s match stx with @@ -90,30 +78,9 @@ private def parseModifier (s : String) : CoreM Grind.AttrKind := do | _ => throwError "unexpected modifier {s}" open PremiseSelection in -def elabGrindParams - (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) - (premises : Array Suggestion := #[]) (lax : Bool := false) : - MetaM Grind.Params := do +def elabGrindPremises + (params : Grind.Params) (premises : Array Suggestion := #[]) : MetaM Grind.Params := do let mut params := params - for p in ps do - try - match p with - | `(Parser.Tactic.grindParam| - $id:ident) => - let declName ← realizeGlobalConstNoOverloadWithInfo id - if let some declName ← Grind.isCasesAttrCandidate? declName false then - Grind.ensureNotBuiltinCases declName - params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) } - else if (← Grind.isInjectiveTheorem declName) then - params := { params with inj := params.inj.erase (.decl declName) } - else - params := { params with ematch := (← params.ematch.eraseDecl declName) } - | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) => - params ← processParam params p mod? id (minIndexable := false) - | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) => - params ← processParam params p mod? id (minIndexable := true) - | _ => throwError "unexpected `grind` parameter{indentD p}" - catch ex => - if !lax then throw ex for p in premises do let attr ← match p.flag with | some flag => parseModifier flag @@ -130,108 +97,15 @@ def elabGrindParams -- Let's only do this if there is a prospect of a premise selector supprting this. throwError "unexpected modifier {p.flag}" return params -where - ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do - if minIndexable then - throwError "redundant modifier `!` in `grind` parameter" - processParam (params : Grind.Params) - (p : TSyntax `Lean.Parser.Tactic.grindParam) - (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod)) - (id : TSyntax `ident) - (minIndexable : Bool) - : MetaM Grind.Params := do - let mut params := params - let declName ← try - realizeGlobalConstNoOverloadWithInfo id - catch err => - if (← resolveLocalName id.getId).isSome then - throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically" - else - throw err - let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer - match kind with - | .ematch .user => - unless only do - withRef p <| Grind.throwInvalidUsrModifier - ensureNoMinIndexable minIndexable - let s ← Grind.getEMatchTheorems - let thms := s.find (.decl declName) - let thms := thms.filter fun thm => thm.kind == .user - if thms.isEmpty then - throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`" - for thm in thms do - params := { params with extra := params.extra.push thm } - | .ematch kind => - params ← withRef p <| addEMatchTheorem params id declName kind minIndexable - | .cases eager => - ensureNoMinIndexable minIndexable - withRef p <| Grind.validateCasesAttr declName eager - params := { params with casesTypes := params.casesTypes.insert declName eager } - | .intro => - if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then - for ctor in info.ctors do - params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable - else - throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate" - | .inj => - let thm ← Grind.mkInjectiveTheorem declName - params := { params with inj := params.inj.insert thm } - | .ext => - throwError "`[grind ext]` cannot be set using parameters" - | .infer => - if let some declName ← Grind.isCasesAttrCandidate? declName false then - params := { params with casesTypes := params.casesTypes.insert declName false } - if let some info ← isInductivePredicate? declName then - -- If it is an inductive predicate, - -- we also add the constructors (intro rules) as E-matching rules - for ctor in info.ctors do - -- **Note**: We should not warn if `declName` is an inductive - params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False) - else - params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true) - | .symbol prio => - ensureNoMinIndexable minIndexable - params := { params with symPrios := params.symPrios.insert declName prio } - return params - - addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name) - (kind : Grind.EMatchTheoremKind) - (minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do - let info ← getAsyncConstInfo declName - match info.kind with - | .thm | .axiom | .ctor => - match kind with - | .eqBoth gen => - ensureNoMinIndexable minIndexable - let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios - let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios - if warn && - params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns && - params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then - warnRedundantEMatchArg params.ematch declName - return { params with extra := params.extra.push thm₁ |>.push thm₂ } - | _ => - if kind matches .eqLhs _ | .eqRhs _ then - ensureNoMinIndexable minIndexable - let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then - Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true) - else - Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable) - if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then - warnRedundantEMatchArg params.ematch declName - return { params with extra := params.extra.push thm } - | .defn => - if (← isReducible declName) then - throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them" - if !kind.isEqLhs && !kind.isDefault then - throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='" - ensureNoMinIndexable minIndexable - let some thms ← Grind.mkEMatchEqTheoremsForDef? declName - | throwError "failed to generate equation theorems for `{.ofConstName declName}`" - return { params with extra := params.extra ++ thms.toPArray' } - | _ => - throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type" +open PremiseSelection in +def elabGrindParamsAndPremises + (params : Grind.Params) + (ps : TSyntaxArray ``Parser.Tactic.grindParam) + (premises : Array Suggestion := #[]) + (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do + let params ← elabGrindParams params ps (lax := lax) (only := only) + elabGrindPremises params premises def mkGrindParams (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) : @@ -246,7 +120,7 @@ def mkGrindParams pure suggestions else pure #[] - let params ← elabGrindParams params ps only premises (lax := config.lax) + let params ← elabGrindParamsAndPremises params ps premises (only := only) (lax := config.lax) trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}" return params diff --git a/src/Lean/Elab/Tactic/Grind/Param.lean b/src/Lean/Elab/Tactic/Grind/Param.lean new file mode 100644 index 0000000000..a1d8495bf1 --- /dev/null +++ b/src/Lean/Elab/Tactic/Grind/Param.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Lean.Meta.Tactic.Grind.Main +import Lean.Elab.Tactic.Grind.Basic +import Lean.Elab.Tactic.Grind.Anchor +namespace Lean.Elab.Tactic +open Meta + +/-! +`grind` parameter elaboration +-/ + +def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do + let minIndexable := false -- TODO: infer it + let kinds ← match s.getKindsFor (.decl declName) with + | [] => return () + | [k] => pure m!"@{k.toAttribute minIndexable}" + | [.eqLhs gen, .eqRhs _] + | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}" + | ks => + let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}" + pure m!"{ks}" + logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`" + +def parseModifier (s : String) : CoreM Grind.AttrKind := do + let stx := Parser.runParserCategory (← getEnv) `Lean.Parser.Attr.grindMod s + match stx with + | .ok stx => Grind.getAttrKindCore stx + | _ => throwError "unexpected modifier {s}" + +def ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do + if minIndexable then + throwError "redundant modifier `!` in `grind` parameter" + +public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name) + (kind : Grind.EMatchTheoremKind) + (minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do + let info ← getAsyncConstInfo declName + match info.kind with + | .thm | .axiom | .ctor => + match kind with + | .eqBoth gen => + ensureNoMinIndexable minIndexable + let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios + let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios + if warn && + params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns && + params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then + warnRedundantEMatchArg params.ematch declName + return { params with extra := params.extra.push thm₁ |>.push thm₂ } + | _ => + if kind matches .eqLhs _ | .eqRhs _ then + ensureNoMinIndexable minIndexable + let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then + Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true) + else + Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable) + if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then + warnRedundantEMatchArg params.ematch declName + return { params with extra := params.extra.push thm } + | .defn => + if (← isReducible declName) then + throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them" + if !kind.isEqLhs && !kind.isDefault then + throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='" + ensureNoMinIndexable minIndexable + let some thms ← Grind.mkEMatchEqTheoremsForDef? declName + | throwError "failed to generate equation theorems for `{.ofConstName declName}`" + return { params with extra := params.extra ++ thms.toPArray' } + | _ => + throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type" + +def processParam (params : Grind.Params) + (p : TSyntax `Lean.Parser.Tactic.grindParam) + (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod)) + (id : TSyntax `ident) + (minIndexable : Bool) + (only : Bool) + : MetaM Grind.Params := do + let mut params := params + let declName ← try + realizeGlobalConstNoOverloadWithInfo id + catch err => + if (← resolveLocalName id.getId).isSome then + throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically" + else + throw err + let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer + match kind with + | .ematch .user => + unless only do + withRef p <| Grind.throwInvalidUsrModifier + ensureNoMinIndexable minIndexable + let s ← Grind.getEMatchTheorems + let thms := s.find (.decl declName) + let thms := thms.filter fun thm => thm.kind == .user + if thms.isEmpty then + throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`" + for thm in thms do + params := { params with extra := params.extra.push thm } + | .ematch kind => + params ← withRef p <| addEMatchTheorem params id declName kind minIndexable + | .cases eager => + ensureNoMinIndexable minIndexable + withRef p <| Grind.validateCasesAttr declName eager + params := { params with casesTypes := params.casesTypes.insert declName eager } + | .intro => + if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then + for ctor in info.ctors do + params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable + else + throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate" + | .inj => + let thm ← Grind.mkInjectiveTheorem declName + params := { params with inj := params.inj.insert thm } + | .ext => + throwError "`[grind ext]` cannot be set using parameters" + | .infer => + if let some declName ← Grind.isCasesAttrCandidate? declName false then + params := { params with casesTypes := params.casesTypes.insert declName false } + if let some info ← isInductivePredicate? declName then + -- If it is an inductive predicate, + -- we also add the constructors (intro rules) as E-matching rules + for ctor in info.ctors do + -- **Note**: We should not warn if `declName` is an inductive + params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False) + else + params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true) + | .symbol prio => + ensureNoMinIndexable minIndexable + params := { params with symPrios := params.symPrios.insert declName prio } + return params + +def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind.Params := do + let anchorRefs := params.anchorRefs?.getD #[] + let anchorRef ← Grind.elabAnchorRef val + return { params with anchorRefs? := some <| anchorRefs.push anchorRef } + +public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) + (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do + let mut params := params + for p in ps do + try + match p with + | `(Parser.Tactic.grindParam| - $id:ident) => + let declName ← realizeGlobalConstNoOverloadWithInfo id + if let some declName ← Grind.isCasesAttrCandidate? declName false then + Grind.ensureNotBuiltinCases declName + params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) } + else if (← Grind.isInjectiveTheorem declName) then + params := { params with inj := params.inj.erase (.decl declName) } + else + params := { params with ematch := (← params.ematch.eraseDecl declName) } + | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) => + params ← processParam params p mod? id (minIndexable := false) (only := only) + | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) => + params ← processParam params p mod? id (minIndexable := true) (only := only) + | `(Parser.Tactic.grindParam| #$anchor:hexnum) => + unless only do + throwErrorAt anchor "invalid anchor, `only` modifier expected" + params ← processAnchor params anchor + | _ => throwError "unexpected `grind` parameter{indentD p}" + catch ex => + if !lax then throw ex + return params + +end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic/Grind/Anchor.lean b/src/Lean/Meta/Tactic/Grind/Anchor.lean index ac23f9f27a..ad1b836d1c 100644 --- a/src/Lean/Meta/Tactic/Grind/Anchor.lean +++ b/src/Lean/Meta/Tactic/Grind/Anchor.lean @@ -86,11 +86,11 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do return a /-- -Example: `isAnchorPrefix 4 0x0c88 0x0c88ab10ef20206a` returns `true` +Example: `{ numDigits := 4, anchorPrefix := 0x0c88 }.matches 0x0c88ab10ef20206a` returns `true` -/ -public def isAnchorPrefix (numHexDigits : Nat) (anchorPrefix : UInt64) (anchor : UInt64) : Bool := - let shift := 64 - numHexDigits.toUInt64*4 - anchorPrefix == anchor >>> shift +public def AnchorRef.matches (anchorRef : AnchorRef) (anchor : UInt64) : Bool := + let shift := 64 - anchorRef.numDigits.toUInt64*4 + anchorRef.anchorPrefix == anchor >>> shift public class HasAnchor (α : Type u) where getAnchor : α → UInt64 @@ -124,12 +124,15 @@ public structure ExprWithAnchor where public instance : HasAnchor ExprWithAnchor where getAnchor e := e.anchor -public def mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do +public def mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax ``Parser.Tactic.anchor) := do let hexnum := mkNode `hexnum #[mkAtom (anchorPrefixToString numDigits anchorPrefix)] - `(Parser.Tactic.Grind.anchor| #$hexnum) + `(Parser.Tactic.anchor| #$hexnum) -public def mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do +public def mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax ``Parser.Tactic.anchor) := do let anchorPrefix := anchor >>> (64 - 4*numDigits.toUInt64) mkAnchorSyntaxFromPrefix numDigits anchorPrefix +public def SplitInfo.getAnchor (s : SplitInfo) : GrindM UInt64 := do + Grind.getAnchor s.getExpr + end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean index e585711c36..475a461470 100644 --- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean +++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean @@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.PropagatorAttr import Lean.Meta.Tactic.Grind.Propagate import Lean.Meta.Tactic.Grind.Internalize import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.Anchor import Lean.Meta.Tactic.Grind.EqResolution import Lean.Meta.Tactic.Grind.SynthInstance public section @@ -74,6 +75,15 @@ private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : E private def isNewPat (patternsFoundSoFar : Array (List Expr)) (thm' : EMatchTheorem) : Bool := patternsFoundSoFar.all fun ps => thm'.patterns != ps +/-- +Returns `true`, if there are no anchor references restricting the search, +or there is an anchor references `ref` s.t. `ref` matches `proof`. +-/ +private def checkAnchorRefs (proof : Expr) : GrindM Bool := do + let some anchorRefs ← getAnchorRefs | return true + let anchor ← getAnchor (← inferType proof) + return anchorRefs.any (·.matches anchor) + private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do let proof ← mkEqTrueProof e let origin ← if let some fvarId := isEqTrueHyp? proof then @@ -82,6 +92,9 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do let idx ← modifyGet fun s => (s.ematch.nextThmIdx, { s with ematch.nextThmIdx := s.ematch.nextThmIdx + 1 }) pure <| .local ((`local).appendIndexAfter idx) let proof := mkOfEqTrueCore e proof + -- **Note**: Do we really need to restrict the instantiation of local theorems? + -- **Note**: Should we distinguish anchors restricting case-splits and local theorems? + unless (← checkAnchorRefs proof) do return () let size := (← get).ematch.newThms.size let gen ← getGeneration e let mut patternsFoundSoFar := #[] diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 69edf84167..6f49beb072 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Main.lean @@ -29,14 +29,15 @@ public section namespace Lean.Meta.Grind structure Params where - config : Grind.Config - ematch : EMatchTheorems := default - inj : InjectiveTheorems := default - symPrios : SymbolPriorities := {} - casesTypes : CasesTypes := {} - extra : PArray EMatchTheorem := {} - norm : Simp.Context - normProcs : Array Simprocs + config : Grind.Config + ematch : EMatchTheorems := default + inj : InjectiveTheorems := default + symPrios : SymbolPriorities := {} + casesTypes : CasesTypes := {} + extra : PArray EMatchTheorem := {} + norm : Simp.Context + normProcs : Array Simprocs + anchorRefs? : Option (Array AnchorRef) := none -- TODO: inductives to split def mkParams (config : Grind.Config) : MetaM Params := do @@ -90,7 +91,8 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti let simp := params.norm let config := params.config let symPrios := params.symPrios - x (← mkMethods evalTactic?).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios } + let anchorRefs? := params.anchorRefs? + x (← mkMethods evalTactic?).toMethodsRef { config, anchorRefs?, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios } |>.run' { scState } private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean index 470353f3cb..0461f80aa5 100644 --- a/src/Lean/Meta/Tactic/Grind/Split.lean +++ b/src/Lean/Meta/Tactic/Grind/Split.lean @@ -167,6 +167,15 @@ private inductive SplitCandidate where | none | some (c : SplitInfo) (numCases : Nat) (isRec : Bool) (tryPostpone : Bool) +/-- +Returns `true`, if there are no anchor references restricting the search, +or there is an anchor references `ref` s.t. `ref` matches `c`. +-/ +private def checkAnchorRefs (c : SplitInfo) : GrindM Bool := do + let some anchorRefs ← getAnchorRefs | return true + let anchor ← c.getAnchor + return anchorRefs.any (·.matches anchor) + /-- Returns the next case-split to be performed. It uses a very simple heuristic. -/ private def selectNextSplit? : GoalM SplitCandidate := do if (← isInconsistent) then return .none @@ -186,30 +195,38 @@ where modify fun s => { s with split.num := numSplits, ematch.num := 0 } return c? | c::cs => - trace_goal[grind.debug.split] "checking: {c.getExpr}" - match (← checkSplitStatus c) with - | .notReady => go cs c? (c::cs') - | .resolved => go cs c? cs' - | .ready numCases isRec tryPostpone => - if (← cheapCasesOnly) && numCases > 1 then - go cs c? (c::cs') - else match c? with - | .none => go cs (.some c numCases isRec tryPostpone) cs' - | .some c' numCases' _ tryPostpone' => - let isBetter : GoalM Bool := do - if tryPostpone' && !tryPostpone then - return true - else if tryPostpone && !tryPostpone' then - return false - else if numCases == 1 && !isRec && numCases' > 1 then - return true - if (← getGeneration c.getExpr) < (← getGeneration c'.getExpr) then - return true - return numCases < numCases' - if (← isBetter) then - go cs (.some c numCases isRec tryPostpone) (c'::cs') - else + if !(← checkAnchorRefs c) then + /- + **Note**: `grind`s context contains anchor references restricting the + case-splits that can be performed, and `c` does not matches any of + the references provided. + -/ + go cs c? cs' + else + trace_goal[grind.debug.split] "checking: {c.getExpr}" + match (← checkSplitStatus c) with + | .notReady => go cs c? (c::cs') + | .resolved => go cs c? cs' + | .ready numCases isRec tryPostpone => + if (← cheapCasesOnly) && numCases > 1 then go cs c? (c::cs') + else match c? with + | .none => go cs (.some c numCases isRec tryPostpone) cs' + | .some c' numCases' _ tryPostpone' => + let isBetter : GoalM Bool := do + if tryPostpone' && !tryPostpone then + return true + else if tryPostpone && !tryPostpone' then + return false + else if numCases == 1 && !isRec && numCases' > 1 then + return true + if (← getGeneration c.getExpr) < (← getGeneration c'.getExpr) then + return true + return numCases < numCases' + if (← isBetter) then + go cs (.some c numCases isRec tryPostpone) (c'::cs') + else + go cs c? (c::cs') private def mkGrindEM (c : Expr) := mkApp (mkConst ``Lean.Grind.em) c @@ -266,7 +283,7 @@ def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return tr let candidates := (← get).split.candidates let candidates ← candidates.toArray.filterMapM fun c => do let e := c.getExpr - let anchor ← getAnchor e + let anchor ← c.getAnchor let status ← checkSplitStatus c -- **Note**: we ignore case-splits that are not ready or have already been resolved. -- We may consider adding an option for including "not-ready" splits in the future. diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 33cc66f2cb..171df0073e 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -57,6 +57,15 @@ register_builtin_option grind.warning : Bool := { descr := "generate a warning whenever `grind` is used" } +/-- +Anchors are used to reference terms, local theorems, and case-splits in the `grind` state. +We also use anchors to prune the search space when they are provided as `grind` parameters +and the `finish` tactic. +-/ +structure AnchorRef where + numDigits : Nat + anchorPrefix : UInt64 + /-- Opaque solver extension state. -/ opaque SolverExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩ @[expose] def SolverExtensionState : Type := SolverExtensionStateSpec.fst @@ -101,6 +110,11 @@ structure Context where simpMethods : Simp.Methods config : Grind.Config /-- + If `anchorRefs? := some anchorRefs`, then only local instances and case-splits in `anchorRefs` + are considered. + -/ + anchorRefs? : Option (Array AnchorRef) + /-- If `cheapCases` is `true`, `grind` only applies `cases` to types that contain at most one minor premise. Recall that `grind` applies `cases` when introducing types tagged with `[grind cases eager]`, @@ -298,6 +312,10 @@ def getOrderingEqExpr : GrindM Expr := do def getIntExpr : GrindM Expr := do return (← readThe Context).intExpr +/-- Returns the anchor references (if any) being used to restrict the search. -/ +def getAnchorRefs : GrindM (Option (Array AnchorRef)) := do + return (← readThe Context).anchorRefs? + def resetAnchors : GrindM Unit := do modify fun s => { s with anchors := {} } @@ -1878,6 +1896,12 @@ def anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String := def anchorToString (numDigits : Nat) (anchor : UInt64) : String := anchorPrefixToString numDigits (anchor >>> (64 - 4*numDigits.toUInt64)) +def AnchorRef.toString (anchorRef : AnchorRef) : String := + anchorPrefixToString anchorRef.numDigits anchorRef.anchorPrefix + +instance : ToString AnchorRef where + toString := AnchorRef.toString + /-- Returns activated `match`-declaration equations. Recall that in tactics such as `instantiate only [...]`, `match`-declarations are always instantiated. diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean index 9fd9036f89..b4e40a78c6 100644 --- a/tests/lean/run/grind_finish_trace.lean +++ b/tests/lean/run/grind_finish_trace.lean @@ -178,3 +178,76 @@ example (f : Int → Int) (x y : Int) have : x ≠ 0 have : x ≠ 1 have : x ≠ 2 + +example (f g : Int → Int) (x y z w : Int) + : 0 ≤ x → x ≤ 1 → 0 ≤ w → + g 0 = z → g 1 = z → g 2 = z → + f 0 = y → f 1 = y → + g w ≠ z → f x = y := by + set_option trace.grind.split true in + grind => + mbtc + cases #23ad + mbtc + cases #beb4 + +/-- +trace: [grind.split] w = 0, generation: 0 +[grind.split] x = 0, generation: 0 +[grind.split] w = 1, generation: 0 +[grind.split] x = 1, generation: 0 +-/ +#guard_msgs in +example (f g : Int → Int) (x y z w : Int) + : 0 ≤ x → x ≤ 1 → 0 ≤ w → + g 0 = z → g 1 = z → g 2 = z → + f 0 = y → f 1 = y → + g w ≠ z → f x = y := by + set_option trace.grind.split true in + grind + +/-- +trace: [grind.split] x = 0, generation: 0 +[grind.split] x = 1, generation: 0 +-/ +#guard_msgs in +example (f g : Int → Int) (x y z w : Int) + : 0 ≤ x → x ≤ 1 → 0 ≤ w → + g 0 = z → g 1 = z → g 2 = z → + f 0 = y → f 1 = y → + g w ≠ z → f x = y := by + fail_if_success grind [#23ad] -- not possible to solve using this set of anchors. + set_option trace.grind.split true in + grind only [#23ad, #beb4] -- Only these two splits were performed. + +/-- +trace: [grind.ematch.instance] h: f (f a) = f a +[grind.ematch.instance] h: f (f (f a)) = f (f a) +[grind.ematch.instance] h: f (f (f (f a))) = f (f (f a)) +[grind.ematch.instance] h_1: g (g (g b)) = g (g b) +[grind.ematch.instance] h_1: g (g b) = g b +-/ +#guard_msgs in +example (f g : Int → Int) + (_ : ∀ x, f (f x) = f x) + (_ : ∀ x, g (g x) = g x) + (a b : Int) + (_ : g (g b) = b) + : f (f (f a)) = f a := by + set_option trace.grind.ematch.instance true in + grind + +/-- +trace: [grind.ematch.instance] h: f (f a) = f a +[grind.ematch.instance] h: f (f (f a)) = f (f a) +[grind.ematch.instance] h: f (f (f (f a))) = f (f (f a)) +-/ +#guard_msgs in +example (f g : Int → Int) + (_ : ∀ x, f (f x) = f x) + (_ : ∀ x, g (g x) = g x) + (a b : Int) + (_ : g (g b) = b) + : f (f (f a)) = f a := by + set_option trace.grind.ematch.instance true in + grind only [#99cb]