grind depends on its surroundings

Stream: lean4

[Snir Broshi]

import Mathlib
namespace SimpleGraph.Walk
variable {V : Type*} {G : SimpleGraph V}

theorem fst_darts_getElem? {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.length) :
    (p.darts[i]'(by grind [length_darts])).fst = p.support[i]'(by grind [length_support]) := by
  sorry
theorem snd_darts_getElem? {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.length) :
    (p.darts[i]'(by grind [length_darts])).snd = p.support[i + 1]'(by grind [length_support]) := by
  sorry

theorem error {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'}
    (hnil : ¬p₁.Nil) : p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts := by
  simp only [isSubwalk_iff_support_isInfix, List.infix_iff_getElem?, length_support, length_darts]
  refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
  · rw [getElem?_pos _ _ <| by grind [length_darts], Option.some_inj]
    ext <;> grind [fst_darts_getElem?, snd_darts_getElem?]
  · rw [getElem?_pos _ _ <| by grind [length_support], Option.some_inj]
    by_cases hi' : i = p₁.length
    · have : 0 < i := by grind [not_nil_iff_lt_length]
      have := h (i - 1) <| by cutsat
      grind [fst_darts_getElem?, snd_darts_getElem?]
    have := h i
    grind [fst_darts_getElem?]

(couldn't figure out how to avoid Mathlib in the mwe, sorry)

---

Currently the grind inside by_cases (line 23) is failing. I know of 5 mysterious ways to fix it:

1. Swap the by cutsat above it to by grind:

-have := h (i - 1) <| by cutsat
+have := h (i - 1) <| by grind

2. Delete the by cutsat proof arg entirely:

-have := h (i - 1) <| by cutsat
+have := h (i - 1)

3. Duplicate the have:

 have := h (i - 1) <| by cutsat
+have := h (i - 1) <| by cutsat

4. Add set_option trace.grind.debug true before the theorem

5. Replace the proof in the first cdot of the proof (lines 17-18) with sorry:

-  · rw [getElem?_pos _ _ <| by grind [length_darts], Option.some_inj]
-    ext <;> grind [fst_darts_getElem?, snd_darts_getElem?]
+  · sorry

Spooky action at a distance.

---

My best guess is that all grinds in a proof share a common "fuel", so the sub-proofs can affect grinds outside. What's going on? I'm thoroughly confused.

(original discussion: #new members > `grind` depends on proof inside `have`)

[Snir Broshi]

image.png
Now I'm even more confused, what are these magic hex numbers?
(this is when using solution number 2)

[Chris Henson]

I don't believe they are documented fully in the reference manual yet, but these were introduced in lean4#10709 as part of the grind interactive mode.

[Kim Morrison]

@Snir Broshi, this appears to already be working on the latest nightly.

I verified this (for future reference for you, or any other bug reporters! :-) by running:

git remote add nightly-testing git@github.com:leanprover-community/mathlib4-nightly-testing.git
git fetch nightly-testing
git checkout nightly-testing-green
lake exe cache get

and then pasting in your code.