Theorem: LoVe.BigStep_assign_Iff (LoVe/Lectures/LoVe09_OperationalSemantics_Demo.lean)

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

case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t

State before:
case mp
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t → t = State.update x (a s) s

case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | assign => rfl }
State after:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t

State before:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
{ intro h
  rw [h]
  apply BigStep.assign }
State after:
no goals

State before:
case mp
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t → t = State.update x (a s) s
Tactic:
intro h
State after:
case mp
x : String
a : State → ℕ
s t : State
h : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s

State before:
case mp
x : String
a : State → ℕ
s t : State
h : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s
Tactic:
cases h with
| assign => rfl
State after:
no goals

State before:
case mp.assign
x : String
a : State → ℕ
s : State
⊢ State.update x (a s) s = State.update x (a s) s
Tactic:
rfl
State after:
no goals

State before:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
intro h
State after:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t

State before:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Tactic:
rw [h]
State after:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s

State before:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s
Tactic:
apply BigStep.assign
State after:
no goals