English
A technical equality describing the evaluation of splitAtPred under equalities of the inputs and outputs, used in proving invariants of TM encodings.
Русский
Техническое равенство, описывающее поведение splitAtPred при равенствах входов/выходов, используемое при доказательстве инвариантов кодирования TM.
LaTeX
$$$\\text{splitAtPred } p\\ L = (L_1, o, L_2)$ при определённых предпосылках; точное выражение длинное и техническое.$$
Lean4
theorem splitAtPred_eq {α} (p : α → Bool) :
∀ L l₁ o l₂,
(∀ x ∈ l₁, p x = false) →
Option.elim' (L = l₁ ∧ l₂ = []) (fun a => p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
| [], _, none, _, _, ⟨rfl, rfl⟩ => rfl
| [], l₁, some o, l₂, _, ⟨_, h₃⟩ => by simp at h₃
| a :: L, l₁, o, l₂, h₁, h₂ => by
rw [splitAtPred]
have IH := splitAtPred_eq p L
rcases o with - | o
· rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨⟨⟩, rfl⟩
rw [h₁ a (List.Mem.head _), cond, IH L none [] _ ⟨rfl, rfl⟩]
exact fun x h => h₁ x (List.Mem.tail _ h)
· rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨h₂, ⟨⟩⟩
· rw [h₂, cond]
rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩] <;> try rfl
exact fun x h => h₁ x (List.Mem.tail _ h)
