English
Red L (L1 ++ L2) holds iff there exist L3, L4 with L = L3 ++ L4 and Red L3 L1 and Red L4 L2.
Русский
Редукция Red L (L1 ++ L2) эквивалентна существованию L3,L4 с L = L3 ++ L4 и Red L3 L1 и Red L4 L2.
LaTeX
$$$Red(L, L_1 \!++\! L_2) \iff \exists L_3 \exists L_4, L = L_3 ++ L_4 \land Red L_3 L_1 \land Red L_4 L_2$$$
Lean4
@[to_additive]
theorem to_append_iff : Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂ :=
Iff.intro
(by
generalize eq : L₁ ++ L₂ = L₁₂
intro h
induction h generalizing L₁ L₂ with
| refl => exact ⟨_, _, eq.symm, by rfl, by rfl⟩
| tail hLL' h ih =>
obtain @⟨s, e, a, b⟩ := h
rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
· have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) = L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
· have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ = s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩)
fun ⟨_, _, Eq, h₃, h₄⟩ => Eq.symm ▸ append_append h₃ h₄
