False positives for tryAtEachStep linter and grind +suggestions tactic #36440
Description
Sometimes when I run tryAtEachStep linter to identify which steps (or multiple subsequent steps) in the proof can be performed by grind +suggestions I encounter false positives: the linter says I can replace a proof step with the tactic, but when I actually replace, the proof does not pass. I think I observed it only for grind +suggestions , other tactics (including grind) do not result in such false positives.
An example: let's say we use Lean and mathlib 4.28.0 and have example.lean with this content:
import Mathlib
set_option linter.tacticAnalysis.tryAtEachStep.selfReplacements false
set_option linter.tacticAnalysis.tryAtEachStepFromEnv true
theorem Munkres_exercise_17_4 {X : Type*} [TopologicalSpace X]
(U A : Set X) (hU : IsOpen U) (hA : IsClosed A) :
IsOpen (U \ A) ∧ IsClosed (A \ U) := by
have h1 : IsOpen (U \ A) := by
exact IsOpen.inter hU (isOpen_compl_iff.mpr hA)
have h2 : IsClosed (A \ U) := by
exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)
exact ⟨h1, h2⟩when I run
export TRY_AT_EACH_STEP_TACTIC=grind+suggestions
lake env lean --json example.lean | jq .
I get info with multiple replacement suggestions, in particular :
{
...
"caption": "",
"data": "`exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)` can be replaced with `grind+suggestions` (76ms)",
"endPos": {
"column": 55,
"line": 12
},
"fileName": "example.lean",
"isSilent": false,
"keepFullRange": false,
"kind": "[anonymous]",
"pos": {
"column": 4,
"line": 12
},
"severity": "information"
...
}
This is saying that the proof of h2 statement may be done just by grind+suggestions. However, when I actually replace this proof step in the file with grind+suggestions, it does not work:
import Mathlib
set_option linter.tacticAnalysis.tryAtEachStep.selfReplacements false
set_option linter.tacticAnalysis.tryAtEachStepFromEnv true
theorem Munkres_exercise_17_4 {X : Type*} [TopologicalSpace X]
(U A : Set X) (hU : IsOpen U) (hA : IsClosed A) :
IsOpen (U \ A) ∧ IsClosed (A \ U) := by
have h1 : IsOpen (U \ A) := by
exact IsOpen.inter hU (isOpen_compl_iff.mpr hA)
have h2 : IsClosed (A \ U) := by grind +suggestions
--exact IsClosed.inter hA (isClosed_compl_iff.mpr hU)
exact ⟨h1, h2⟩▼ 11:36-11:54: error:
`grind` failed
case grind.1.1.1.1.1.1.1
X : Type u_1
inst : TopologicalSpace X
U A : Set X
hU : IsOpen U
hA : IsClosed A
h1 : IsOpen (U \ A)
h : ¬IsClosed (A \ U)
w : X
h_2 : ¬∀ (F : Filter X), F.NeBot → F ≤ Filter.principal (A \ U) → F ≤ nhds w → w ∈ A \ U
w_1 : X
h_4 : ¬((∃ᶠ (y : X) in nhds w_1, y ∈ A \ U) → w_1 ∈ A \ U)
w_2 : X
left : ∀ a ∈ nhds w_2, (a ∩ (A \ U)).Nonempty
right : w_2 ∉ A \ U
w_3 : Filter X
h_8 : ¬(w_3.NeBot → w_3 ≤ Filter.principal (A \ U) → w_3 ≤ nhds w → w ∈ A \ U)
w_4 : X
h_10 : ¬(w_4 ∈ closure (A \ U) → w_4 ∈ A \ U)
h_11 : w_1 ∉ A
h_12 : w_2 ∉ A
h_13 : w ∉ A
w_5 : Set X
h_14 : ¬(w_5 ∈ nhds w → (w_5 ∩ A).Nonempty)
w_6 : X
h_15 : (w_6 ∈ closure (A \ U)) = (w_6 ∉ A \ U)
w_7 : Set X
h_16 : ¬(w_7 ∈ nhds w_1 → (w_7 ∩ A).Nonempty)
w_8 : Set X
h_17 : ¬(w_8 ∈ nhds w_2 → (w_8 ∩ A).Nonempty)
h_18 : w_4 ∉ A
left_1 : w_6 ∈ closure (A \ U)
right_1 : w_6 ∉ A \ U
left_2 : A \ U ⊆ A \ U
right_2 : ∀ (x : X), True
w_9 : Set X
h_21 : ¬(w_9 ∈ nhds w_4 → (w_9 ∩ A).Nonempty)
h_22 : w_6 ∉ A
w_10 : Set X
h_23 : ¬(w_10 ∈ nhds w_6 → (w_10 ∩ A).Nonempty)
⊢ False
Any help here would be much appreciated!