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

State before:
Ss Ll Rr : Stmt × State
hl : Ss ⇒ Ll
hr : Ss ⇒ Rr
⊢ Ll = Rr
Tactic:
induction hl generalizing Rr with
| assign x a s =>
  cases hr with
  | assign _ _ _ => rfl
| seq_step S S₁ T s s₁ hS₁ ih =>
  cases hr with
  | seq_step S S₂ _ _ s₂ hS₂ =>
    have hSs₁₂ :=
      ih hS₂
    aesop
  | seq_skip => cases hS₁
| seq_skip T s =>
  cases hr with
  | seq_step _ S _ _ s' hskip => cases hskip
  | seq_skip                  => rfl
| if_true B S T s hB =>
  cases hr with
  | if_true  => rfl
  | if_false => aesop
| if_false B S T s hB =>
  cases hr with
  | if_true  => aesop
  | if_false => rfl
| whileDo B S s =>
  cases hr with
  | whileDo => rfl
State after:
no goals

State before:
case assign
Ss Ll : Stmt × State
x : String
a : State → ℕ
s : State
Rr : Stmt × State
hr : (Stmt.assign x a, s) ⇒ Rr
⊢ (Stmt.skip, State.update x (a s) s) = Rr
Tactic:
cases hr with
| assign _ _ _ => rfl
State after:
no goals

State before:
case assign.assign
Ss Ll : Stmt × State
x : String
a : State → ℕ
s : State
⊢ (Stmt.skip, State.update x (a s) s) = (Stmt.skip, State.update x (a s) s)
Tactic:
rfl
State after:
no goals

State before:
case seq_step
Ss Ll : Stmt × State
S S₁ T : Stmt
s s₁ : State
hS₁ : (S, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (S, s) ⇒ Rr → (S₁, s₁) = Rr
Rr : Stmt × State
hr : (S; T, s) ⇒ Rr
⊢ (S₁; T, s₁) = Rr
Tactic:
cases hr with
| seq_step S S₂ _ _ s₂ hS₂ =>
  have hSs₁₂ :=
    ih hS₂
  aesop
| seq_skip => cases hS₁
State after:
no goals

State before:
case seq_step.seq_step
Ss Ll : Stmt × State
S S₁ T : Stmt
s s₁ : State
hS₁ : (S, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (S, s) ⇒ Rr → (S₁, s₁) = Rr
S₂ : Stmt
s₂ : State
hS₂ : (S, s) ⇒ (S₂, s₂)
⊢ (S₁; T, s₁) = (S₂; T, s₂)
Tactic:
have hSs₁₂ :=
  ih hS₂
State after:
case seq_step.seq_step
Ss Ll : Stmt × State
S S₁ T : Stmt
s s₁ : State
hS₁ : (S, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (S, s) ⇒ Rr → (S₁, s₁) = Rr
S₂ : Stmt
s₂ : State
hS₂ : (S, s) ⇒ (S₂, s₂)
hSs₁₂ : (S₁, s₁) = (S₂, s₂)
⊢ (S₁; T, s₁) = (S₂; T, s₂)

State before:
case seq_step.seq_step
Ss Ll : Stmt × State
S S₁ T : Stmt
s s₁ : State
hS₁ : (S, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (S, s) ⇒ Rr → (S₁, s₁) = Rr
S₂ : Stmt
s₂ : State
hS₂ : (S, s) ⇒ (S₂, s₂)
hSs₁₂ : (S₁, s₁) = (S₂, s₂)
⊢ (S₁; T, s₁) = (S₂; T, s₂)
Tactic:
aesop
State after:
no goals

State before:
case seq_step.seq_skip
Ss Ll : Stmt × State
S₁ T : Stmt
s s₁ : State
hS₁ : (Stmt.skip, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (Stmt.skip, s) ⇒ Rr → (S₁, s₁) = Rr
⊢ (S₁; T, s₁) = (T, s)
Tactic:
cases hS₁
State after:
no goals

State before:
case seq_skip
Ss Ll : Stmt × State
T : Stmt
s : State
Rr : Stmt × State
hr : (Stmt.skip; T, s) ⇒ Rr
⊢ (T, s) = Rr
Tactic:
cases hr with
| seq_step _ S _ _ s' hskip => cases hskip
| seq_skip                  => rfl
State after:
no goals

State before:
case seq_skip.seq_step
Ss Ll : Stmt × State
T : Stmt
s : State
S : Stmt
s' : State
hskip : (Stmt.skip, s) ⇒ (S, s')
⊢ (T, s) = (S; T, s')
Tactic:
cases hskip
State after:
no goals

State before:
case seq_skip.seq_skip
Ss Ll : Stmt × State
T : Stmt
s : State
⊢ (T, s) = (T, s)
Tactic:
rfl
State after:
no goals

State before:
case if_true
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : B s
Rr : Stmt × State
hr : (Stmt.ifThenElse B S T, s) ⇒ Rr
⊢ (S, s) = Rr
Tactic:
cases hr with
| if_true  => rfl
| if_false => aesop
State after:
no goals

State before:
case if_true.if_true
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB hcond✝ : B s
⊢ (S, s) = (S, s)
Tactic:
rfl
State after:
no goals

State before:
case if_true.if_false
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : B s
hcond✝ : ¬B s
⊢ (S, s) = (T, s)
Tactic:
aesop
State after:
no goals

State before:
case if_false
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
Rr : Stmt × State
hr : (Stmt.ifThenElse B S T, s) ⇒ Rr
⊢ (T, s) = Rr
Tactic:
cases hr with
| if_true  => aesop
| if_false => rfl
State after:
no goals

State before:
case if_false.if_true
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
hcond✝ : B s
⊢ (T, s) = (S, s)
Tactic:
aesop
State after:
no goals

State before:
case if_false.if_false
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB hcond✝ : ¬B s
⊢ (T, s) = (T, s)
Tactic:
rfl
State after:
no goals

State before:
case whileDo
Ss Ll : Stmt × State
B : State → Prop
S : Stmt
s : State
Rr : Stmt × State
hr : (Stmt.whileDo B S, s) ⇒ Rr
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) = Rr
Tactic:
cases hr with
| whileDo => rfl
State after:
no goals

State before:
case whileDo.whileDo
Ss Ll : Stmt × State
B : State → Prop
S : Stmt
s : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) = (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s)
Tactic:
rfl
State after:
no goals