Proving termination for Parsec

Stream: lean4

[Yakov Pechersky]

Consider:

import Lean.Data.Parsec

open Lean

def moveToEnd : Parsec Unit := do
  let c ← Parsec.anyChar
  dbg_trace c
  moveToEnd <|> pure ()

#eval moveToEnd.run "ab"

What's the right approach to prove termination here? Use an explicit fun it?

[Yakov Pechersky]

I seem to have made some progress with my moveToEnd and moveToEnd' below, but now I don't know why the moveToEnd' has two independent String.Iterators. For the case of the more "manual" definition in moveToEnd, how do I restrict the termination obligation to just a subset of cases where it.hasNext? Since if that's not true, then one terminates right away.

import Lean.Data.Parsec

theorem Nat.lt_add_right_iff {m n : Nat} : m < m + n ↔ 0 < n := by sorry

theorem Nat.sub_lt_sub_left_of_le {a b c : Nat} (h : b ≤ a) (h' : c < b) :
    a - b < a - c := by sorry

open Lean

theorem csize_pos (c : Char) : 0 < String.csize c := String.one_le_csize c
theorem pos_le_pos_iff {p q : String.Pos} : p ≤ q ↔ p.byteIdx ≤ q.byteIdx := Iff.rfl
theorem pos_lt_pos_iff {p q : String.Pos} : p < q ↔ p.byteIdx < q.byteIdx := Iff.rfl
@[simp] theorem byteIdx_pos_add_char (p : String.Pos) (c : Char) :
  (p + c).byteIdx = p.byteIdx + String.csize c := rfl
theorem pos_lt_add_char_right (p : String.Pos) (c : Char) : p < p + c := by
  simp [pos_lt_pos_iff, Nat.lt_add_right_iff, csize_pos]

@[simp] theorem String.Iterator.s_next (it : String.Iterator) : it.next.s = it.s := rfl
@[simp] theorem String.Iterator.pos_next (it : String.Iterator) : it.next.pos = it.s.next it.pos := rfl

def moveToEnd : Parsec Unit := fun it => Id.run <| do
  let Parsec.ParseResult.success _ c ← Parsec.anyChar it | return Parsec.ParseResult.error it "end"
  dbg_trace c
  return moveToEnd it.next
termination_by moveToEnd it => it.s.length - it.pos.byteIdx
decreasing_by {
  -- a✝: String.Iterator -- only one such String.Iterator
  rename String.Iterator => it
  simp_wf
  simp
  refine Nat.sub_lt_sub_left_of_le ?_ ?_
  sorry
  sorry
}

def moveToEnd' : Parsec Unit := fun it => ((do
  let c ← Parsec.anyChar
  dbg_trace c
  moveToEnd') <|> pure () : Parsec Unit) it
termination_by moveToEnd' it => it.s.length - it.pos.byteIdx
decreasing_by {
  -- a✝¹a✝: String.Iterator -- two such String.Iterators
  rename String.Iterator => it -- (aside, how do I rename both)
  simp_wf
  sorry
}

#eval moveToEnd.run "ab"
#eval moveToEnd'.run "ab"