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

State before:
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
apply Iff.intro
State after:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u

State before:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | seq =>
    apply Exists.intro
    apply And.intro <;>
      assumption }
State after:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u

State before:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | intro s' h' =>
    cases h' with
    | intro hS hT =>
      apply BigStep.seq <;>
        assumption }
State after:
no goals

State before:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
intro h
State after:
case mp
S T : Stmt
s u : State
h : (S; T, s) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

State before:
case mp
S T : Stmt
s u : State
h : (S; T, s) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
cases h with
| seq =>
  apply Exists.intro
  apply And.intro <;>
    assumption
State after:
no goals

State before:
case mp.seq
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
apply Exists.intro
State after:
case mp.seq.h
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ (S, s) ⟹ ?mp.seq.w ∧ (T, ?mp.seq.w) ⟹ u

case mp.seq.w
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ State

State before:
case mp.seq.h
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ (S, s) ⟹ ?mp.seq.w ∧ (T, ?mp.seq.w) ⟹ u

case mp.seq.w
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ State
Tactic:
apply And.intro <;>
  assumption
State after:
no goals

State before:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
intro h
State after:
case mpr
S T : Stmt
s u : State
h : ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
⊢ (S; T, s) ⟹ u

State before:
case mpr
S T : Stmt
s u : State
h : ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
cases h with
| intro s' h' =>
  cases h' with
  | intro hS hT =>
    apply BigStep.seq <;>
      assumption
State after:
no goals

State before:
case mpr.intro
S T : Stmt
s u s' : State
h' : (S, s) ⟹ s' ∧ (T, s') ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
cases h' with
| intro hS hT =>
  apply BigStep.seq <;>
    assumption
State after:
no goals

State before:
case mpr.intro.intro
S T : Stmt
s u s' : State
hS : (S, s) ⟹ s'
hT : (T, s') ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
apply BigStep.seq <;>
  assumption
State after:
no goals