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

State before:
Ss₀ Ss₁ : Stmt × State
s₂ : State
h₁ : Ss₀ ⇒ Ss₁
⊢ Ss₁ ⟹ s₂ → Ss₀ ⟹ s₂
Tactic:
induction h₁ generalizing s₂ with
| assign x a s               => simp
| seq_step S S' T s s' hS ih => aesop
| seq_skip T s               => simp
| if_true B S T s hB         => aesop
| if_false B S T s hB        => aesop
| whileDo B S s              => aesop
State after:
no goals

State before:
case assign
Ss₀ Ss₁ : Stmt × State
x : String
a : State → ℕ
s s₂ : State
⊢ (Stmt.skip, State.update x (a s) s) ⟹ s₂ → (Stmt.assign x a, s) ⟹ s₂
Tactic:
simp
State after:
no goals

State before:
case seq_step
Ss₀ Ss₁ : Stmt × State
S S' T : Stmt
s s' : State
hS : (S, s) ⇒ (S', s')
ih : ∀ {s₂ : State}, (S', s') ⟹ s₂ → (S, s) ⟹ s₂
s₂ : State
⊢ (S'; T, s') ⟹ s₂ → (S; T, s) ⟹ s₂
Tactic:
aesop
State after:
no goals

State before:
case seq_skip
Ss₀ Ss₁ : Stmt × State
T : Stmt
s s₂ : State
⊢ (T, s) ⟹ s₂ → (Stmt.skip; T, s) ⟹ s₂
Tactic:
simp
State after:
no goals

State before:
case if_true
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : B s
s₂ : State
⊢ (S, s) ⟹ s₂ → (Stmt.ifThenElse B S T, s) ⟹ s₂
Tactic:
aesop
State after:
no goals

State before:
case if_false
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
s₂ : State
⊢ (T, s) ⟹ s₂ → (Stmt.ifThenElse B S T, s) ⟹ s₂
Tactic:
aesop
State after:
no goals

State before:
case whileDo
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S : Stmt
s s₂ : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ s₂ → (Stmt.whileDo B S, s) ⟹ s₂
Tactic:
aesop
State after:
no goals