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

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

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

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

case mpr
S₁ S₂ : Stmt
s t : State
⊢ (∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t) → (S₁; S₂, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq
  apply Exists.intro
  apply And.intro <;>
    assumption }
State after:
case mpr
S₁ S₂ : Stmt
s t : State
⊢ (∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t) → (S₁; S₂, s) ⟹ t

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

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

State before:
case mp
S₁ S₂ : Stmt
s t : State
hseq : (S₁; S₂, s) ⟹ t
⊢ ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
Tactic:
cases hseq
State after:
case mp.seq
S₁ S₂ : Stmt
s t t✝ : State
hS✝ : (S₁, s) ⟹ t✝
hT✝ : (S₂, t✝) ⟹ t
⊢ ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t

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

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

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

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

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

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

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

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