From facc56609d8f42378d0cdd1e61e3ce4cf0876868 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jan 2025 18:36:26 -0800 Subject: [PATCH] feat: add `[grind cases]` and `[grind cases eager]` attributes This PR adds the attributes `[grind cases]` and `[grind cases eager]` for controlling case splitting in `grind`. They will replace the `[grind_cases]` and the configuration option `splitIndPred`. After update stage0, we will push the second part of this PR. --- src/Init/Grind/Tactics.lean | 8 +- src/Lean/Elab/Tactic/Grind.lean | 63 +++++----- src/Lean/Meta/Tactic/Grind/Attr.lean | 70 +++++++++++- src/Lean/Meta/Tactic/Grind/Cases.lean | 73 ++++++++++++ src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 108 ++++++------------ src/Lean/Meta/Tactic/Grind/Main.lean | 12 +- tests/lean/run/grind_cases.lean | 34 ++++++ 7 files changed, 255 insertions(+), 113 deletions(-) diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 0a234217a1a3..0f9b5082660b 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -14,10 +14,12 @@ syntax grindEqRhs := atomic("=" "_") syntax grindEqBwd := atomic("←" "=") syntax grindBwd := "←" syntax grindFwd := "→" +syntax grindCases := &"cases" +syntax grindCasesEager := atomic(&"cases" &"eager") -syntax grindThmMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd +syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindCasesEager <|> grindCases -syntax (name := grind) "grind" (grindThmMod)? : attr +syntax (name := grind) "grind" (grindMod)? : attr end Lean.Parser.Attr @@ -65,7 +67,7 @@ namespace Lean.Parser.Tactic -/ syntax grindErase := "-" ident -syntax grindLemma := (Attr.grindThmMod)? ident +syntax grindLemma := (Attr.grindMod)? ident syntax grindParam := grindErase <|> grindLemma syntax (name := grind) diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 41dfdb105182..2c753e944432 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -51,41 +51,52 @@ def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic. match p with | `(Parser.Tactic.grindParam| - $id:ident) => let declName ← realizeGlobalConstNoOverloadWithInfo id - if (← isInductivePredicate declName) then - throwErrorAt p "NIY" + if (← Grind.isCasesAttrCandidate declName false) then + params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) } else params := { params with ematch := (← params.ematch.eraseDecl declName) } - | `(Parser.Tactic.grindParam| $[$mod?:grindThmMod]? $id:ident) => + | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) => let declName ← realizeGlobalConstNoOverloadWithInfo id - let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default - if (← isInductivePredicate declName) then - throwErrorAt p "NIY" - else - let info ← getConstInfo declName - match info with - | .thmInfo _ => - if kind == .eqBoth then - params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) } - params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) } - else - params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) } - | .defnInfo _ => - if (← isReducible declName) then - throwErrorAt p "`{declName}` is a reducible definition, `grind` automatically unfolds them" - if kind != .eqLhs && kind != .default then - throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='" - let some thms ← Grind.mkEMatchEqTheoremsForDef? declName - | throwErrorAt p "failed to genereate equation theorems for `{declName}`" - params := { params with extra := params.extra ++ thms.toPArray' } - | _ => - throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type" + let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer + match kind with + | .ematch kind => + params ← withRef p <| addEMatchTheorem params declName kind + | .cases eager => + withRef p <| Grind.validateCasesAttr declName eager + params := { params with casesTypes := params.casesTypes.insert declName eager } + | .infer => + if (← Grind.isCasesAttrCandidate declName false) then + params := { params with casesTypes := params.casesTypes.insert declName false } + else + params ← withRef p <| addEMatchTheorem params declName .default | _ => throwError "unexpected `grind` parameter{indentD p}" return params +where + addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.TheoremKind) : MetaM Grind.Params := do + let info ← getConstInfo declName + match info with + | .thmInfo _ => + if kind == .eqBoth then + let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) } + return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) } + else + return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) } + | .defnInfo _ => + if (← isReducible declName) then + throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them" + if kind != .eqLhs && kind != .default then + throwError "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='" + let some thms ← Grind.mkEMatchEqTheoremsForDef? declName + | throwError "failed to genereate equation theorems for `{declName}`" + return { params with extra := params.extra ++ thms.toPArray' } + | _ => + throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type" def mkGrindParams (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do let params ← Grind.mkParams config let ematch ← if only then pure {} else Grind.getEMatchTheorems - let params := { params with ematch } + let casesTypes ← if only then pure {} else Grind.getCasesTypes + let params := { params with ematch, casesTypes } elabGrindParams params ps def grind diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean index 70b5f5228a7f..7bb6c610d645 100644 --- a/src/Lean/Meta/Tactic/Grind/Attr.lean +++ b/src/Lean/Meta/Tactic/Grind/Attr.lean @@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Meta.Tactic.Simp.Attr -import Lean.Meta.Tactic.Simp.Simproc +import Lean.Meta.Tactic.Grind.EMatchTheorem +import Lean.Meta.Tactic.Grind.Cases namespace Lean.Meta.Grind -open Simp - +--- TODO: delete builtin_initialize grindCasesExt : SimpleScopedEnvExtension Name NameSet ← registerSimpleScopedEnvExtension { initial := {} @@ -59,5 +58,68 @@ builtin_initialize validateGrindCasesAttr declName grindCasesExt.add declName attrKind } +--- END of TODO: detele + +inductive AttrKind where + | ematch (k : TheoremKind) + | cases (eager : Bool) + | infer + +/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/ +def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do + match stx with + | `(Parser.Attr.grindMod| =) => return .ematch .eqLhs + | `(Parser.Attr.grindMod| →) => return .ematch .fwd + | `(Parser.Attr.grindMod| ←) => return .ematch .bwd + | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs + | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth + | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd + | `(Parser.Attr.grindMod| cases) => return .cases false + | `(Parser.Attr.grindMod| cases eager) => return .cases true + | _ => throwError "unexpected `grind` theorem kind: `{stx}`" + +/-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/ +def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do + if stx[1].isNone then + return .infer + else + getAttrKindCore stx[1][0] + +builtin_initialize + registerBuiltinAttribute { + name := `grind + descr := + "The `[grind]` attribute is used to annotate declarations.\ + \ + When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\ + will mark the theorem for use in heuristic instantiations by the `grind` tactic, + using respectively the left-hand side, the right-hand side, or both sides of the theorem.\ + When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\ + When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem + (that is, it will use the theorem for backwards reasoning).\ + When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses + (that is, it will use the theorem for forwards reasoning).\ + \ + The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\ + \ + The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\ + For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\ + `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`." + applicationTime := .afterCompilation + add := fun declName stx attrKind => MetaM.run' do + match (← getAttrKindFromOpt stx) with + | .ematch k => addEMatchAttr declName attrKind k + | .cases eager => addCasesAttr declName eager attrKind + | .infer => + if (← isCasesAttrCandidate declName false) then + addCasesAttr declName false attrKind + else + addEMatchAttr declName attrKind .default + erase := fun declName => MetaM.run' do + if (← isCasesAttrCandidate declName false) then + eraseCasesAttr declName + else + eraseEMatchAttr declName + } end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index ea81d88ddb13..0533dad908d9 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -7,6 +7,79 @@ prelude import Lean.Meta.Tactic.Cases namespace Lean.Meta.Grind + +/-- Types that `grind` will case-split on. -/ +structure CasesTypes where + casesMap : PHashMap Name Bool := {} + deriving Inhabited + +structure CasesEntry where + declName : Name + eager : Bool + deriving Inhabited + +/-- Returns `true` if `s` contains a `declName`. -/ +def CasesTypes.contains (s : CasesTypes) (declName : Name) : Bool := + s.casesMap.contains declName + +/-- Removes the given declaration from `s`. -/ +def CasesTypes.erase (s : CasesTypes) (declName : Name) : CasesTypes := + { s with casesMap := s.casesMap.erase declName } + +def CasesTypes.insert (s : CasesTypes) (declName : Name) (eager : Bool) : CasesTypes := + { s with casesMap := s.casesMap.insert declName eager } + +def CasesTypes.find? (s : CasesTypes) (declName : Name) : Option Bool := + s.casesMap.find? declName + +builtin_initialize casesExt : SimpleScopedEnvExtension CasesEntry CasesTypes ← + registerSimpleScopedEnvExtension { + initial := {} + addEntry := fun s {declName, eager} => s.insert declName eager + } + +def getCasesTypes : CoreM CasesTypes := + return casesExt.getState (← getEnv) + +private def getAlias? (value : Expr) : MetaM (Option Name) := + lambdaTelescope value fun _ body => do + if let .const declName _ := body.getAppFn' then + return some declName + else + return none + +partial def isCasesAttrCandidate (declName : Name) (eager : Bool) : CoreM Bool := do + match (← getConstInfo declName) with + | .inductInfo info => return !info.isRec || !eager + | .defnInfo info => + let some declName ← getAlias? info.value |>.run' {} {} + | return false + isCasesAttrCandidate declName eager + | _ => return false + +def validateCasesAttr (declName : Name) (eager : Bool) : CoreM Unit := do + unless (← isCasesAttrCandidate declName eager) do + if eager then + throwError "invalid `[grind cases eager]`, `{declName}` is not a non-recursive inductive datatype or an alias for one" + else + throwError "invalid `[grind cases]`, `{declName}` is not an inductive datatype or an alias for one" + +def addCasesAttr (declName : Name) (eager : Bool) (attrKind : AttributeKind) : CoreM Unit := do + validateCasesAttr declName eager + casesExt.add { declName, eager } attrKind + +def CasesTypes.eraseDecl (s : CasesTypes) (declName : Name) : CoreM CasesTypes := do + if s.contains declName then + return s.erase declName + else + throwError "`{declName}` is not marked with the `[grind]` attribute" + +def eraseCasesAttr (declName : Name) : CoreM Unit := do + let s := casesExt.getState (← getEnv) + let s ← s.eraseDecl declName + modifyEnv fun env => casesExt.modifyState env fun _ => s + + /-- The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users. This method implements it. diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index d1cb334d351f..51611f66b69d 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -142,7 +142,7 @@ def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchThe def EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool := s.origins.contains origin -/-- Mark the theorm with the given origin as `erased` -/ +/-- Mark the theorem with the given origin as `erased` -/ def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems := { s with erased := s.erased.insert origin, origins := s.origins.erase origin } @@ -705,24 +705,6 @@ where levelParams, origin } -/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/ -def getTheoremKindCore (stx : Syntax) : CoreM TheoremKind := do - match stx with - | `(Parser.Attr.grindThmMod| =) => return .eqLhs - | `(Parser.Attr.grindThmMod| →) => return .fwd - | `(Parser.Attr.grindThmMod| ←) => return .bwd - | `(Parser.Attr.grindThmMod| =_) => return .eqRhs - | `(Parser.Attr.grindThmMod| _=_) => return .eqBoth - | `(Parser.Attr.grindThmMod| ←=) => return .eqBwd - | _ => throwError "unexpected `grind` theorem kind: `{stx}`" - -/-- Return theorem kind for `stx` of the form `(Attr.grindThmMod)?` -/ -def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do - if stx[1].isNone then - return .default - else - getTheoremKindCore stx[1][0] - def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command" @@ -743,20 +725,6 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind else throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions" -private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do - if thmKind == .eqLhs then - addGrindEqAttr declName attrKind thmKind (useLhs := true) - else if thmKind == .eqRhs then - addGrindEqAttr declName attrKind thmKind (useLhs := false) - else if thmKind == .eqBoth then - addGrindEqAttr declName attrKind thmKind (useLhs := true) - addGrindEqAttr declName attrKind thmKind (useLhs := false) - else if !(← getConstInfo declName).isTheorem then - addGrindEqAttr declName attrKind thmKind - else - let thm ← mkEMatchTheoremForDecl declName thmKind - ematchTheoremsExt.add thm attrKind - def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do let throwErr {α} : MetaM α := throwError "`{declName}` is not marked with the `[grind]` attribute" @@ -774,47 +742,37 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat throwErr return s.erase <| .decl declName -builtin_initialize - registerBuiltinAttribute { - name := `grind - descr := - "The `[grind]` attribute is used to annotate declarations.\ - \ - When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\ - will mark the theorem for use in heuristic instantiations by the `grind` tactic, - using respectively the left-hand side, the right-hand side, or both sides of the theorem.\ - When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\ - When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem - (that is, it will use the theorem for backwards reasoning).\ - When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses - (that is, it will use the theorem for forwards reasoning).\ - \ - The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\ - \ - The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\ - For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\ - `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`." - applicationTime := .afterCompilation - add := fun declName stx attrKind => do - addGrindAttr declName attrKind (← getTheoremKindFromOpt stx) |>.run' {} - erase := fun declName => MetaM.run' do - /- - Remark: consider the following example - ``` - attribute [grind] foo -- ok - attribute [-grind] foo.eqn_2 -- ok - attribute [-grind] foo -- error - ``` - One may argue that the correct behavior should be - ``` - attribute [grind] foo -- ok - attribute [-grind] foo.eqn_2 -- error - attribute [-grind] foo -- ok - ``` - -/ - let s := ematchTheoremsExt.getState (← getEnv) - let s ← s.eraseDecl declName - modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s - } +def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do + if thmKind == .eqLhs then + addGrindEqAttr declName attrKind thmKind (useLhs := true) + else if thmKind == .eqRhs then + addGrindEqAttr declName attrKind thmKind (useLhs := false) + else if thmKind == .eqBoth then + addGrindEqAttr declName attrKind thmKind (useLhs := true) + addGrindEqAttr declName attrKind thmKind (useLhs := false) + else if !(← getConstInfo declName).isTheorem then + addGrindEqAttr declName attrKind thmKind + else + let thm ← mkEMatchTheoremForDecl declName thmKind + ematchTheoremsExt.add thm attrKind + +def eraseEMatchAttr (declName : Name) : MetaM Unit := do + /- + Remark: consider the following example + ``` + attribute [grind] foo -- ok + attribute [-grind] foo.eqn_2 -- ok + attribute [-grind] foo -- error + ``` + One may argue that the correct behavior should be + ``` + attribute [grind] foo -- ok + attribute [-grind] foo.eqn_2 -- error + attribute [-grind] foo -- ok + ``` + -/ + let s := ematchTheoremsExt.getState (← getEnv) + let s ← s.eraseDecl declName + modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index a8f1c9f9824e..d99940b91c1c 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Main.lean @@ -17,15 +17,17 @@ import Lean.Meta.Tactic.Grind.EMatch import Lean.Meta.Tactic.Grind.Split import Lean.Meta.Tactic.Grind.Solve import Lean.Meta.Tactic.Grind.SimpUtil +import Lean.Meta.Tactic.Grind.Cases namespace Lean.Meta.Grind structure Params where - config : Grind.Config - ematch : EMatchTheorems := {} - extra : PArray EMatchTheorem := {} - norm : Simp.Context - normProcs : Array Simprocs + config : Grind.Config + ematch : EMatchTheorems := {} + casesTypes : CasesTypes := {} + extra : PArray EMatchTheorem := {} + norm : Simp.Context + normProcs : Array Simprocs -- TODO: inductives to split def mkParams (config : Grind.Config) : MetaM Params := do diff --git a/tests/lean/run/grind_cases.lean b/tests/lean/run/grind_cases.lean index 8672c5ddd7af..6ce5ef3eda90 100644 --- a/tests/lean/run/grind_cases.lean +++ b/tests/lean/run/grind_cases.lean @@ -27,3 +27,37 @@ attribute [grind_cases] And attribute [grind_cases] False attribute [grind_cases] Empty + +-- TODO: delete everything above + +/-- +error: invalid `[grind cases eager]`, `List` is not a non-recursive inductive datatype or an alias for one +-/ +#guard_msgs (error) in +attribute [grind cases eager] List + +attribute [grind cases] List + +attribute [grind] Prod + +/-- +error: invalid `[grind cases]`, `id` is not an inductive datatype or an alias for one +-/ +#guard_msgs (error) in +attribute [grind cases] id + +/-- +error: invalid `[grind cases eager]`, `id` is not a non-recursive inductive datatype or an alias for one +-/ +#guard_msgs (error) in +attribute [grind cases eager] id + +example : True := by + grind [-List] + +/-- +error: `Array` is not marked with the `[grind]` attribute +-/ +#guard_msgs (error) in +example : True := by + grind [-Array]