Lean4
theorem pred_ok (q₁ q₂ s v) (c d : List Γ') :
∃ s',
Reaches₁ (TM2.step tr) ⟨some (Λ'.pred q₁ q₂), s, K'.elim (trList v) [] c d⟩
(v.headI.rec ⟨some q₁, s', K'.elim (trList v.tail) [] c d⟩ fun n _ =>
⟨some q₂, s', K'.elim (trList (n :: v.tail)) [] c d⟩) :=
by
rcases v with (_ | ⟨_ | n, v⟩)
· refine ⟨none, TransGen.single ?_⟩
simp
· refine ⟨some Γ'.cons, TransGen.single ?_⟩
simp
refine ⟨none, ?_⟩
simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ, List.tail_cons, List.headI_cons]
rcases (n : Num) with - | a
· simp only [trPosNum, Num.succ', List.singleton_append, List.nil_append]
refine TransGen.head rfl ?_
rw [tr]; simp only [pop', TM2.stepAux]
convert unrev_ok using 2
simp
simp only [Num.succ']
suffices
∀ l₁,
∃ l₁' l₂' s',
List.reverseAux l₁ (trPosNum a) = List.reverseAux l₁' l₂' ∧
Reaches₁ (TM2.step tr) ⟨some (q₁.pred q₂), s, K'.elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d⟩
⟨some (unrev q₂), s', K'.elim (l₂' ++ Γ'.cons :: trList v) l₁' c d⟩
by
obtain ⟨l₁', l₂', s', e, h⟩ := this []
simp only [List.reverseAux] at e
refine h.trans ?_
convert unrev_ok using 2
simp [e, List.reverseAux_eq]
induction a generalizing s with intro l₁
| one =>
refine ⟨Γ'.bit1 :: l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
| bit1 m IH =>
obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
simp
rfl
| bit0 m
IH =>
obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a :: l) ∧ natEnd a = false := by cases m <;> refine ⟨_, _, rfl, rfl⟩
refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide, Option.iget, -natEnd]
rfl
