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

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

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

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

case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | while_true _ _ _ t _ hB hS hw =>
    apply Or.intro_left
    apply Exists.intro t
    aesop
  | while_false _ _ _ hB =>
    apply Or.intro_right
    aesop }
State after:
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u

State before:
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | inl hex =>
    cases hex with
    | intro t h =>
      cases h with
      | intro hB h =>
        cases h with
        | intro hS hwhile =>
          apply BigStep.while_true <;>
            assumption
  | inr h =>
    cases h with
    | intro hB hus =>
      rw [hus]
      apply BigStep.while_false
      assumption}
State after:
no goals

State before:
case mp
B : State → Prop
S : Stmt
s u : State
⊢ (Stmt.whileDo B S, s) ⟹ u → (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
intro h
State after:
case mp
B : State → Prop
S : Stmt
s u : State
h : (Stmt.whileDo B S, s) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s

State before:
case mp
B : State → Prop
S : Stmt
s u : State
h : (Stmt.whileDo B S, s) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
cases h with
| while_true _ _ _ t _ hB hS hw =>
  apply Or.intro_left
  apply Exists.intro t
  aesop
| while_false _ _ _ hB =>
  apply Or.intro_right
  aesop
State after:
no goals

State before:
case mp.while_true
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
apply Or.intro_left
State after:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u

State before:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
apply Exists.intro t
State after:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u

State before:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
aesop
State after:
no goals

State before:
case mp.while_false
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ s) ∨ ¬B s ∧ s = s
Tactic:
apply Or.intro_right
State after:
case mp.while_false.h
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s ∧ s = s

State before:
case mp.while_false.h
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s ∧ s = s
Tactic:
aesop
State after:
no goals

State before:
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
Tactic:
intro h
State after:
case mpr
B : State → Prop
S : Stmt
s u : State
h : (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u

State before:
case mpr
B : State → Prop
S : Stmt
s u : State
h : (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| inl hex =>
  cases hex with
  | intro t h =>
    cases h with
    | intro hB h =>
      cases h with
      | intro hS hwhile =>
        apply BigStep.while_true <;>
          assumption
| inr h =>
  cases h with
  | intro hB hus =>
    rw [hus]
    apply BigStep.while_false
    assumption
State after:
no goals

State before:
case mpr.inl
B : State → Prop
S : Stmt
s u : State
hex : ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases hex with
| intro t h =>
  cases h with
  | intro hB h =>
    cases h with
    | intro hS hwhile =>
      apply BigStep.while_true <;>
        assumption
State after:
no goals

State before:
case mpr.inl.intro
B : State → Prop
S : Stmt
s u t : State
h : B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hB h =>
  cases h with
  | intro hS hwhile =>
    apply BigStep.while_true <;>
      assumption
State after:
no goals

State before:
case mpr.inl.intro.intro
B : State → Prop
S : Stmt
s u t : State
hB : B s
h : (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hS hwhile =>
  apply BigStep.while_true <;>
    assumption
State after:
no goals

State before:
case mpr.inl.intro.intro.intro
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hwhile : (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
apply BigStep.while_true <;>
  assumption
State after:
no goals

State before:
case mpr.inr
B : State → Prop
S : Stmt
s u : State
h : ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hB hus =>
  rw [hus]
  apply BigStep.while_false
  assumption
State after:
no goals

State before:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
rw [hus]
State after:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ s

State before:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ s
Tactic:
apply BigStep.while_false
State after:
case mpr.inr.intro.hcond
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ ¬B s

State before:
case mpr.inr.intro.hcond
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ ¬B s
Tactic:
assumption
State after:
no goals