English
A simplified form of a mem-mem lemma for options in elements.
Русский
Упрощенная форма леммы для опций в элементах.
LaTeX
$$$ Eq (Option.instMembership.mem b a) (Eq b (Option.some a)) $$$
Lean4
theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg :=
by
intro c₁ c₂ h
obtain @⟨- | l, v, S, L, hT⟩ := h; · constructor
rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _
· exact ⟨b, c, TransGen.head' rfl r⟩
simp only [tr]
generalize M l = N
induction N using stmtStRec generalizing v S L hT with
| run k s q IH => exact tr_respects_aux M hT s @IH
| load a _ IH => exact IH _ hT
| branch p q₁ q₂ IH₁ IH₂ =>
unfold TM2.stepAux trNormal TM1.stepAux
beta_reduce
cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
| goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
| halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
