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

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

case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t

State before:
case mp
B : State → Prop
S T : Stmt
s t : State
⊢ (Stmt.ifThenElse B S T, s) ⟹ t → B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t

case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | if_true _ _ _ _ _ hB hS =>
    apply Or.intro_left
    aesop
  | if_false _ _ _ _ _ hB hT =>
    apply Or.intro_right
    aesop }
State after:
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t

State before:
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | inl h =>
    cases h with
    | intro hB hS =>
      apply BigStep.if_true <;>
        assumption
  | inr h =>
    cases h with
    | intro hB hT =>
      apply BigStep.if_false <;>
        assumption }
State after:
no goals

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

State before:
case mp
B : State → Prop
S T : Stmt
s t : State
h : (Stmt.ifThenElse B S T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
cases h with
| if_true _ _ _ _ _ hB hS =>
  apply Or.intro_left
  aesop
| if_false _ _ _ _ _ hB hT =>
  apply Or.intro_right
  aesop
State after:
no goals

State before:
case mp.if_true
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
apply Or.intro_left
State after:
case mp.if_true.h
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t

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

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

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

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

State before:
case mpr
B : State → Prop
S T : Stmt
s t : State
h : B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
cases h with
| inl h =>
  cases h with
  | intro hB hS =>
    apply BigStep.if_true <;>
      assumption
| inr h =>
  cases h with
  | intro hB hT =>
    apply BigStep.if_false <;>
      assumption
State after:
no goals

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

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

State before:
case mpr.inr
B : State → Prop
S T : Stmt
s t : State
h : ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
cases h with
| intro hB hT =>
  apply BigStep.if_false <;>
    assumption
State after:
no goals

State before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
apply BigStep.if_false <;>
  assumption
State after:
no goals