feat: add String.splitOn_of_valid

[chabulhwi]

String.splitOn_of_valid is the first of the eleven unproved theorems
about strings. I added the following to prove it:

• lemmas about Nat.add and lists
• the file Batteries.Data.List.SplitOnList
• the theorem String.splitOnAux_of_valid

---

This is the third version of #495 and includes #531. The second version is #719.

• depends on: refactor: move theorems about lists from mathlib #756
• depends on: refactor: move Function.id_def from mathlib #755

[chabulhwi]

awaiting-review

[kim-em]

This is doing too many things at once. Can you split out the preliminary steps (upstreaming from Mathlib) as separate PRs?

[chabulhwi]

This is doing too many things at once. Can you split out the preliminary steps (upstreaming from Mathlib) as separate PRs?

@semorrison I've split these commits into separate PRs.

[chabulhwi]

awaiting-review

[chabulhwi]

I resolved merge conflicts.

[chabulhwi]

awaiting-review

[chabulhwi]

@chabulhwi said:

The following three lemmas about lists in Batteries#743 aren't necessary for proving the theorem String.splitOn_of_valid, which is the whole point of this pull request. Should I move these lemmas to a separate PR or just remove them?

import Batteries.Control.ForInStep.Lemmas
import Batteries.Data.List.Basic
import Batteries.Tactic.Init
import Batteries.Tactic.Alias

namespace List

-- NOTE: I need this lemma.
theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l
  | _::_, _ => rfl

theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) :
    [l.head hne] = l := by
  conv => rhs; rw [← head_cons_tail l hne, htl]

theorem singleton_prefix_cons (a) : [a] <+: a :: l :=
  (prefix_cons_inj a).mpr nil_prefix

-- NOTE: I need this lemma.
theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
  intro heq
  simp [heq, nil_prefix] at h

theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α]
    {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧
      l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by
  constructor <;> intro h
  · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
    obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
    simp only [cons_prefix_cons, not_and] at h
    cases Decidable.em (c₁ = c₂)
    · subst c₂
      simp only [forall_const] at h
      let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ :=
        not_prefix_and_not_prefix_symm_iff_exists.mp h
      exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩
    · next hc =>
      exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩
  · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h
    rw [heq₁, heq₂]
    simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm]

end List

---

I moved them to a new PR: #987.