Adaptation note in DyckWord

Stream: mathlib4

[Jeremy Tan]

@Michael Rothgang

include h in
lemma firstReturn_pos : 0 < p.firstReturn := by
  by_contra! f
  rw [Nat.le_zero, firstReturn, findIdx_eq] at f
  #adaptation_note
  /--
  If we don't swap, then the second goal is dropped after completing the first goal.
  What's going on?
  -/
  swap
  · rw [length_range, length_pos_iff]
    exact toList_ne_nil.mpr h
  · rw [getElem_range] at f
    simp at f
    rw [← p.cons_tail_dropLast_concat h] at f
    simp at f

In trying to remove this adaptation note (#24492) I have found out the following.

[Jeremy Tan]

Just before the findIdx_eq rewrite the goal state is the following

p : DyckWord
h : p ≠ 0
f : findIdx (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ False

[Jeremy Tan]

After the rewrite:

p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f : decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
    true ∧
  ∀ (j : ℕ) (hji : j < 0),
    decide (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
      false
⊢ False

p : DyckWord
h : p ≠ 0
f : findIdx (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ 0 < (range (↑p).length).length

[Jeremy Tan]

By contrast, if I write it like

include h in
lemma firstReturn_pos : 0 < p.firstReturn := by
  rw [← not_le, Nat.le_zero, firstReturn, findIdx_eq, getElem_range]
  · simp
    rw [← p.cons_tail_dropLast_concat h]
    simp
  · rwa [length_range, length_pos_iff, toList_ne_nil]

no spurious f✝ hypothesis is generated. Why would f✝ be generated in the first case?

[Jeremy Tan]

Now suppose I have

include h in
lemma firstReturn_pos : 0 < p.firstReturn := by
  by_contra! f
  have k : 0 < (range p.toList.length).length := by
    rw [length_range, length_pos_iff]
    exact toList_ne_nil.mpr h
  rw [Nat.le_zero, firstReturn, findIdx_eq k] at f
  rw [getElem_range] at f
  simp at f
  rw [← p.cons_tail_dropLast_concat h] at f
  simp at f

Then when the findIdx rewrite happens, f jumps from above k in the hypothesis list to below it:

p : DyckWord
h : p ≠ 0
f : findIdx (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
k : 0 < (range (↑p).length).length
⊢ False

p : DyckWord
h : p ≠ 0
k : 0 < (range (↑p).length).length
f : decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
    true ∧
  ∀ (j : ℕ) (hji : j < 0),
    decide (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
      false
⊢ False

Is this a bug?

[Damiano Testa]

The ordering of the hypotheses is, initially, "chronological". Once you start modifying them, the hypothesis that was just modified becomes last. This means that the answer to your last question may be that this is not a bug, but expected behaviour.

[Damiano Testa]

As for disappearing goals, that is usually a consequence of a goal solved by unification, while Lean realises what the ingredients of a proof are in a separate branch.

[Damiano Testa]

So, Lean figures out what the relevant metavariables are in one branch and then propagates this information to the branches that were created when the first one was also created, now has the information of what they need to be and, sometimes, this is information enough to actually solve them.