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

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

case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u

State before:
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
{ intro hloop
  cases hloop with
  | loop_base S s =>
    apply Or.inl
    rfl
  | loop_step S s t u hS hl =>
    apply Or.inr
    apply Exists.intro t
    aesop }
State after:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u

State before:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
{ intro hor
  cases hor with
  | inl hsu =>
    rw [hsu]
    apply BigStep.loop_base
  | inr hex =>
    cases hex with
    | intro t hand =>
      cases hand with
      | intro hS hl =>
        apply BigStep.loop_step <;>
          assumption }
State after:
no goals

State before:
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
intro hloop
State after:
case mp
S : Stmt
s u : State
hloop : (Stmt.loop S, s) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

State before:
case mp
S : Stmt
s u : State
hloop : (Stmt.loop S, s) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
cases hloop with
| loop_base S s =>
  apply Or.inl
  rfl
| loop_step S s t u hS hl =>
  apply Or.inr
  apply Exists.intro t
  aesop
State after:
no goals

State before:
case mp.loop_base
S : Stmt
s : State
⊢ s = s ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ s
Tactic:
apply Or.inl
State after:
case mp.loop_base.h
S : Stmt
s : State
⊢ s = s

State before:
case mp.loop_base.h
S : Stmt
s : State
⊢ s = s
Tactic:
rfl
State after:
no goals

State before:
case mp.loop_step
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
apply Or.inr
State after:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

State before:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
apply Exists.intro t
State after:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

State before:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
aesop
State after:
no goals

State before:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
intro hor
State after:
case mpr
S : Stmt
s u : State
hor : s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u

State before:
case mpr
S : Stmt
s u : State
hor : s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
cases hor with
| inl hsu =>
  rw [hsu]
  apply BigStep.loop_base
| inr hex =>
  cases hex with
  | intro t hand =>
    cases hand with
    | intro hS hl =>
      apply BigStep.loop_step <;>
        assumption
State after:
no goals

State before:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
rw [hsu]
State after:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, u) ⟹ u

State before:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, u) ⟹ u
Tactic:
apply BigStep.loop_base
State after:
no goals

State before:
case mpr.inr
S : Stmt
s u : State
hex : ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
cases hex with
| intro t hand =>
  cases hand with
  | intro hS hl =>
    apply BigStep.loop_step <;>
      assumption
State after:
no goals

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

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