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 34425ac40e01..08ccdfca5e75 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -49,13 +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 - 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) } else - throwError "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.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..eb0e94ea40b1 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,26 @@ 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 + mkEMatchEqTheorem eqn (normalizePattern := true) + 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) 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 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]