From efb398b040005ff19afee3fa8a1052566897fe43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Sep 2025 19:44:11 -0700 Subject: [PATCH] feat: new `grind` pattern inference heuristic and code action (#10422) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements the new E-matching pattern inference heuristic for `grind`. It is not enabled yet. You can activate the new behavior using `set_option backward.grind.inferPattern false`. Here is a summary of the new behavior. * `[grind =]`, `[grind =_]`, `[grind _=_]`, `[grind <-=]`: no changes; we keep the current behavior. * `[grind ->]`, `[grind <-]`, `[grind =>]`, `[grind <=]`: we stop using the *minimal indexable subexpression* and instead use the first indexable one. * `[grind! ]`: behaves like `[grind ]` but uses the minimal indexable subexpression restriction. We generate an error if the user writes `[grind! =]`, `[grind! =_]`, `[grind! _=_]`, or `[grind! <-=]`, since there is no pattern search in these cases. * `[grind]`: it tries `=`, `=_`, `<-`, `->`, `<=`, `=>` with and without the minimal indexable subexpression restriction. For the ones that work, we generate a code action to encourage users to select the one they prefer. * `[grind!]`: it tries `<-`, `->`, `<=`, `=>` using the minimal indexable subexpression restriction. For the ones that work, we generate a code action to encourage users to select the one they prefer. * `[grind? ]`: where `` is one of the modifiers above, it behaves like `[grind ]` but also displays the pattern. Example: ```lean /-- info: Try these: • [grind =] for pattern: [f (g #0)] • [grind =_] for pattern: [r #0 #0] • [grind! ←] for pattern: [g #0] -/ #guard_msgs in @[grind] axiom fg₇ : f (g x) = r x x ``` --- src/Init/Grind/Attr.lean | 14 +- src/Lean/Meta/Tactic/Grind/Attr.lean | 36 +-- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 226 ++++++++++++------ stage0/src/stdlib_flags.h | 1 + tests/lean/run/grind_pat_sel.lean | 123 ++++++++++ .../run/grind_pattern_inference_issue.lean | 4 +- 6 files changed, 315 insertions(+), 89 deletions(-) create mode 100644 tests/lean/run/grind_pat_sel.lean diff --git a/src/Init/Grind/Attr.lean b/src/Init/Grind/Attr.lean index 0d9d327ecf..194a348a6d 100644 --- a/src/Init/Grind/Attr.lean +++ b/src/Init/Grind/Attr.lean @@ -98,28 +98,34 @@ syntax grindEqBwd := patternIgnore(atomic("←" "=") <|> atomic("<-" "=")) The `←` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem. In other words, `grind` will use the theorem for backwards reasoning. This may fail if not all of the arguments to the theorem appear in the conclusion. +Each time it encounters a subexpression which covers an argument which was not +previously covered, it adds that subexpression as a pattern, until all arguments have been covered. +If `grind!` is used, then only minimal indexable subexpressions are considered. -/ syntax grindBwd := patternIgnore("←" <|> "<-") (grindGen)? /-- The `→` modifier instructs `grind` to select a multi-pattern from the hypotheses of the theorem. In other words, `grind` will use the theorem for forwards reasoning. To generate a pattern, it traverses the hypotheses of the theorem from left to right. -Each time it encounters a minimal indexable subexpression which covers an argument which was not +Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. +If `grind!` is used, then only minimal indexable subexpressions are considered. -/ syntax grindFwd := patternIgnore("→" <|> "->") /-- The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then all the hypotheses from right to left. -Each time it encounters a minimal indexable subexpression which covers an argument which was not +Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. +If `grind!` is used, then only minimal indexable subexpressions are considered. -/ syntax grindRL := patternIgnore("⇐" <|> "<=") /-- The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from left to right, followed by the conclusion. -Each time it encounters a minimal indexable subexpression which covers an argument which was not +Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. +If `grind!` is used, then only minimal indexable subexpressions are considered. -/ syntax grindLR := patternIgnore("⇒" <|> "=>") /-- @@ -195,6 +201,8 @@ syntax grindMod := <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym syntax (name := grind) "grind" (ppSpace grindMod)? : attr +syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr +syntax (name := grind!?) "grind!?" (ppSpace grindMod)? : attr end Attr end Lean.Parser diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean index a73b842de5..d535d43138 100644 --- a/src/Lean/Meta/Tactic/Grind/Attr.lean +++ b/src/Lean/Meta/Tactic/Grind/Attr.lean @@ -59,18 +59,24 @@ def throwInvalidUsrModifier : CoreM α := throwError "the modifier `usr` is only relevant in parameters for `grind only`" /-- -Auxiliary function for registering `grind` and `grind?` attributes. -The `grind?` is an alias for `grind` which displays patterns using `logInfo`. +Auxiliary function for registering `grind`, `grind!`, `grind?`, and `grind!?` attributes. +`grind!` is like `grind` but selects minimal indexable subterms. +The `grind?` and `grind!?` are aliases for `grind` and `grind!` which displays patterns using `logInfo`. It is just a convenience for users. -/ -private def registerGrindAttr (showInfo : Bool) : IO Unit := +private def registerGrindAttr (minIndexable : Bool) (showInfo : Bool) : IO Unit := registerBuiltinAttribute { - name := if showInfo then `grind? else `grind + name := match minIndexable, showInfo with + | false, false => `grind + | false, true => `grind? + | true, false => `grind! + | true, true => `grind!? descr := - let header := if showInfo then - "The `[grind?]` attribute is identical to the `[grind]` attribute, but displays inferred pattern information." - else - "The `[grind]` attribute is used to annotate declarations." + let header := match minIndexable, showInfo with + | false, false => "The `[grind]` attribute is used to annotate declarations." + | false, true => "The `[grind?]` attribute is identical to the `[grind]` attribute, but displays inferred pattern information." + | true, false => "The `[grind!]` attribute is used to annotate declarations, but selecting minimal indexable subterms." + | true, true => "The `[grind!?]` attribute is identical to the `[grind!]` attribute, but displays inferred pattern information." header ++ "\ \ When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\ @@ -91,12 +97,12 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit := add := fun declName stx attrKind => MetaM.run' do match (← getAttrKindFromOpt stx) with | .ematch .user => throwInvalidUsrModifier - | .ematch k => addEMatchAttr declName attrKind k (← getGlobalSymbolPriorities) (showInfo := showInfo) + | .ematch k => addEMatchAttr declName attrKind k (← getGlobalSymbolPriorities) (minIndexable := minIndexable) (showInfo := showInfo) | .cases eager => addCasesAttr declName eager attrKind | .intro => if let some info ← isCasesAttrPredicateCandidate? declName false then for ctor in info.ctors do - addEMatchAttr ctor attrKind (.default false) (← getGlobalSymbolPriorities) (showInfo := showInfo) + addEMatchAttr ctor attrKind (.default false) (← getGlobalSymbolPriorities) (minIndexable := minIndexable) (showInfo := showInfo) else throwError "invalid `[grind intro]`, `{.ofConstName declName}` is not an inductive predicate" | .ext => addExtAttr declName attrKind @@ -107,9 +113,9 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit := -- If it is an inductive predicate, -- we also add the constructors (intro rules) as E-matching rules for ctor in info.ctors do - addEMatchAttr ctor attrKind (.default false) (← getGlobalSymbolPriorities) (showInfo := showInfo) + addEMatchAttr ctor attrKind (.default false) (← getGlobalSymbolPriorities) (minIndexable := minIndexable) (showInfo := showInfo) else - addEMatchAttr declName attrKind (.default false) (← getGlobalSymbolPriorities) (showInfo := showInfo) + addEMatchAttrAndSuggest stx declName attrKind (← getGlobalSymbolPriorities) (minIndexable := minIndexable) (showInfo := showInfo) | .symbol prio => addSymbolPriorityAttr declName attrKind prio erase := fun declName => MetaM.run' do if showInfo then @@ -123,7 +129,9 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit := } builtin_initialize - registerGrindAttr true - registerGrindAttr false + registerGrindAttr (minIndexable := false) (showInfo := true) + registerGrindAttr (minIndexable := false) (showInfo := false) + registerGrindAttr (minIndexable := true) (showInfo := true) + registerGrindAttr (minIndexable := true) (showInfo := false) end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index eb20f55fb2..9d0d59244f 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -18,6 +18,7 @@ public import Lean.Meta.Tactic.Grind.Util import Lean.Message import Lean.Meta.Tactic.FVarSubst import Lean.Meta.Match.Basic +import Lean.Meta.Tactic.TryThis public section @@ -348,22 +349,25 @@ def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool | .default _ => true | _ => false -def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String - | .eqLhs true => "[grind = gen]" - | .eqLhs false => "[grind =]" - | .eqRhs true => "[grind =_ gen]" - | .eqRhs false => "[grind =_]" - | .eqBoth false => "[grind _=_]" - | .eqBoth true => "[grind _=_ gen]" - | .eqBwd => "[grind ←=]" - | .fwd => "[grind →]" - | .bwd false => "[grind ←]" - | .bwd true => "[grind ← gen]" - | .leftRight => "[grind =>]" - | .rightLeft => "[grind <=]" - | .default false => "[grind]" - | .default true => "[grind gen]" - | .user => "[grind]" +def EMatchTheoremKind.toAttributeCore : EMatchTheoremKind → String + | .eqLhs true => " = gen" + | .eqLhs false => " =" + | .eqRhs true => " =_ gen" + | .eqRhs false => " =_" + | .eqBoth false => " _=_" + | .eqBoth true => " _=_ gen" + | .eqBwd => " ←=" + | .fwd => " →" + | .bwd false => " ←" + | .bwd true => " ← gen" + | .leftRight => " =>" + | .rightLeft => " <=" + | .default false => "" + | .default true => " gen" + | .user => "" + +def EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) : String := + s!"[grind{toAttributeCore k}]" private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String | .eqLhs _ => "failed to find pattern in the left-hand side of the theorem's conclusion" @@ -1085,8 +1089,13 @@ Normalizes `e` if it qualifies as a candidate pattern, and returns `some p` where `p` is the normalized pattern. `argKinds == NormalizePattern.getPatternArgKinds e.getAppFn e.getAppNumArgs` + +If `minIndexable == true`, then enforces the minimal indexable subexpression condition. +That is, an indexable subexpression is minimal if there is no smaller indexable subexpression +whose head constant has at least as high priority. -/ -private def normalizePattern? (e : Expr) (argKinds : Array NormalizePattern.PatternArgKind) : CollectorM (Option Expr) := do +private def normalizePattern? (e : Expr) (argKinds : Array NormalizePattern.PatternArgKind) + (minIndexable : Bool) : CollectorM (Option Expr) := do let p := e.abstract (← read).xs unless p.hasLooseBVars do trace[grind.debug.ematch.pattern] "skip, does not contain pattern variables" @@ -1101,60 +1110,64 @@ private def normalizePattern? (e : Expr) (argKinds : Array NormalizePattern.Patt return sizeOfDiff (← get).bvarsFound stateBefore.bvarsFound try let p ← NormalizePattern.normalizePattern p - let stateAfter ← getThe NormalizePattern.State let numNewBVars ← getNumNewBVars if numNewBVars == 0 then trace[grind.debug.ematch.pattern] "skip, no new variables covered" return (← failed) - /- - Checks whether one of `e`s children subsumes it. We say a child `c` subsumes `e` - 1- `e` and `c` have the same new pattern variables. We say a pattern variable is new if it is not in `stateOld.bvarsFound`. - 2- `c` is not a support argument. See `NormalizePattern.getPatternSupportMask` for definition. - 3- `c` is not an offset pattern. - 4- `c` is not a bound variable. - 5- `c` is also a candidate. - -/ - for arg in e.getAppArgs, argKind in argKinds do - unless argKind.isSupport do - unless arg.isFVar do - unless isOffsetPattern? arg |>.isSome do - if (← isPatternFnCandidate arg.getAppFn) then - let pArg := arg.abstract (← read).xs - set stateBefore - discard <| NormalizePattern.normalizePattern pArg - let numArgNewBVars ← getNumNewBVars - if numArgNewBVars == numNewBVars then - trace[grind.debug.ematch.pattern] "skip, subsumed by argument" - return (← failed) - set stateAfter + if minIndexable then + let stateAfter ← getThe NormalizePattern.State + /- + Checks whether one of `e`s children subsumes it. We say a child `c` subsumes `e` + 1- `e` and `c` have the same new pattern variables. We say a pattern variable is new if it is not in `stateOld.bvarsFound`. + 2- `c` is not a support argument. See `NormalizePattern.getPatternSupportMask` for definition. + 3- `c` is not an offset pattern. + 4- `c` is not a bound variable. + 5- `c` is also a candidate. + -/ + for arg in e.getAppArgs, argKind in argKinds do + unless argKind.isSupport do + unless arg.isFVar do + unless isOffsetPattern? arg |>.isSome do + if (← isPatternFnCandidate arg.getAppFn) then + let pArg := arg.abstract (← read).xs + set stateBefore + discard <| NormalizePattern.normalizePattern pArg + let numArgNewBVars ← getNumNewBVars + if numArgNewBVars == numNewBVars then + trace[grind.debug.ematch.pattern] "skip, subsumed by argument" + return (← failed) + set stateAfter return some p catch ex => trace[grind.debug.ematch.pattern] "skip, exception during normalization{indentD ex.toMessageData}" failed -private partial def collect (e : Expr) : CollectorM Unit := do - if (← get).done then return () - match e with - | .app .. => - trace[grind.debug.ematch.pattern] "collect: {e}" - let f := e.getAppFn - let argKinds ← NormalizePattern.getPatternArgKinds f e.getAppNumArgs - if (← isPatternFnCandidate f) then - trace[grind.debug.ematch.pattern] "candidate: {e}" - if let some p ← normalizePattern? e argKinds then - addNewPattern p - return () - let args := e.getAppArgs - for arg in args, argKind in argKinds do - unless isOffsetPattern? arg |>.isSome do - trace[grind.debug.ematch.pattern] "arg: {arg}, support: {argKind.isSupport}" - unless argKind.isSupport do - collect arg - | .forallE _ d b _ => - if (← pure e.isArrow <&&> isProp d <&&> isProp b) then - collect d - collect b - | _ => return () +private partial def collect (e : Expr) (minIndexable : Bool) : CollectorM Unit := do + go e +where + go (e : Expr) : CollectorM Unit := do + if (← get).done then return () + match e with + | .app .. => + trace[grind.debug.ematch.pattern] "collect: {e}" + let f := e.getAppFn + let argKinds ← NormalizePattern.getPatternArgKinds f e.getAppNumArgs + if (← isPatternFnCandidate f) then + trace[grind.debug.ematch.pattern] "candidate: {e}" + if let some p ← normalizePattern? e argKinds minIndexable then + addNewPattern p + return () + let args := e.getAppArgs + for arg in args, argKind in argKinds do + unless isOffsetPattern? arg |>.isSome do + trace[grind.debug.ematch.pattern] "arg: {arg}, support: {argKind.isSupport}" + unless argKind.isSupport do + go arg + | .forallE _ d b _ => + if (← pure e.isArrow <&&> isProp d <&&> isProp b) then + go d + go b + | _ => return () register_builtin_option backward.grind.inferPattern : Bool := { defValue := true @@ -1169,7 +1182,7 @@ register_builtin_option backward.grind.checkInferPatternDiscrepancy : Bool := { } private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) (symPrios : SymbolPriorities) (minPrio : Nat) - : MetaM (Option (List Expr × List HeadIndex)) := do + (minIndexable : Bool) : MetaM (Option (List Expr × List HeadIndex)) := do let go (useOld : Bool): CollectorM (Option (List Expr)) := do for place in searchPlaces do trace[grind.debug.ematch.pattern] "place: {place}" @@ -1177,7 +1190,7 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar if useOld then OldCollector.collect place else - collect place + collect place minIndexable if (← get).done then return some ((← get).patterns.toList) return none @@ -1279,6 +1292,7 @@ private partial def collectSingletons (e : Expr) : StateT (Array (Expr × List H unless p.hasLooseBVars do trace[grind.debug.ematch.pattern] "skip, does not contain pattern variables" return () + -- **TODO**: `minIndexable` support let p ← NormalizePattern.normalizePattern p addNewPattern p if (← getThe Collector.State).done then @@ -1333,7 +1347,7 @@ since the theorem is already in the `grind` state and there is nothing to be ins -/ def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) - (groundPatterns := true) (showInfo := false) : MetaM (Option EMatchTheorem) := do + (groundPatterns := true) (showInfo := false) (minIndexable := false) : MetaM (Option EMatchTheorem) := do match kind with | .eqLhs gen => return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (gen := gen) (showInfo := showInfo)) @@ -1378,7 +1392,7 @@ where collect (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (List Expr × List HeadIndex)) := do let prios := collectUsedPriorities symPrios searchPlaces for minPrio in prios do - if let some r ← collectPatterns? proof xs searchPlaces symPrios minPrio then + if let some r ← collectPatterns? proof xs searchPlaces symPrios minPrio (minIndexable := minIndexable) then return some r else if groundPatterns then if let some (pattern, symbols) ← collectGroundPattern? proof xs searchPlaces symPrios minPrio then @@ -1395,8 +1409,9 @@ where levelParams, origin, kind } -def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo := false) : MetaM EMatchTheorem := do - let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind prios (showInfo := showInfo) +def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) + (showInfo := false) (minIndexable := false) : MetaM EMatchTheorem := do + let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind prios (showInfo := showInfo) (minIndexable := minIndexable) | throwError "`@{thmKind.toAttribute} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command" return thm @@ -1431,23 +1446,94 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat throwErr return s.erase <| .decl declName -def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo := false) : MetaM Unit := do +private def ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do + if minIndexable then + throwError "redundant modifier `!` in `grind` attribute" + +def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) + (showInfo := false) (minIndexable := false) : MetaM Unit := do match thmKind with | .eqLhs _ => + ensureNoMinIndexable minIndexable addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo) | .eqRhs _ => + ensureNoMinIndexable minIndexable addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo) | .eqBoth _ => + ensureNoMinIndexable minIndexable addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo) addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo) | _ => let info ← getConstInfo declName if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then + ensureNoMinIndexable minIndexable addGrindEqAttr declName attrKind thmKind (showInfo := showInfo) else - let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := showInfo) + let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := showInfo) (minIndexable := minIndexable) ematchTheoremsExt.add thm attrKind +private structure SelectM.State where + -- **Note**: hack, an attribute is not a tactic. + suggestions : Array Tactic.TryThis.Suggestion := #[] + thms : Array EMatchTheorem := #[] + +private abbrev SelectM := StateT SelectM.State MetaM + +private def save (thm : EMatchTheorem) (minIndexable : Bool) : SelectM Unit := do + -- We only save `thm` if the pattern is different from the ones that were already found. + if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then + let baseAttr := if minIndexable then "grind!" else "grind" + let msg := s!"] for pattern: {← thm.patterns.mapM fun p => (ppPattern p).toString}" + modify fun s => { s with + thms := s.thms.push thm + suggestions := s.suggestions.push { + suggestion := .string s!"{baseAttr}{thm.kind.toAttributeCore}" + -- **Note**: small hack to include brackets in the suggestion + preInfo? := some "[" + -- **Note**: appears only on the info view. + postInfo? := some msg + } + } + +/-- +Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked. + +Remark: if `backward.grind.inferPattern` is `true`, then `.default false` is used. +The parameter `showInfo` is only taken into account when `backward.grind.inferPattern` is `true`. +-/ +def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities) (minIndexable : Bool) (showInfo : Bool) : MetaM Unit := do + if backward.grind.inferPattern.get (← getOptions) then + addEMatchAttr declName attrKind (.default false) prios (minIndexable := minIndexable) (showInfo := showInfo) + else + let tryModifier (thmKind : EMatchTheoremKind) (minIndexable : Bool) : SelectM Unit := do + try + let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := minIndexable) + save thm minIndexable + catch _ => + return () + let searchCore (minIndexable : Bool) : SelectM Unit := do + tryModifier (.bwd false) minIndexable + tryModifier .fwd minIndexable + tryModifier .rightLeft minIndexable + tryModifier .leftRight minIndexable + let search : SelectM Unit := do + if minIndexable then + searchCore true + else + tryModifier (.eqLhs false) false + tryModifier (.eqRhs false) false + searchCore false + searchCore true + let (_, s) ← search.run {} + if h₁ : 0 < s.thms.size then + if s.suggestions.size == 1 then + Tactic.TryThis.addSuggestion ref s.suggestions[0]! + else + Tactic.TryThis.addSuggestions ref s.suggestions + ematchTheoremsExt.add s.thms[0] attrKind + else + throwError "invalid `grind` theorem, failed to find an usable pattern using different modifiers" + def eraseEMatchAttr (declName : Name) : MetaM Unit := do /- Remark: consider the following example diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ad491b0de1 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean { diff --git a/tests/lean/run/grind_pat_sel.lean b/tests/lean/run/grind_pat_sel.lean new file mode 100644 index 0000000000..69ceae5288 --- /dev/null +++ b/tests/lean/run/grind_pat_sel.lean @@ -0,0 +1,123 @@ +-- Enable new pattern selection algorithm +set_option backward.grind.inferPattern false +set_option warn.sorry false + +opaque f : Nat → Nat +opaque g : Nat → Nat + +/-- info: fg₁: [g #0] -/ +#guard_msgs in +@[grind!? ←] axiom fg₁ : f (g x) = x + +set_option trace.Meta.debug true + +/-- info: fg₂: [f (g #0)] -/ +#guard_msgs in +@[grind? ←] axiom fg₂ : f (g x) = x + +/-- error: redundant modifier `!` in `grind` attribute -/ +#guard_msgs in +@[grind! =] axiom fg₃ : f (g x) = x + +/-- error: redundant modifier `!` in `grind` attribute -/ +#guard_msgs in +@[grind! =_] axiom fg₄ : f (g x) = x + +/-- +error: invalid pattern, (non-forbidden) application expected + #0 +-/ +#guard_msgs (error) in +@[grind =_] theorem fg₅ : f (g x) = x := sorry + +opaque p : Nat → Prop + +/-- info: pf₁: [f #3, f #2] -/ +#guard_msgs in +@[grind!? →] axiom pf₁ : p (f x) → p (f y) → f x = f y + +/-- info: pf₂: [p (f #3), p (f #2)] -/ +#guard_msgs in +@[grind? →] axiom pf₂ : p (f x) → p (f y) → f x = f y + +/-- info: pf₃: [p (f #3), f (f #2)] -/ +#guard_msgs in +@[grind? →] axiom pf₃ : p (f x) → f (f y) = y → f x = f y + +opaque r : Nat → Nat → Nat + +/-- info: pr₁: [p (f #2), r #2 (f #1)] -/ +#guard_msgs in +@[grind? =>] axiom pr₁ : p (f x) → r x (f y) = y + +/-- info: pr₂: [f #2, f #1] -/ +#guard_msgs in +@[grind!? =>] axiom pr₂ : p (f x) → r x (f y) = y + +/-- info: pr₃: [r #2 (f #1)] -/ +#guard_msgs in +@[grind!? <=] axiom pr₃ : p (f x) → r x (f y) = y + +/-- info: pr₄: [r #1 (f #1), p (f #2)] -/ +#guard_msgs in +@[grind? <=] axiom pr₄ : p (f x) → r y (f y) = y + +/-- +info: Try these: + • [grind! ←] for pattern: [r #2 (f #1)] + • [grind! =>] for pattern: [f #2, f #1] +-/ +#guard_msgs in +@[grind!] theorem pr₅ : p (f x) → r x (f y) = y := sorry + +/-- +info: Try these: + • [grind! <=] for pattern: [f #1, f #2] + • [grind! =>] for pattern: [f #2, f #1] +-/ +#guard_msgs in +@[grind!] theorem pr₆ : p (f x) → r y (f y) = y := sorry + +/-- +info: Try these: + • [grind <=] for pattern: [r #1 (f #1), p (f #2)] + • [grind =>] for pattern: [p (f #2), r #1 (f #1)] + • [grind! <=] for pattern: [f #1, f #2] + • [grind! =>] for pattern: [f #2, f #1] +-/ +#guard_msgs in +@[grind] theorem pr₇ : p (f x) → r y (f y) = y := sorry + +/-- +info: Try these: + • [grind =] for pattern: [r #2 (f #1)] + • [grind =>] for pattern: [p (f #2), r #2 (f #1)] + • [grind! =>] for pattern: [f #2, f #1] +-/ +#guard_msgs in +@[grind] theorem pr₈ : p (f x) → r x (f y) = y := sorry + + +/-- +info: Try these: + • [grind =] for pattern: [f (g #0)] + • [grind! ←] for pattern: [g #0] +-/ +#guard_msgs in +@[grind] axiom fg₆ : f (g x) = x + +/-- +info: Try these: + • [grind =] for pattern: [f (g #0)] + • [grind =_] for pattern: [r #0 #0] + • [grind! ←] for pattern: [g #0] +-/ +#guard_msgs in +@[grind] axiom fg₇ : f (g x) = r x x + +/-- +info: Try this: + [grind =] for pattern: [f #0] +-/ +#guard_msgs in +@[grind] axiom fg₈ : f x = x diff --git a/tests/lean/run/grind_pattern_inference_issue.lean b/tests/lean/run/grind_pattern_inference_issue.lean index 4011c7e227..84536bd8be 100644 --- a/tests/lean/run/grind_pattern_inference_issue.lean +++ b/tests/lean/run/grind_pattern_inference_issue.lean @@ -18,7 +18,7 @@ def Vector.toList (xs : Vector α n) : List α := /-- info: length_toList: [@toList #2 #1 #0] -/ #guard_msgs (info) in -@[grind?] theorem Vector.length_toList (xs : Vector α n) : xs.toList.length = n := by sorry +@[grind!? ←] theorem Vector.length_toList (xs : Vector α n) : xs.toList.length = n := by sorry def wrapper (f : Nat → Nat → List α → List α) (h : ∀ n m xs, xs.length = n → (f n m xs).length = m) : (n m : Nat) → Vector α n → Vector α m := @@ -32,4 +32,4 @@ new: -/ #guard_msgs in set_option backward.grind.checkInferPatternDiscrepancy true in -@[grind] theorem Vector.length_toList' (xs : Vector α n) : xs.toList.length = n := by sorry +@[grind! ←] theorem Vector.length_toList' (xs : Vector α n) : xs.toList.length = n := by sorry