Theorem: LoVe.BigStepEquiv.if_seq_while_skip (LoVe/Labs/Lab6Solution.lean)

State before:
B : State → Prop
S : Stmt
⊢ Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip ~ Stmt.whileDo B S
Tactic:
intro s t
State after:
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t ↔ (Stmt.whileDo B S, s) ⟹ t

State before:
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t ↔ (Stmt.whileDo B S, s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t

case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t

State before:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t

case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hseq =>
    cases hseq with
    | seq _ _ _ u _ hS hT =>
      apply BigStep.while_true <;>
        assumption
  | if_false _ _ _ _ _ hB hskip =>
    cases hskip
    apply BigStep.while_false
    assumption }
State after:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t

State before:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
{ intro hwhile
  cases hwhile with
  | while_true _ _ _ u _ hB hS hw =>
    apply BigStep.if_true
    exact hB
    apply BigStep.seq <;>
      assumption
  | while_false _ _ _ hB =>
    apply BigStep.if_false
    exact hB
    apply BigStep.skip }
State after:
no goals

State before:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t
Tactic:
intro hif
State after:
case mp
B : State → Prop
S : Stmt
s t : State
hif : (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t

State before:
case mp
B : State → Prop
S : Stmt
s t : State
hif : (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hseq =>
  cases hseq with
  | seq _ _ _ u _ hS hT =>
    apply BigStep.while_true <;>
      assumption
| if_false _ _ _ _ _ hB hskip =>
  cases hskip
  apply BigStep.while_false
  assumption
State after:
no goals

State before:
case mp.if_true
B : State → Prop
S : Stmt
s t : State
hB : B s
hseq : (S; Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS hT =>
  apply BigStep.while_true <;>
    assumption
State after:
no goals

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

State before:
case mp.if_false
B : State → Prop
S : Stmt
s t : State
hB : ¬B s
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hskip
State after:
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s

State before:
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s
Tactic:
apply BigStep.while_false
State after:
case mp.if_false.skip.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

State before:
case mp.if_false.skip.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Tactic:
assumption
State after:
no goals

State before:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
intro hwhile
State after:
case mpr
B : State → Prop
S : Stmt
s t : State
hwhile : (Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t

State before:
case mpr
B : State → Prop
S : Stmt
s t : State
hwhile : (Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
cases hwhile with
| while_true _ _ _ u _ hB hS hw =>
  apply BigStep.if_true
  exact hB
  apply BigStep.seq <;>
    assumption
| while_false _ _ _ hB =>
  apply BigStep.if_false
  exact hB
  apply BigStep.skip
State after:
no goals

State before:
case mpr.while_true
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
apply BigStep.if_true
State after:
case mpr.while_true.hcond
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ B s

case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t

State before:
case mpr.while_true.hcond
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ B s

case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t
Tactic:
exact hB
State after:
case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t

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

State before:
case mpr.while_false
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ s
Tactic:
apply BigStep.if_false
State after:
case mpr.while_false.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s

State before:
case mpr.while_false.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Tactic:
exact hB
State after:
case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s

State before:
case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Tactic:
apply BigStep.skip
State after:
no goals