diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index c80a8b2361..8019efb4e6 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -68,6 +68,17 @@ def elabInitGrindNorm : CommandElab := fun stx => Grind.registerNormTheorems pre post | _ => throwUnsupportedSyntax +private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do + let kinds ← match s.getKindsFor (.decl declName) with + | [] => return () + | [k] => pure m!"@{k.toAttribute}" + | [.eqLhs gen, .eqRhs _] + | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute}" + | ks => + let ks := ks.map fun k => m!"@{k.toAttribute}" + pure m!"{ks}" + logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`" + def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do let mut params := params for p in ps do @@ -125,14 +136,19 @@ where let info ← getAsyncConstInfo declName match info.kind with | .thm | .axiom | .ctor => - if params.ematch.containsWithSameKind (.decl declName) kind then - logWarning m!"this parameter is redundant, environment already contains `@{kind.toAttribute} {declName}`" match kind with | .eqBoth gen => - let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios) } - return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios) } + let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios + let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios + if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns && + params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then + warnRedundantEMatchArg params.ematch declName + return { params with extra := params.extra.push thm₁ |>.push thm₂ } | _ => - return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind params.symPrios) } + let thm ← Grind.mkEMatchTheoremForDecl declName kind params.symPrios + if params.ematch.containsWithSamePatterns thm.origin thm.patterns then + warnRedundantEMatchArg params.ematch declName + return { params with extra := params.extra.push thm } | .defn => if (← isReducible declName) then throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them" @@ -203,7 +219,7 @@ def evalGrindCore let only := only.isSome let params := if let some params := params then params.getElems else #[] if Grind.grind.warning.get (← getOptions) then - logWarningAt ref "The `grind` tactic is new and its behaviour may change in the future. This project has used `set_option grind.warning true` to discourage its use." + logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use." withMainContext do let result ← grind (← getMainGoal) config only params fallback replaceMainGoal [] diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 2fdee13240..f10c07012a 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -441,17 +441,18 @@ def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems def EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) : Bool := s.erased.contains origin -/-- Returns `true` if there is a theorem with exactly the same kind is already in `s` -/ -def EMatchTheorems.containsWithSameKind (s : EMatchTheorems) (origin : Origin) (kind : EMatchTheoremKind) : Bool := - match kind with - | .eqBoth gen => go (.eqLhs gen) && go (.eqRhs gen) - | _ => go kind -where - go (kind : EMatchTheoremKind) : Bool := - if let some thms := s.omap.find? origin then - thms.any fun thm => thm.kind == kind - else - false +/-- Returns `true` if there is a theorem with exactly the same pattern is already in `s` -/ +def EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin) (patterns : List Expr) : Bool := + if let some thms := s.omap.find? origin then + thms.any fun thm => thm.patterns == patterns + else + false + +def EMatchTheorems.getKindsFor (s : EMatchTheorems) (origin : Origin) : List EMatchTheoremKind := + if let some thms := s.omap.find? origin then + thms.map (·.kind) + else + [] /-- Retrieves theorems from `s` associated with the given symbol. See `EMatchTheorem.insert`. diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index a335a1abab..aa473f7cc7 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -948,7 +948,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) next k_ne_i => have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k - grind [Fin.getElem_fin] + grind · by_cases li.2 = true next li_eq_true => have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by diff --git a/tests/lean/run/grind_warn_param.lean b/tests/lean/run/grind_warn_param.lean index a216315f7c..5dd9e2ff26 100644 --- a/tests/lean/run/grind_warn_param.lean +++ b/tests/lean/run/grind_warn_param.lean @@ -16,36 +16,69 @@ opaque g : Nat → Nat → Nat theorem hg : h x = g x (g x x) := sorry /-- -warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set` +warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]` -/ #guard_msgs (warning) in example : True := by grind [= Array.size_set] -/-- warning: this parameter is redundant, environment already contains `@[grind →] pqf` -/ +/-- +warning: this parameter is redundant, environment already contains `pqf` annotated with `@[grind →]` +-/ #guard_msgs (warning) in example : True := by grind [→ pqf] /-- -warning: this parameter is redundant, environment already contains `@[grind →] pqf` +warning: this parameter is redundant, environment already contains `pqf` annotated with `@[grind →]` --- -warning: this parameter is redundant, environment already contains `@[grind =] Array.size_set` +warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]` -/ #guard_msgs (warning) in example : True := by grind [→ pqf, = Array.size_set] -/-- warning: this parameter is redundant, environment already contains `@[grind _=_] hg` -/ +/-- +warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]` +-/ +#guard_msgs (warning) in +example : True := by grind [Array.size_set] + +/-- +warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]` +-/ #guard_msgs (warning) in example : True := by grind [_=_ hg] -/-- warning: this parameter is redundant, environment already contains `@[grind =_] hg` -/ +/-- +warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]` +-/ #guard_msgs (warning) in example : True := by grind [=_ hg] +/-- +warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]` +-/ #guard_msgs (warning) in example : True := by grind [Array.size_set] #guard_msgs (warning) in example : True := by grind [pqf] +/-- +warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]` +-/ #guard_msgs (warning) in example : True := by grind [hg] + +@[grind =] theorem mem_range : m ∈ List.range n ↔ m < n := + sorry + +/-- +warning: this parameter is redundant, environment already contains `mem_range` annotated with `@[grind =]` +-/ +#guard_msgs (warning) in +example : True := by grind [mem_range] + +/-- +warning: this parameter is redundant, environment already contains `mem_range` annotated with `@[grind =]` +-/ +#guard_msgs (warning) in +example : True := by grind [= mem_range]