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

State before:
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us ↔ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
apply Iff.intro
State after:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us

State before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
{ intro h
  cases h with
  | if_true _ _ _ _ hB  => aesop
  | if_false _ _ _ _ hB => aesop }
State after:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us

State before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
{ intro hor
  cases hor with
  | inl hand =>
    cases hand with
    | intro hB hUs =>
      rw [hUs]
      apply SmallStep.if_true
      assumption
  | inr hand =>
    cases hand with
    | intro hB hUs =>
      rw [hUs]
      apply SmallStep.if_false
      assumption }
State after:
no goals

State before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
intro h
State after:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
h : (Stmt.ifThenElse B S T, s) ⇒ Us
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

State before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
h : (Stmt.ifThenElse B S T, s) ⇒ Us
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
cases h with
| if_true _ _ _ _ hB  => aesop
| if_false _ _ _ _ hB => aesop
State after:
no goals

State before:
case mp.if_true
B : State → Prop
S T : Stmt
s : State
hB : B s
⊢ B s ∧ (S, s) = (S, s) ∨ ¬B s ∧ (S, s) = (T, s)
Tactic:
aesop
State after:
no goals

State before:
case mp.if_false
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
⊢ B s ∧ (T, s) = (S, s) ∨ ¬B s ∧ (T, s) = (T, s)
Tactic:
aesop
State after:
no goals

State before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
intro hor
State after:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hor : B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us

State before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hor : B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hor with
| inl hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_true
    assumption
| inr hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_false
    assumption
State after:
no goals

State before:
case mpr.inl
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hand : B s ∧ Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hand with
| intro hB hUs =>
  rw [hUs]
  apply SmallStep.if_true
  assumption
State after:
no goals

State before:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
rw [hUs]
State after:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)

State before:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)
Tactic:
apply SmallStep.if_true
State after:
case mpr.inl.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ B s

State before:
case mpr.inl.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case mpr.inr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hand : ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hand with
| intro hB hUs =>
  rw [hUs]
  apply SmallStep.if_false
  assumption
State after:
no goals

State before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
rw [hUs]
State after:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)

State before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)
Tactic:
apply SmallStep.if_false
State after:
case mpr.inr.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ ¬B s

State before:
case mpr.inr.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ ¬B s
Tactic:
assumption
State after:
no goals