From 2b9d708f909f5ce2e5a99861312da4751d8e81f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2025 18:01:45 -0800 Subject: [PATCH 1/3] fix: bugs in `grind` --- src/Lean/Elab/Tactic/Grind.lean | 15 ++++++---- src/Lean/Meta/Tactic/Grind.lean | 2 ++ src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 30 ++++++++++++------- 3 files changed, 32 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 34425ac40e01..98f70534d397 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -50,12 +50,17 @@ def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic. if (← isInductivePredicate declName) then throwErrorAt p "NIY" else if (← getConstInfo declName).isTheorem then - params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) } - else if let some eqns ← getEqnsFor? declName then - for eqn in eqns do - params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl eqn kind) } + 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) } + else if let some thms ← Grind.mkEMatchEqTheoremsForDef? declName then + if kind != .eqLhs && kind != .default then + throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='" + params := { params with extra := params.extra ++ thms.toPArray' } else - throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type" + throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type" | _ => throwError "unexpected `grind` parameter{indentD p}" return params diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index b3212a168101..0cd55eef6eeb 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -67,4 +67,6 @@ builtin_initialize registerTraceClass `grind.debug.split builtin_initialize registerTraceClass `grind.debug.canon builtin_initialize registerTraceClass `grind.debug.offset builtin_initialize registerTraceClass `grind.debug.offset.proof +builtin_initialize registerTraceClass `grind.debug.ematch.pattern + end Lean diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index dff322df1397..1b3b22cd9239 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -516,7 +516,9 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : | HEq _ lhs _ rhs => pure (lhs, rhs) | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}" let pat := if useLhs then lhs else rhs + trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: origin: {← origin.pp}, pat: {pat}, useLhs: {useLhs}" let pat ← preprocessPattern pat normalizePattern + trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat}" let pats := splitWhileForbidden (pat.abstract xs) return (xs.size, pats) mkEMatchTheoremCore origin levelParams numParams proof patterns @@ -651,9 +653,9 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do if kind == .eqLhs then - return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true)) + return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true)) else if kind == .eqRhs then - return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := false)) + return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false)) let type ← inferType proof forallTelescopeReducing type fun xs type => do let searchPlaces ← match kind with @@ -694,22 +696,30 @@ def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do 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" + return thm + +def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchTheorem)) := do + let some eqns ← getEqnsFor? declName | return none + eqns.mapM fun eqn => do + /- + We disable normalization because we don't want to reduce equation theorems's LHS such as + `List.replicate 0 [] = []` + -/ + mkEMatchEqTheorem eqn (normalizePattern := false) + private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do if (← getConstInfo declName).isTheorem then ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind - else if let some eqns ← getEqnsFor? declName then + else if let some thms ← mkEMatchEqTheoremsForDef? declName then unless useLhs do throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns" - for eqn in eqns do - ematchTheoremsExt.add (← mkEMatchEqTheorem eqn) attrKind + thms.forM (ematchTheoremsExt.add · attrKind) else throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions" -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" - return thm - private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do if thmKind == .eqLhs then addGrindEqAttr declName attrKind thmKind (useLhs := true) From 99a5108523245f5513f673060c3218baab4bdf28 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2025 18:40:16 -0800 Subject: [PATCH 2/3] chore: improve error messages --- src/Lean/Declaration.lean | 4 +++ src/Lean/Elab/Tactic/Grind.lean | 29 ++++++++++++------- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 6 +--- src/Lean/Meta/Tactic/Grind/SimpUtil.lean | 18 +++++++++++- 4 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 3ce068d3eca3..97ea0ad4987e 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -469,6 +469,10 @@ def isInductive : ConstantInfo → Bool | .inductInfo _ => true | _ => false +def isDefinition : ConstantInfo → Bool + | .defnInfo _ => true + | _ => false + def isTheorem : ConstantInfo → Bool | .thmInfo _ => true | _ => false diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 98f70534d397..08ccdfca5e75 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -49,18 +49,25 @@ def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic. let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default if (← isInductivePredicate declName) then throwErrorAt p "NIY" - else if (← getConstInfo declName).isTheorem then - 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) } - else if let some thms ← Grind.mkEMatchEqTheoremsForDef? declName then - if kind != .eqLhs && kind != .default then - throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='" - params := { params with extra := params.extra ++ thms.toPArray' } else - throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type" + 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" | _ => throwError "unexpected `grind` parameter{indentD p}" return params diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 1b3b22cd9239..eb0e94ea40b1 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -704,11 +704,7 @@ def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMa def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchTheorem)) := do let some eqns ← getEqnsFor? declName | return none eqns.mapM fun eqn => do - /- - We disable normalization because we don't want to reduce equation theorems's LHS such as - `List.replicate 0 [] = []` - -/ - mkEMatchEqTheorem eqn (normalizePattern := false) + mkEMatchEqTheorem eqn (normalizePattern := true) private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do if (← getConstInfo declName).isTheorem then diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean index 878b0fc59356..26b0a71b8903 100644 --- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean +++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean @@ -7,6 +7,7 @@ prelude import Lean.Meta.Tactic.Simp.Simproc import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.DoNotSimp +import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List namespace Lean.Meta.Grind @@ -14,7 +15,22 @@ namespace Lean.Meta.Grind protected def getSimprocs : MetaM (Array Simprocs) := do let s ← grindNormSimprocExt.getSimprocs let s ← addDoNotSimp s - return #[s, (← Simp.getSEvalSimprocs)] + let e ← Simp.getSEvalSimprocs + /- + We don't want to apply `List.reduceReplicate` as a normalization operation in + `grind`. Consider the following example: + ``` + example (ys : List α) : n = 0 → List.replicate n ys = [] := by + grind only [List.replicate] + ``` + The E-matching module generates the following instance for `List.replicate.eq_1` + ``` + List.replicate 0 [] = [] + ``` + We don't want it to be simplified to `[] = []`. + -/ + let e := e.erase ``List.reduceReplicate + return #[s, e] /-- Returns the simplification context used by `grind`. -/ protected def getSimpContext : MetaM Simp.Context := do From c6719e02d752beb8a0f0929e03e8bf5f7a7f54ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2025 18:41:11 -0800 Subject: [PATCH 3/3] chore: add tests --- tests/lean/run/grind_ematch_patterns.lean | 48 +++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 tests/lean/run/grind_ematch_patterns.lean diff --git a/tests/lean/run/grind_ematch_patterns.lean b/tests/lean/run/grind_ematch_patterns.lean new file mode 100644 index 000000000000..a7cf3c3a37bf --- /dev/null +++ b/tests/lean/run/grind_ematch_patterns.lean @@ -0,0 +1,48 @@ +def replicate : (n : Nat) → (a : α) → List α + | 0, _ => [] + | n+1, a => a :: replicate n a + +/-- +info: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0] +[grind.ematch.pattern] replicate.eq_2: [@replicate #2 (Lean.Grind.offset #0 (1)) #1] +-/ +#guard_msgs (info) in +set_option trace.grind.ematch.pattern true in +attribute [grind] replicate + +example : ys = [] → replicate 0 [] = ys := by + grind only [replicate] + +/-- +error: invalid `grind` parameter, `replicate` is a definition, the only acceptable (and redundant) modifier is '=' +-/ +#guard_msgs (error) in +example : ys = [] → replicate 0 [] = ys := by + grind only [←replicate] + +example : ys = [] → replicate 0 [] = ys := by + fail_if_success grind only + sorry + +example (ys : List α) : n = 0 → replicate n ys = [] := by + grind only [replicate] + +example (ys : List α) : n = 0 → List.replicate n ys = [] := by + grind only [List.replicate] + +opaque foo : Nat → Nat +opaque bla : Nat → Nat + +theorem foo_bla : foo x = bla x := sorry + +example : foo x = bla x := by + grind only [_=_ foo_bla] + +@[reducible] def inc (_ : Nat) := 1 + +/-- +error: `inc` is a reducible definition, `grind` automatically unfolds them +-/ +#guard_msgs (error) in +example : a = 1 → inc x = a := by + grind [inc]