Theorem: LoVe.GCL.BigStep_assert (LoVe/Labs/Lab6Solution.lean)

State before:
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t ↔ t = s ∧ B s
Tactic:
apply Iff.intro
State after:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s

case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t

State before:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s

case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
{ intro hast
  cases hast
  simp [*] }
State after:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t

State before:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
{ intro hand
  cases hand with
  | intro hts hB =>
    rw [hts]
    apply BigStep.assert
    exact hB }
State after:
no goals

State before:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s
Tactic:
intro hast
State after:
case mp
B : State → Prop
s t : State
hast : (Stmt.assert B, s) ⟹ t
⊢ t = s ∧ B s

State before:
case mp
B : State → Prop
s t : State
hast : (Stmt.assert B, s) ⟹ t
⊢ t = s ∧ B s
Tactic:
cases hast
State after:
case mp.assert
B : State → Prop
s : State
hB✝ : B s
⊢ s = s ∧ B s

State before:
case mp.assert
B : State → Prop
s : State
hB✝ : B s
⊢ s = s ∧ B s
Tactic:
simp [*]
State after:
no goals

State before:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
intro hand
State after:
case mpr
B : State → Prop
s t : State
hand : t = s ∧ B s
⊢ (Stmt.assert B, s) ⟹ t

State before:
case mpr
B : State → Prop
s t : State
hand : t = s ∧ B s
⊢ (Stmt.assert B, s) ⟹ t
Tactic:
cases hand with
| intro hts hB =>
  rw [hts]
  apply BigStep.assert
  exact hB
State after:
no goals

State before:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ t
Tactic:
rw [hts]
State after:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ s

State before:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ s
Tactic:
apply BigStep.assert
State after:
case mpr.intro.hB
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ B s

State before:
case mpr.intro.hB
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ B s
Tactic:
exact hB
State after:
no goals