Proving termination/correctness of KMP helper

Stream: Program verification

[Clarence Chew]

I'm trying out Lean4 so I'm proving some stuff as practice. I'm trying to implementing KMP, but for now it's just the function that calculates how much to jump forward while string searching. Below is what I tried.

/-
Implementation details:
(boundary W i) gives the length of the longest prefix which is also a proper suffix of W[0:i].
(boundary W 0) is defined to be -1

Note that (boundary W i) >= (boundary W (i-1)) + 1

(boundary helper W i j) gives the length of the longest prefix which is also a proper suffix of W[0:i],
given that
- j is the length of some prefix which is also a suffix of W[0:i-1]
- we tried extending all prefixes which are also suffixes of W[0:i-1], longer than j, and it didn't work

(boundary W 0) is defined to be -1
(boundary W 1) is calculatable as 0
-/
mutual
  def boundary (W : String) (i : Nat) (h : i ≤ W.length) : Int :=
    have boundary_zero_eq_neg_one (W : String) : (boundary W Nat.zero (Nat.zero_le W.length)) + 1 = 0 := by
      -- boundary.casesOn
      sorry
    have boundary_loop_inv (W : String) (i : Nat) (h : i ≤ W.length) : (boundary W i h) + 1 ≤ i := by
      /- induction' i with zero succ
      rw [boundary_zero_eq_neg_one W]
      linarith-/
      sorry
      /-have hyp : boundary W (Nat.succ a) h + 1 ≤ (Nat.succ a) := by
        exact (ha h)-/
    match i with
    | Nat.zero => -1
    | Nat.succ k => Id.run do {
      have boundary_hyp : k ≤ W.length := by
        linarith
      have boundary_helper_hyp : (boundary W k boundary_hyp) + 2 ≤  Int.ofNat (Nat.succ k) := by
        have hyp : (boundary W k boundary_hyp) + 2 ≤ k + 1 := by
          have hyp : (boundary W k boundary_hyp) + 1 ≤ k := by
            exact (boundary_loop_inv W k boundary_hyp)
          linarith
        have hyp2 : Int.ofNat k + 1 ≤ Int.ofNat (Nat.succ k) := by
          sorry
        exact (le_trans hyp hyp2)
      boundary_helper W (Nat.succ k) h (boundary W k boundary_hyp) boundary_helper_hyp
    }
  def boundary_helper (W : String) (i : Nat) (h : i ≤ W.length) (j : Int) (hj : j + 2 ≤ i) : Int :=
    match j, (W.take (i-1) == W.take (Int.toNat j)) with
    | Int.negSucc _, _ => 0
    | _, true => j+1
    | Int.ofNat k, false => Id.run do {
      have hyp : k ≤ W.length := by
        sorry
      have boundary_helper_hyp : (boundary W k hyp) + 2 ≤ i := by
        sorry
      boundary_helper W i h (boundary W k hyp) boundary_helper_hyp
    }
end
termination_by
  boundary W i h => (i, i)
  boundary_helper W i h j hj => (i, Int.toNat (j + 1))
decreasing_by
  simp_wf
  have hyp : 0 ≤ i := by
    exact (Nat.zero_le i)
  /-have termination_hyp1 (k : Nat) : (k, k) < (Nat.succ k, Nat.succ k) := by
    sorry
  have termination_hyp2 : (Nat.succ k, Int.toNat (boundary W k boundary_hyp)) < (Nat.succ k, Nat.succ k) := by
    sorry
  have termination_hyp3 : (boundary W k hyp) + 1 ≤ k := by
    sorry-/
  sorry

I tried running the definition with

lemma h : (4 ≤ "123123123".length) := by sorry
#eval boundary "123123123" 4 h

expected value: 1, actual value: 0

Also, in the decreasing_by block I'm getting a goal of the following (Prod.Lex):
image.png
I'm confused because I'm not sure why Lean is getting me to prove (0, 0) < (i, i). It's false because i could be 0.

[Clarence Chew]

Update: I rewrote it in this form, it seems more promising to prove the required results to demonstrate termination.

def boundary (W : String) (i : Nat) (h : i ≤ W.length) : Int :=
  ...
where boundary_helper (W : String) (i : Nat) (h : i ≤ W.length) (j : Int) (hj : j + 2 ≤ i) : Int :=
  ...
termination_by
  ...
decreasing_by
  ...