analyzing the definition of `Substring.next`

Stream: mathlib4

[Bulhwi Cha]

import Mathlib.Data.String.Basic

namespace Substring

def next' : Substring → String.Pos → String.Pos
  | ⟨s, b, e⟩, p =>
    let absP := b+p
    if absP = e then p else p + s.get absP

theorem next_eq_next' : next = next' := by
  funext ⟨s, b, e⟩ p
  simp [next, next']
  split
  · rfl
  · simp [String.next, String.Pos.ext_iff]
    show b.byteIdx + p.byteIdx + String.csize (String.get s (b + p)) - b.byteIdx =
         p.byteIdx + String.csize (String.get s (b + p))
    rw [Nat.add_comm, Nat.add_sub_assoc, Nat.add_sub_self_left, Nat.add_comm]
    apply Nat.le_add_right

end Substring

Is there a better way to prove the above theorem?

[Kevin Buzzard]

To unobfuscate: I think you're really asking how to prove foo, right?

@[simp] lemma String.byteIdx_add {b p : String.Pos}  :
  (b + p).byteIdx = b.byteIdx + p.byteIdx := rfl

lemma foo (a b c : ℕ) : a + b + c - a = b + c := sorry

theorem next_eq_next' : next = next' := by
  funext ⟨s, b, e⟩ p
  simp [next, next']
  split
  · rfl
  · simp [String.next, foo]

[Floris van Doorn]

foo is docs4#Nat.add_sub_cancel_left / docs4#add_tsub_cancel_left or maybe one add_assoc away from it.

[Bulhwi Cha]

Kevin Buzzard said:

To unobfuscate: I think you're really asking how to prove foo, right?

Right, but I also wonder whether we need to include several lemmas like String.byteIdx_add in Lean's core library.

[Bulhwi Cha]

Floris van Doorn said:

foo is docs4#Nat.add_sub_cancel_left / docs4#add_tsub_cancel_left or maybe one add_assoc away from it.

Thanks!

example (a b c : Nat) : a + b + c - a = b + c := by
  rw [Nat.add_assoc, Nat.add_sub_cancel_left]

Edited proof

import Std.Data.String.Lemmas

namespace Substring

def next' : Substring → String.Pos → String.Pos
  | ⟨s, b, e⟩, p =>
    let absP := b+p
    if absP = e then p else p + s.get absP

theorem next_eq_next' : next = next' := by
  funext ⟨s, b, e⟩ p
  simp [next, next']
  split
  · rfl
  · simp [String.next, String.Pos.ext_iff]
    rw [Nat.add_assoc, Nat.add_sub_cancel_left]

end Substring

[Bulhwi Cha]

Now Kevin Buzzard's proof should be modified as follows:

Edited proof

lemma foo (a b c : ℕ) : a + b + c - a = b + c := sorry

theorem next_eq_next' : next = next' := by
  funext ⟨s, b, e⟩ p
  simp [next, next']
  split
  · rfl
  · simp [String.next, String.Pos.ext_iff, foo]