English
A simplification of move₂_ok showing component-wise equality of option memberships and updates.
Русский
Упрощение move₂_ok, показывающее поэлементную эквивалентность обновлений иMembership.
LaTeX
$$$\\text{move\\_2\\_ok\\_simp} : \\; \\text{Eq}(Option.mem b a, Option.some a)$$$
Lean4
theorem move₂_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂) (h₂ : S rev = [])
(e : splitAtPred p (S k₁) = (L₁, o, L₂)) :
Reaches₁ (TM2.step tr) ⟨some (move₂ p k₁ k₂ q), s, S⟩
⟨some q, none, update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂)⟩ :=
by
refine (move_ok h₁.1 e).trans (TransGen.head rfl ?_)
simp only [TM2.step, Option.mem_def, Option.elim]
cases o <;> simp only <;> rw [tr] <;> simp only [id, TM2.stepAux, Option.isSome, cond_true, cond_false]
· convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2
simp only [Function.update_comm h₁.1, Function.update_idem]
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]
simp only [Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1, Function.update_of_ne h₁.1.symm,
List.reverseAux_eq, h₂, Function.update_self, List.append_nil, List.reverse_reverse]
· convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2
simp only [h₂, Function.update_comm h₁.1, List.reverseAux_eq, Function.update_self, List.append_nil,
Function.update_idem]
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]
simp only [Function.update_of_ne h₁.1.symm, Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1,
Function.update_self, List.reverse_reverse]
