Need help proving termination!

Stream: new members

[Igor Shimanogov]

Hey guys! Looking forward to help mathlib. For the firsts contribution I came up with idea of proving equalent condition of List commutativity (Lyndon-Schutzenberger lemma). Can some one help me to fancify my proof and prooving that recursion is terminating? Best regards!
https://gist.github.com/MrSumato/275a10e182044f915dea2e54cb879d8b

[Johannes Tantow]

I think you need to rewrite your proof as -- t is smaller then p! is not necessarily true. It should be possible that p, q and t are all empty and hence the theorem does not terminate.

[Johannes Tantow]

also #mwe . If you post your code directly here, then others only have to click the button and not have to copy to the live-lean.

[Igor Shimanogov]

Thx for the comments!
I managed to finish the proof and showed that it is terminating.

import Mathlib.Data.Prod.Basic
import Mathlib.Data.Nat.Init

universe u

variable {α : Type u} {v u w : List α} {n m : Nat}

def repeatList : Nat → List α → List α
  | Nat.zero, _ => []
  | Nat.succ p, l => l ++ repeatList p l

def repeat_list_homo : repeatList n w ++ repeatList m w = repeatList (n+m) w := by
  induction n with
  | zero => simp [repeatList]
  | succ p ih => simp [repeatList, List.append_assoc, ih, Nat.add_assoc, Nat.add_comm]

def prefix_if_concat_comm : (u ++ v = v ++ u) → (v <+: u ∨ u <+: v) := by
  intro h
  rw [List.append_eq_append_iff] at h
  cases h with
  | inl r =>
    right
    obtain ⟨as, h₁, h₂⟩ := r
    rw [h₁]
    exact List.prefix_append u as
  | inr l =>
    left
    obtain ⟨as, h₁, h₂⟩ := l
    rw [h₁]
    exact List.prefix_append v as

theorem lyndon_schutzenberger {q p : List α} : (q ++ p = p ++ q) ↔ (∃ w k l, q = repeatList k w ∧ p = repeatList l w) := by
  constructor
  -- Forward direction (u++v=v++u → ∃w k l...)
  · intro h
    have pr := prefix_if_concat_comm h
    match p, q with
      | [], smth =>
        exists smth, 1, 0
        constructor
        simp [repeatList]
        simp [repeatList]
      | smth, [] =>
        exists smth, 0, 1
      | hp :: tp, hq :: tq =>
        cases pr with
        | inr qp =>
          cases qp with
          | intro t ht =>
            rw [← ht]
            rw [← ht, List.append_assoc, List.append_cancel_left_eq] at h
            have bb := lyndon_schutzenberger.mp h
            cases bb with | intro wc wct =>
            cases wct with | intro kc kct =>
            cases kct with | intro lc lct =>
            cases lct with
            | intro left right =>
              exists wc, kc, (kc+lc)
              constructor
              assumption
              simp [left, right, repeat_list_homo]
        | inl pq =>
          cases pq with
            | intro t ht =>
              rw [← ht]
              rw [← ht, List.append_assoc, List.append_cancel_left_eq] at h
              have bb := lyndon_schutzenberger.mp h.symm
              cases bb with | intro wc wct =>
              cases wct with | intro kc kct =>
              cases kct with | intro lc lct =>
              cases lct with
              | intro left right =>
                exists wc, (kc+lc), kc
                constructor
                simp [left, right, repeat_list_homo]
                assumption

  -- Reverse direction (∃w k l... → u++v=v++u)
  · rintro ⟨w, k, l, rfl, rfl⟩
    simp [repeat_list_homo, Nat.add_comm]

termination_by (p++q).length
decreasing_by

  have n : (hp :: tp).length + t.length = (hq :: tq).length := by
      rw [← List.length_append]
      exact congrArg List.length ht
  rw [List.length_append, Nat.add_comm, n, List.length_append, List.length_cons]
  simp

  have n : (hq :: tq).length + t.length = (hp :: tp).length := by
     rw [← List.length_append]
     exact congrArg List.length ht
  rw [List.length_append, Nat.add_comm, n, List.length_append, List.length_cons]
  simp

So I have some followup questions. Is it enough for the first contribution? What part of Mathlib it belongs to? How I can made this proof cleaner or shorter?