From af4c693030f0491645bbaa5bbf7d75bb549e105e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 May 2025 16:48:32 -0700 Subject: [PATCH] feat: improve E-matching pattern inference in `grind` (#8196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR improves the E-matching pattern inference procedure in `grind`. Consider the following theorem: ```lean @[grind →] theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] := append_eq_empty_iff.mp h ``` Before this PR, `grind` inferred the following pattern: ```lean @HAppend.hAppend _ _ _ _ #2 #1 ``` Note that this pattern would match any `++` application, even if it had nothing to do with arrays. With this PR, the inferred pattern becomes: ```lean @HAppend.hAppend (Array #3) (Array _) (Array _) _ #2 #1 ``` With the new pattern, the theorem will not be considered by `grind` for goals that do not involve `Array`s. --- src/Lean/Meta/Tactic/Grind.lean | 3 +- src/Lean/Meta/Tactic/Grind/EMatch.lean | 2 +- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 135 ++++++++++++------ src/Lean/Meta/Tactic/Grind/Internalize.lean | 3 +- src/Lean/Meta/Tactic/Grind/Types.lean | 20 +++ tests/lean/grind/hashmap_list.lean | 18 --- tests/lean/grind/mvar.lean | 14 -- tests/lean/run/grind_ematch1.lean | 26 ++-- tests/lean/run/grind_eq_pattern.lean | 4 +- tests/lean/run/grind_hashmap_list.lean | 12 ++ tests/lean/run/grind_mvar.lean | 12 ++ tests/lean/run/grind_pattern1.lean | 14 +- tests/lean/run/grind_pattern2.lean | 2 +- 13 files changed, 164 insertions(+), 101 deletions(-) delete mode 100644 tests/lean/grind/hashmap_list.lean delete mode 100644 tests/lean/grind/mvar.lean create mode 100644 tests/lean/run/grind_hashmap_list.lean create mode 100644 tests/lean/run/grind_mvar.lean diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 1126a6553c..7e33907547 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -42,7 +42,6 @@ builtin_initialize registerTraceClass `grind.eqc builtin_initialize registerTraceClass `grind.internalize builtin_initialize registerTraceClass `grind.ematch builtin_initialize registerTraceClass `grind.ematch.pattern -builtin_initialize registerTraceClass `grind.ematch.pattern.search builtin_initialize registerTraceClass `grind.ematch.instance builtin_initialize registerTraceClass `grind.ematch.instance.assignment builtin_initialize registerTraceClass `grind.eqResolution @@ -71,6 +70,7 @@ builtin_initialize registerTraceClass `grind.debug.final builtin_initialize registerTraceClass `grind.debug.forallPropagator builtin_initialize registerTraceClass `grind.debug.split builtin_initialize registerTraceClass `grind.debug.canon +builtin_initialize registerTraceClass `grind.debug.ematch.activate builtin_initialize registerTraceClass `grind.debug.ematch.pattern builtin_initialize registerTraceClass `grind.debug.beta builtin_initialize registerTraceClass `grind.debug.internalize @@ -81,7 +81,6 @@ builtin_initialize registerTraceClass `grind.debug.mbtc builtin_initialize registerTraceClass `grind.debug.ematch builtin_initialize registerTraceClass `grind.debug.proveEq builtin_initialize registerTraceClass `grind.debug.pushNewFact -builtin_initialize registerTraceClass `grind.debug.ematch.activate builtin_initialize registerTraceClass `grind.debug.appMap builtin_initialize registerTraceClass `grind.debug.ext diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index a36ef0e56f..4a245b9397 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -300,7 +300,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w let report : M Unit := do reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}" unless (← withDefault <| isDefEq mvarIdType vType) do - let some heq ← proveEq? vType mvarIdType + let some heq ← withoutReportingMVarIssues <| proveEq? vType mvarIdType | report return () /- diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 7d6f964903..cab2ee4ee0 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -337,35 +337,54 @@ private def foundBVar (idx : Nat) : M Bool := private def saveBVar (idx : Nat) : M Unit := do modify fun s => { s with bvarsFound := s.bvarsFound.insert idx } -private def getPatternFn? (pattern : Expr) : Option Expr := - if !pattern.isApp && !pattern.isConst then - none - else match pattern.getAppFn with - | f@(.const declName _) => if isForbidden declName then none else some f - | f@(.fvar _) => some f - | _ => none +inductive PatternArgKind where + | /-- Argument is relevant for E-matching. -/ + relevant + | /-- Instance implicit arguments are considered support and handled using `isDefEq`. -/ + instImplicit + | /-- Proofs are ignored during E-matching. Lean is proof irrelevant. -/ + proof + | /-- + Types and type formers are mostly ignored during E-matching, and processed using + `isDefEq`. However, if the argument is of the form `C ..` where `C` is inductive type + we process it as part of the pattern. Suppose we have `as bs : List α`, and a pattern + candidate expression `as ++ bs`, i.e., `@HAppend.hAppend (List α) (List α) (List α) inst as bs`. + If we completely ignore the types, the pattern will just be + ``` + @HAppend.hAppend _ _ _ _ #1 #0 + ``` + This is not ideal because the E-matcher will try it in any goal that contains `++`, + even if it does not even mention lists. + -/ + typeFormer + deriving Repr + +def PatternArgKind.isSupport : PatternArgKind → Bool + | .relevant => false + | _ => true /-- -Returns a bit-mask `mask` s.t. `mask[i]` is true if the corresponding argument is +Returns an array `kinds` s.ts `kinds[i]` is the kind of the corresponding argument. + - a type (that is not a proposition) or type former (which has forward dependencies) or - a proof, or - an instance implicit argument -When `mask[i]`, we say the corresponding argument is a "support" argument. +When `kinds[i].isSupport` is `true`, we say the corresponding argument is a "support" argument. -/ -def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do +def getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind) := do let pinfos := (← getFunInfoNArgs f numArgs).paramInfo forallBoundedTelescope (← inferType f) numArgs fun xs _ => do xs.mapIdxM fun idx x => do if (← isProp x) then - return false + return .relevant else if (← isProof x) then - return true + return .proof else if (← isTypeFormer x) then if h : idx < pinfos.size then /- We originally wanted to ignore types and type formers in `grind` and treat them as supporting elements. - Thus, we would always return `true`. However, we changed our heuristic because of the following example: + Thus, we wanted to always return `.typeFormer`. However, we changed our heuristic because of the following example: ``` example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by grind @@ -374,33 +393,53 @@ def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do a type or type former is considered a supporting element only if it has forward dependencies. Note that this is not the case for `Nonempty`. -/ - return pinfos[idx].hasFwdDeps + if pinfos[idx].hasFwdDeps then return .typeFormer else return .relevant else - return true + return .typeFormer + else if (← x.fvarId!.getDecl).binderInfo matches .instImplicit then + return .instImplicit else - return (← x.fvarId!.getDecl).binderInfo matches .instImplicit + return .relevant -private partial def go (pattern : Expr) : M Expr := do +private def getPatternFn? (pattern : Expr) (inSupport : Bool) (argKind : PatternArgKind) : MetaM (Option Expr) := do + if !pattern.isApp && !pattern.isConst then + return none + else match pattern.getAppFn with + | f@(.const declName _) => + if isForbidden declName then + return none + if inSupport then + if argKind matches .typeFormer | .relevant then + if (← isInductive declName) then + return some f + return none + return some f + | f@(.fvar _) => + if inSupport then return none else return some f + | _ => + return none + +private partial def go (pattern : Expr) (inSupport : Bool) : M Expr := do if let some (e, k) := isOffsetPattern? pattern then - let e ← goArg e (isSupport := false) + let e ← goArg e inSupport .relevant if e == dontCare then return dontCare else return mkOffsetPattern e k - let some f := getPatternFn? pattern + let some f ← getPatternFn? pattern inSupport .relevant | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}" assert! f.isConst || f.isFVar unless f.isConstOf ``Grind.eqBwdPattern do - saveSymbol f.toHeadIndex + saveSymbol f.toHeadIndex let mut args := pattern.getAppArgs.toVector - let supportMask ← getPatternSupportMask f args.size + let patternArgKinds ← getPatternArgKinds f args.size for h : i in [:args.size] do let arg := args[i] - let isSupport := supportMask[i]?.getD false - args := args.set i (← goArg arg isSupport) + let argKind := patternArgKinds[i]?.getD .relevant + args := args.set i (← goArg arg (inSupport || argKind.isSupport) argKind) return mkAppN f args.toArray where - goArg (arg : Expr) (isSupport : Bool) : M Expr := do + goArg (arg : Expr) (inSupport : Bool) (argKind : PatternArgKind) : M Expr := do if !arg.hasLooseBVars then if arg.hasMVar then pure dontCare @@ -408,25 +447,23 @@ where pure <| mkGroundPattern arg else match arg with | .bvar idx => - if isSupport && (← foundBVar idx) then + if inSupport && (← foundBVar idx) then pure dontCare else saveBVar idx pure arg | _ => - if isSupport then - pure dontCare - else if let some _ := getPatternFn? arg then - go arg + if let some _ ← getPatternFn? arg inSupport argKind then + go arg inSupport else pure dontCare def main (patterns : List Expr) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat) := do - let (patterns, s) ← patterns.mapM go |>.run {} + let (patterns, s) ← patterns.mapM (go (inSupport := false)) |>.run {} return (patterns, s.symbols.toList, s.bvarsFound) def normalizePattern (e : Expr) : M Expr := do - go e + go e (inSupport := false) end NormalizePattern @@ -668,11 +705,11 @@ private def isPatternFnCandidate (f : Expr) : CollectorM Bool := do | _ => return false private def addNewPattern (p : Expr) : CollectorM Unit := do - trace[grind.ematch.pattern.search] "found pattern: {ppPattern p}" + trace[grind.debug.ematch.pattern] "found pattern: {ppPattern p}" let bvarsFound := (← getThe NormalizePattern.State).bvarsFound let done := (← checkCoverage (← read).proof (← read).xs.size bvarsFound) matches .ok if done then - trace[grind.ematch.pattern.search] "found full coverage" + trace[grind.debug.ematch.pattern] "found full coverage" modify fun s => { s with patterns := s.patterns.push p, done } /-- Collect the pattern (i.e., de Bruijn) variables in the given pattern. -/ @@ -696,10 +733,11 @@ Returns `true` if pattern `p` contains a child `c` such that 3- `c` is not an offset pattern. 4- `c` is not a bound variable. -/ -private def hasChildWithSameNewBVars (p : Expr) (supportMask : Array Bool) (alreadyFound : Std.HashSet Nat) : CoreM Bool := do +private def hasChildWithSameNewBVars (p : Expr) + (argKinds : Array NormalizePattern.PatternArgKind) (alreadyFound : Std.HashSet Nat) : CoreM Bool := do let s := diff (collectPatternBVars p) alreadyFound - for arg in p.getAppArgs, support in supportMask do - unless support do + for arg in p.getAppArgs, argKind in argKinds do + unless argKind.isSupport do unless arg.isBVar do unless isOffsetPattern? arg |>.isSome do let sArg := diff (collectPatternBVars arg) alreadyFound @@ -711,31 +749,33 @@ 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 supportMask ← NormalizePattern.getPatternSupportMask f e.getAppNumArgs + let argKinds ← NormalizePattern.getPatternArgKinds f e.getAppNumArgs if (← isPatternFnCandidate f) then let saved ← getThe NormalizePattern.State try - trace[grind.ematch.pattern.search] "candidate: {e}" + trace[grind.debug.ematch.pattern] "candidate: {e}" let p := e.abstract (← read).xs unless p.hasLooseBVars do - trace[grind.ematch.pattern.search] "skip, does not contain pattern variables" + trace[grind.debug.ematch.pattern] "skip, does not contain pattern variables" return () let p ← NormalizePattern.normalizePattern p if saved.bvarsFound.size < (← getThe NormalizePattern.State).bvarsFound.size then - unless (← hasChildWithSameNewBVars p supportMask saved.bvarsFound) do + unless (← hasChildWithSameNewBVars p argKinds saved.bvarsFound) do addNewPattern p return () - trace[grind.ematch.pattern.search] "skip, no new variables covered" + trace[grind.debug.ematch.pattern] "skip, no new variables covered" -- restore state and continue search set saved - catch _ => - trace[grind.ematch.pattern.search] "skip, exception during normalization" + catch ex => + trace[grind.debug.ematch.pattern] "skip, exception during normalization{indentD ex.toMessageData}" -- restore state and continue search set saved let args := e.getAppArgs - for arg in args, support in supportMask do - unless support do + for arg in args, argKind in argKinds 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 @@ -746,6 +786,7 @@ private partial def collect (e : Expr) : CollectorM Unit := do private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (List Expr × List HeadIndex)) := do let go : CollectorM (Option (List Expr)) := do for place in searchPlaces do + trace[grind.debug.ematch.pattern] "place: {place}" let place ← preprocessPattern place collect place if (← get).done then @@ -782,8 +823,8 @@ where return some e else let args := e.getAppArgs - for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do - unless flag do + for arg in args, argKind in (← NormalizePattern.getPatternArgKinds f args.size) do + unless argKind.isSupport do if let some r ← visit? arg then return r return none diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index ea56777fc4..99ce01a221 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -313,7 +313,8 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt mkENode e generation activateTheoremPatterns declName generation | .mvar .. => - reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables." + if (← reportMVarInternalization) then + reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables." mkENode' e generation | .mdata .. => reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata" diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 4897eda69a..e584867bfb 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -68,6 +68,13 @@ structure Context where when performing lookahead. -/ cheapCases : Bool := false + /- + If `reportMVarIssue` is `true`, `grind` reports an issue when internalizing metavariables. + The default value is `true`. We set it to `false` when invoking `proveEq` from the `instantiateTheorem` + at in the E-matching module. There, the terms may contain metavariables, and we don't want to bother + user with "false-alarms". If the instantiation fails, we produce a more informative issue anyways. + -/ + reportMVarIssue : Bool := true /-- Key for the congruence theorem cache. -/ structure CongrTheoremCacheKey where @@ -147,6 +154,16 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM +@[inline] def mapGrindM [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α} (x : m α) : m α := + controlAt GrindM fun runInBase => f <| runInBase x + +/-- +`withoutReportingMVarIssues x` executes `x` without reporting metavariables found during internalization. +See comment at `Grind.Context.reportMVarIssue` for additional details. +-/ +def withoutReportingMVarIssues [MonadControlT GrindM m] [Monad m] : m α → m α := + mapGrindM <| withTheReader Grind.Context fun ctx => { ctx with reportMVarIssue := false } + /-- Returns the user-defined configuration options -/ def getConfig : GrindM Grind.Config := return (← readThe Context).config @@ -177,6 +194,9 @@ def getMainDeclName : GrindM Name := def cheapCasesOnly : GrindM Bool := return (← readThe Context).cheapCases +def reportMVarInternalization : GrindM Bool := + return (← readThe Context).reportMVarIssue + def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do if (← getConfig).trace then modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } } diff --git a/tests/lean/grind/hashmap_list.lean b/tests/lean/grind/hashmap_list.lean deleted file mode 100644 index a6644f2a97..0000000000 --- a/tests/lean/grind/hashmap_list.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Std.Data.HashMap - -reset_grind_attrs% - -open Std - -attribute [grind →] List.length_pos_of_mem -attribute [grind] HashMap.size_insert - --- Fails with issue: --- [issue] type error constructing proof for List.length_pos_of_mem --- when assigning metavariable ?l with --- m.insert 1 2 --- has type --- HashMap Nat Nat : Type --- but is expected to have type --- List Nat : Type -example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≤ m.size := by grind diff --git a/tests/lean/grind/mvar.lean b/tests/lean/grind/mvar.lean deleted file mode 100644 index fada34399a..0000000000 --- a/tests/lean/grind/mvar.lean +++ /dev/null @@ -1,14 +0,0 @@ -open List - --- Failing with: --- [issue] unexpected metavariable during internalization --- ?α --- `grind` is not supposed to be used in goals containing metavariables. - -- [issue] type error constructing proof for Array.eq_empty_of_append_eq_empty - -- when assigning metavariable ?xs with - -- l₁ - -- has type - -- List α : Type u_1 - -- but is expected to have type - -- Array ?α : Type ?u.430 -theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by grind (gen := 6) diff --git a/tests/lean/run/grind_ematch1.lean b/tests/lean/run/grind_ematch1.lean index dae4eb5dcd..907015c794 100644 --- a/tests/lean/run/grind_ematch1.lean +++ b/tests/lean/run/grind_ematch1.lean @@ -83,15 +83,25 @@ error: `@[grind →] theorem using_grind_fwd.StransBad` failed to find patterns @[grind→] theorem StransBad (a b c d : Nat) : S a b ∨ R a b → S b c → S a c ∧ S b d := sorry -set_option trace.grind.ematch.pattern.search true in +set_option trace.grind.debug.ematch.pattern true in /-- -info: [grind.ematch.pattern.search] candidate: S a b -[grind.ematch.pattern.search] found pattern: S #4 #3 -[grind.ematch.pattern.search] candidate: R a b -[grind.ematch.pattern.search] skip, no new variables covered -[grind.ematch.pattern.search] candidate: S b c -[grind.ematch.pattern.search] found pattern: S #3 #2 -[grind.ematch.pattern.search] found full coverage +info: [grind.debug.ematch.pattern] place: S a b ∨ R a b +[grind.debug.ematch.pattern] collect: S a b ∨ R a b +[grind.debug.ematch.pattern] arg: S a b, support: false +[grind.debug.ematch.pattern] collect: S a b +[grind.debug.ematch.pattern] candidate: S a b +[grind.debug.ematch.pattern] found pattern: S #4 #3 +[grind.debug.ematch.pattern] arg: R a b, support: false +[grind.debug.ematch.pattern] collect: R a b +[grind.debug.ematch.pattern] candidate: R a b +[grind.debug.ematch.pattern] skip, no new variables covered +[grind.debug.ematch.pattern] arg: a, support: false +[grind.debug.ematch.pattern] arg: b, support: false +[grind.debug.ematch.pattern] place: S b c +[grind.debug.ematch.pattern] collect: S b c +[grind.debug.ematch.pattern] candidate: S b c +[grind.debug.ematch.pattern] found pattern: S #3 #2 +[grind.debug.ematch.pattern] found full coverage [grind.ematch.pattern] Strans: [S #4 #3, S #3 #2] -/ #guard_msgs (info) in diff --git a/tests/lean/run/grind_eq_pattern.lean b/tests/lean/run/grind_eq_pattern.lean index 5985f2d855..9921bd99d9 100644 --- a/tests/lean/run/grind_eq_pattern.lean +++ b/tests/lean/run/grind_eq_pattern.lean @@ -1,14 +1,14 @@ reset_grind_attrs% /-- -info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend _ _ _ _ #2 #0] +info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0] -/ #guard_msgs (info) in set_option trace.grind.ematch.pattern true in attribute [grind] List.append_ne_nil_of_left_ne_nil /-- -info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend _ _ _ _ #1 #2] +info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2] -/ #guard_msgs (info) in set_option trace.grind.ematch.pattern true in diff --git a/tests/lean/run/grind_hashmap_list.lean b/tests/lean/run/grind_hashmap_list.lean new file mode 100644 index 0000000000..319619fbd0 --- /dev/null +++ b/tests/lean/run/grind_hashmap_list.lean @@ -0,0 +1,12 @@ +import Std.Data.HashMap +set_option grind.warning false +reset_grind_attrs% + +open Std + +attribute [grind →] List.length_pos_of_mem +attribute [grind] HashMap.size_insert + +set_option trace.grind.issues true in +example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≥ m.size := by + grind diff --git a/tests/lean/run/grind_mvar.lean b/tests/lean/run/grind_mvar.lean new file mode 100644 index 0000000000..d8fd669659 --- /dev/null +++ b/tests/lean/run/grind_mvar.lean @@ -0,0 +1,12 @@ +open List +reset_grind_attrs% +set_option grind.warning false + +attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero +attribute [grind] Vector.getElem?_append getElem?_dropLast + +#guard_msgs (info) in -- should not report any issues +set_option trace.grind.issues true +theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by + fail_if_success grind (gen := 6) + grind -ext only [List.dropLast_append_cons, List.dropLast_singleton, List.append_nil] diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean index ad05c66f1b..3f51edf302 100644 --- a/tests/lean/run/grind_pattern1.lean +++ b/tests/lean/run/grind_pattern1.lean @@ -1,20 +1,20 @@ set_option trace.grind.ematch.pattern true /-- -info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem _ `[Nat] #4 _ _ (@Array.push _ #3 #2) #1 _] +info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _] -/ #guard_msgs in grind_pattern Array.getElem_push_lt => (xs.push x)[i] /-- -info: [grind.ematch.pattern] List.getElem_attach: [@getElem _ `[Nat] _ _ _ (@List.attach #3 #2) #1 _] +info: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _] -/ #guard_msgs in grind_pattern List.getElem_attach => xs.attach[i] /-- -info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 _ _ (@HAppend.hAppend _ _ _ _ #1 (@List.cons _ #0 (@List.nil _))) #0] +info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0] -/ #guard_msgs in grind_pattern List.mem_concat_self => a ∈ xs ++ [a] @@ -54,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl -/-- info: [grind.ematch.pattern] fEq: [@f _ _ _ _ #0] -/ +/-- info: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/ #guard_msgs in grind_pattern fEq => f a theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl -/-- info: [grind.ematch.pattern] fEq2: [@f _ _ _ _ #1] -/ +/-- info: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/ #guard_msgs in grind_pattern fEq2 => f a @@ -71,12 +71,12 @@ theorem gEq [Boo α β] (a : List α) : (g (β := Array β) a).1 = a := rfl /-- error: invalid pattern(s) for `gEq` - [@g _ _ _ #0] + [@g (List #3) _ _ #0] the following theorem parameters cannot be instantiated: β : Type inst✝ : Boo α β --- -info: [grind.ematch.pattern] gEq: [@g _ _ _ #0] +info: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0] -/ #guard_msgs in grind_pattern gEq => g a diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean index 6f126ba4b4..8ff7817c7a 100644 --- a/tests/lean/run/grind_pattern2.lean +++ b/tests/lean/run/grind_pattern2.lean @@ -62,7 +62,7 @@ theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[ /-- -info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem _ `[Nat] _ _ _ #2 #5 _) (@getElem _ `[Nat] _ _ _ #2 #4 _)] +info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)] -/ #guard_msgs in grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)