Theorem: LoVe.GCL.BigStep_assign_iff (LoVe/Labs/Lab6Solution.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 hasn
  cases hasn
  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 heq
  rw [heq]
  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 hasn
State after:
case mp
x : String
a : State → ℕ
s t : State
hasn : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s

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

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 heq
State after:
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t

State before:
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Tactic:
rw [heq]
State after:
case mpr
x : String
a : State → ℕ
s t : State
heq : 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
heq : 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