-- Mathlib/Computability/TuringMachine.lean
theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Proof state:
case mk.some.intro.intro
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
b : ?m.147876
c : ?m.148193 b
r : Reaches (TM1.step (tr M)) (?m.148194 b) (?m.148195 b)
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
exact ⟨b, c, TransGen.head' rfl r⟩

Result:
no goals

Proof state:
case H₄
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
l✝ : σ → Λ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (TM2.stepAux (TM2.Stmt.goto l✝) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (TM2.Stmt.goto l✝)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg c₁ c₂
⊢ match TM2.step M c₁ with
  | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
  | none => TM1.step (tr M) c₂ = none

Tactic:
obtain @⟨- | l, v, S, L, hT⟩ := h

Result:
case mk.none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ match TM2.step M { l := none, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

case mk.some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Proof state:
case mk.some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _

Result:
case mk.some.intro.intro
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
b : ?m.147876
c : ?m.148193 b
r : Reaches (TM1.step (tr M)) (?m.148194 b) (?m.148195 b)
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
⊢ ∃ b, ?m.148193 b ∧ Reaches (TM1.step (tr M)) (?m.148194 b) (?m.148195 b)

Proof state:
case mk.none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ match TM2.step M { l := none, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
constructor

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
N : TM2.Stmt Γ Λ σ
⊢ ∃ b, TrCfg (TM2.stepAux N v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal N) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
induction N using stmtStRec generalizing v S L hT with
| H₁ k s q IH => exact tr_respects_aux M hT s @IH
| H₂ a _ IH => exact IH _ hT
| H₃ p q₁ q₂ IH₁ IH₂ =>
  unfold TM2.stepAux trNormal TM1.stepAux
  beta_reduce
  cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
| H₄ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
| H₅ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
⊢ Respects (TM2.step M) (TM1.step (tr M)) TrCfg

Tactic:
intro c₁ c₂ h

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
c₁ : TM2.Cfg Γ Λ σ
c₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h : TrCfg c₁ c₂
⊢ match TM2.step M c₁ with
  | some b₁ => ∃ b₂, TrCfg b₁ b₂ ∧ Reaches₁ (TM1.step (tr M)) c₂ b₂
  | none => TM1.step (tr M) c₂ = none