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

State before:
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t ↔ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t

case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t

State before:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t

case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
{ intro hchoice
  cases hchoice with
  | choice _ _ _ i hless hbody =>
    apply Exists.intro i
    apply Exists.intro hless
    assumption }
State after:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t

State before:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
{ intro hex
  cases hex with
  | intro i hex =>
    cases hex with
    | intro hless hstep =>
    apply BigStep.choice <;>
      assumption }
State after:
no goals

State before:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
intro hchoice
State after:
case mp
Ss : List Stmt
s t : State
hchoice : (Stmt.choice Ss, s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t

State before:
case mp
Ss : List Stmt
s t : State
hchoice : (Stmt.choice Ss, s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
cases hchoice with
| choice _ _ _ i hless hbody =>
  apply Exists.intro i
  apply Exists.intro hless
  assumption
State after:
no goals

State before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
apply Exists.intro i
State after:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ hless, (Ss[i], s) ⟹ t

State before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ hless, (Ss[i], s) ⟹ t
Tactic:
apply Exists.intro hless
State after:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ (Ss[i], s) ⟹ t

State before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ (Ss[i], s) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
intro hex
State after:
case mpr
Ss : List Stmt
s t : State
hex : ∃ i hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t

State before:
case mpr
Ss : List Stmt
s t : State
hex : ∃ i hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
cases hex with
| intro i hex =>
  cases hex with
  | intro hless hstep =>
  apply BigStep.choice <;>
    assumption
State after:
no goals

State before:
case mpr.intro
Ss : List Stmt
s t : State
i : ℕ
hex : ∃ hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
cases hex with
| intro hless hstep =>
apply BigStep.choice <;>
  assumption
State after:
no goals

State before:
case mpr.intro.intro
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hstep : (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
apply BigStep.choice <;>
  assumption
State after:
no goals