Theorem: LoVe.BigStepEquiv.skip_assign_id (LoVe/Labs/Lab6Solution.lean)

State before:
x : String
⊢ (Stmt.assign x fun s => s x) ~ Stmt.skip
Tactic:
intro s t
State after:
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t ↔ (Stmt.skip, s) ⟹ t

State before:
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t ↔ (Stmt.skip, s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t

case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t

State before:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t

case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
{ intro hasn
  cases hasn
  simp [*] }
State after:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t

State before:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
{ intro hskip
  cases hskip
  simp [*] }
State after:
no goals

State before:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t
Tactic:
intro hasn
State after:
case mp
x : String
s t : State
hasn : (Stmt.assign x fun s => s x, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ t

State before:
case mp
x : String
s t : State
hasn : (Stmt.assign x fun s => s x, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ t
Tactic:
cases hasn
State after:
case mp.assign
x : String
s : State
⊢ (Stmt.skip, s) ⟹ State.update x ((fun s => s x) s) s

State before:
case mp.assign
x : String
s : State
⊢ (Stmt.skip, s) ⟹ State.update x ((fun s => s x) s) s
Tactic:
simp [*]
State after:
no goals

State before:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
intro hskip
State after:
case mpr
x : String
s t : State
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.assign x fun s => s x, s) ⟹ t

State before:
case mpr
x : String
s t : State
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
cases hskip
State after:
case mpr.skip
x : String
s : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ s

State before:
case mpr.skip
x : String
s : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ s
Tactic:
simp [*]
State after:
no goals