why do these cumbersome hypotheses keep showing up?

Stream: batteries

[Bulhwi Cha]

Bulhwi Cha said:

When I proved that the theorem String.splitOnAux_of_valid terminates, I had to hide more than ten illegible hypotheses from each goal: https://github.com/leanprover-community/batteries/pull/743/files#diff-38e93b9f694cdc66d675df840d70c3c0d47cc4b5a1813c4aa7d4d7744efff544R487-R510.

I wonder why these unwanted hypotheses show up. Here's the hypothesis _₀ of the first goal:

Hypothesis

_₀ : ∀
  (y :
    (_ : List Char) ×'
      (sep₂ : List Char) ×' (_ : List Char) ×' (_ : List Char) ×' (_ : List Char) ×' (_ : List String) ×' sep₂ ≠ []),
  (invImage
          (fun x =>
            PSigma.casesOn x fun sep₁ sep₂ =>
              PSigma.casesOn sep₂ fun sep₂ l =>
                PSigma.casesOn l fun l m =>
                  PSigma.casesOn m fun m r =>
                    PSigma.casesOn r fun r acc =>
                      PSigma.casesOn acc fun acc h => (utf8Len sep₁ + utf8Len r, utf8Len sep₂))
          Prod.instWellFoundedRelation).1
      y ⟨sep₁, sep₂✝⟩ →
    { data := y.2.2.1 ++ y.2.2.2.1 ++ y.1 ++ y.2.2.2.2.1 }.splitOnAux { data := y.1 ++ y.2.1 }
        { byteIdx := utf8Len y.2.2.1 } { byteIdx := utf8Len (y.2.2.1 ++ y.2.2.2.1 ++ y.1) } { byteIdx := utf8Len y.1 }
        y.2.2.2.2.2.1 =
      y.2.2.2.2.2.1.reverse ++
        List.map mk (List.modifyHead (fun x => y.2.2.2.1 ++ x) (y.2.2.2.2.1.splitOnListAux y.1 y.2.1 ⋯))

Today, I had to clean up twenty-seven hypotheses while writing the termination proof for one of my new theorems in Batteries#987:

See the last theorem of my code

namespace List

theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
  intro heq
  simp [heq, nil_prefix] at h

section

variable [DecidableEq α]

/-- Returns the longest common prefix of two lists. -/
def commonPrefix : (l₁ l₂ : List α) → List α
  | [], _ => []
  | _, [] => []
  | a₁::l₁, a₂::l₂ =>
    if a₁ = a₂ then
      a₁ :: (commonPrefix l₁ l₂)
    else
      []

theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by
  match l₁, l₂ with
  | [],   _  => simp [commonPrefix]
  | _::_, [] => simp [commonPrefix]
  | a₁::l₁, a₂::l₂ =>
    simp only [commonPrefix]
    cases Decidable.em (a₁ = a₂)
    · next h =>
      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
      apply commonPrefix_prefix_left
    · next h =>
      simp [h]

theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by
   match l₁, l₂ with
  | [],   _  => simp [commonPrefix]
  | _::_, [] => simp [commonPrefix]
  | a₁::l₁, a₂::l₂ =>
    simp only [commonPrefix]
    cases Decidable.em (a₁ = a₂)
    · next h =>
      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
      apply commonPrefix_prefix_right
    · next h =>
      simp [h]

theorem commonPrefix_append_append (p l₁ l₂ : List α) :
    commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by
  match p with
  | []   => rfl
  | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂

theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p)
    (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧
      t₁.head? ≠ t₂.head? := by
  constructor <;> intro h
  · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
    obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
    cases Decidable.em (a₁ = a₂)
    · subst a₂
      simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂
      simp only [cons_prefix_cons, true_and] at h
      exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h
    · next hne =>
      simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂
      simp [← h₁, ← h₂, hne]
  · rw [h₁, h₂]
    let ⟨ht₁, ht₂, hhd⟩ := h
    obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁
    obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂
    simp only [head?_cons, ne_eq, Option.some.injEq] at hhd
    rw [← ne_eq] at hhd
    simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm]
termination_by l₁.length
decreasing_by
  rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁
    _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇
  clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄
    _₂₅ _₂₆ _₂₇
  subst _l₁
  simp

end

end List

[Kyle Miller]

One way to avoid this to prove it without any recursion or induction:

theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p)
    (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧
      t₁.head? ≠ t₂.head? := by
  subst_vars
  rw [prefix_append_right_inj, prefix_append_right_inj]
  rw [commonPrefix_append_append, append_right_eq_self] at hp
  cases t₁ <;> cases t₂
  · simp
  · simp
  · simp
  · simp only [commonPrefix, ite_eq_right_iff, reduceCtorEq, imp_false] at hp
    simp [Ne.symm hp, hp]

[Bulhwi Cha]

Thanks! Then, what should I do when I have to use recursion or induction to prove a theorem like String.splitOnAux_of_valid?