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

State before:
S : Stmt
s : State
⊢ (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
Tactic:
induction S with
| skip =>
  simp
  intros T t hstep
  cases hstep
| assign x a =>
  simp
  apply Exists.intro Stmt.skip
  apply Exists.intro (s[x ↦ a s])
  apply SmallStep.assign
| seq S T ihS ihT =>
  simp
  cases Classical.em (S = Stmt.skip) with
  | inl h =>
    rw [h]
    apply Exists.intro T
    apply Exists.intro s
    apply SmallStep.seq_skip
  | inr h =>
    simp [h] at ihS
    cases ihS with
    | intro S' hS₀ =>
      cases hS₀ with
      | intro s' hS =>
        apply Exists.intro (S'; T)
        apply Exists.intro s'
        apply SmallStep.seq_step
        assumption
| ifThenElse B S T ihS ihT =>
  simp
  cases Classical.em (B s) with
  | inl h =>
    apply Exists.intro S
    apply Exists.intro s
    apply SmallStep.if_true
    assumption
  | inr h =>
    apply Exists.intro T
    apply Exists.intro s
    apply SmallStep.if_false
    assumption
| whileDo B S ih =>
  simp
  apply Exists.intro
    (Stmt.ifThenElse B (S; Stmt.whileDo B S)
       Stmt.skip)
  apply Exists.intro s
  apply SmallStep.whileDo
State after:
no goals

State before:
case skip
s : State
⊢ (¬∃ T t, (Stmt.skip, s) ⇒ (T, t)) ↔ Stmt.skip = Stmt.skip
Tactic:
simp
State after:
case skip
s : State
⊢ ∀ (x : Stmt) (x_1 : State), ¬(Stmt.skip, s) ⇒ (x, x_1)

State before:
case skip
s : State
⊢ ∀ (x : Stmt) (x_1 : State), ¬(Stmt.skip, s) ⇒ (x, x_1)
Tactic:
intros T t hstep
State after:
case skip
s : State
T : Stmt
t : State
hstep : (Stmt.skip, s) ⇒ (T, t)
⊢ False

State before:
case skip
s : State
T : Stmt
t : State
hstep : (Stmt.skip, s) ⇒ (T, t)
⊢ False
Tactic:
cases hstep
State after:
no goals

State before:
case assign
s : State
x : String
a : State → ℕ
⊢ (¬∃ T t, (Stmt.assign x a, s) ⇒ (T, t)) ↔ Stmt.assign x a = Stmt.skip
Tactic:
simp
State after:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ T t, (Stmt.assign x a, s) ⇒ (T, t)

State before:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ T t, (Stmt.assign x a, s) ⇒ (T, t)
Tactic:
apply Exists.intro Stmt.skip
State after:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ t, (Stmt.assign x a, s) ⇒ (Stmt.skip, t)

State before:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ t, (Stmt.assign x a, s) ⇒ (Stmt.skip, t)
Tactic:
apply Exists.intro (s[x ↦ a s])
State after:
case assign
s : State
x : String
a : State → ℕ
⊢ (Stmt.assign x a, s) ⇒ (Stmt.skip, State.update x (a s) s)

State before:
case assign
s : State
x : String
a : State → ℕ
⊢ (Stmt.assign x a, s) ⇒ (Stmt.skip, State.update x (a s) s)
Tactic:
apply SmallStep.assign
State after:
no goals

State before:
case seq
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ (¬∃ T_1 t, (S; T, s) ⇒ (T_1, t)) ↔ S; T = Stmt.skip
Tactic:
simp
State after:
case seq
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)

State before:
case seq
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
cases Classical.em (S = Stmt.skip) with
| inl h =>
  rw [h]
  apply Exists.intro T
  apply Exists.intro s
  apply SmallStep.seq_skip
| inr h =>
  simp [h] at ihS
  cases ihS with
  | intro S' hS₀ =>
    cases hS₀ with
    | intro s' hS =>
      apply Exists.intro (S'; T)
      apply Exists.intro s'
      apply SmallStep.seq_step
      assumption
State after:
no goals

State before:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
rw [h]
State after:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ ∃ T_1 t, (Stmt.skip; T, s) ⇒ (T_1, t)

State before:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ ∃ T_1 t, (Stmt.skip; T, s) ⇒ (T_1, t)
Tactic:
apply Exists.intro T
State after:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ ∃ t, (Stmt.skip; T, s) ⇒ (T, t)

State before:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ ∃ t, (Stmt.skip; T, s) ⇒ (T, t)
Tactic:
apply Exists.intro s
State after:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ (Stmt.skip; T, s) ⇒ (T, s)

State before:
case seq.inl
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : S = Stmt.skip
⊢ (Stmt.skip; T, s) ⇒ (T, s)
Tactic:
apply SmallStep.seq_skip
State after:
no goals

State before:
case seq.inr
s : State
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
simp [h] at ihS
State after:
case seq.inr
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
ihS : ∃ T t, (S, s) ⇒ (T, t)
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)

State before:
case seq.inr
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
ihS : ∃ T t, (S, s) ⇒ (T, t)
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
cases ihS with
| intro S' hS₀ =>
  cases hS₀ with
  | intro s' hS =>
    apply Exists.intro (S'; T)
    apply Exists.intro s'
    apply SmallStep.seq_step
    assumption
State after:
no goals

State before:
case seq.inr.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
hS₀ : ∃ t, (S, s) ⇒ (S', t)
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
cases hS₀ with
| intro s' hS =>
  apply Exists.intro (S'; T)
  apply Exists.intro s'
  apply SmallStep.seq_step
  assumption
State after:
no goals

State before:
case seq.inr.intro.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ T_1 t, (S; T, s) ⇒ (T_1, t)
Tactic:
apply Exists.intro (S'; T)
State after:
case seq.inr.intro.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S; T, s) ⇒ (S'; T, t)

State before:
case seq.inr.intro.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S; T, s) ⇒ (S'; T, t)
Tactic:
apply Exists.intro s'
State after:
case seq.inr.intro.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S; T, s) ⇒ (S'; T, s')

State before:
case seq.inr.intro.intro
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S; T, s) ⇒ (S'; T, s')
Tactic:
apply SmallStep.seq_step
State after:
case seq.inr.intro.intro.hS
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s')

State before:
case seq.inr.intro.intro.hS
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s')
Tactic:
assumption
State after:
no goals

State before:
case ifThenElse
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ (¬∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)) ↔ Stmt.ifThenElse B S T = Stmt.skip
Tactic:
simp
State after:
case ifThenElse
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)

State before:
case ifThenElse
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)
Tactic:
cases Classical.em (B s) with
| inl h =>
  apply Exists.intro S
  apply Exists.intro s
  apply SmallStep.if_true
  assumption
| inr h =>
  apply Exists.intro T
  apply Exists.intro s
  apply SmallStep.if_false
  assumption
State after:
no goals

State before:
case ifThenElse.inl
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)
Tactic:
apply Exists.intro S
State after:
case ifThenElse.inl
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ ∃ t, (Stmt.ifThenElse B S T, s) ⇒ (S, t)

State before:
case ifThenElse.inl
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ ∃ t, (Stmt.ifThenElse B S T, s) ⇒ (S, t)
Tactic:
apply Exists.intro s
State after:
case ifThenElse.inl
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)

State before:
case ifThenElse.inl
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)
Tactic:
apply SmallStep.if_true
State after:
case ifThenElse.inl.hcond
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ B s

State before:
case ifThenElse.inl.hcond
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : B s
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case ifThenElse.inr
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)
Tactic:
apply Exists.intro T
State after:
case ifThenElse.inr
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ ∃ t, (Stmt.ifThenElse B S T, s) ⇒ (T, t)

State before:
case ifThenElse.inr
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ ∃ t, (Stmt.ifThenElse B S T, s) ⇒ (T, t)
Tactic:
apply Exists.intro s
State after:
case ifThenElse.inr
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)

State before:
case ifThenElse.inr
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)
Tactic:
apply SmallStep.if_false
State after:
case ifThenElse.inr.hcond
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ ¬B s

State before:
case ifThenElse.inr.hcond
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬B s
⊢ ¬B s
Tactic:
assumption
State after:
no goals

State before:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ (¬∃ T t, (Stmt.whileDo B S, s) ⇒ (T, t)) ↔ Stmt.whileDo B S = Stmt.skip
Tactic:
simp
State after:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ ∃ T t, (Stmt.whileDo B S, s) ⇒ (T, t)

State before:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ ∃ T t, (Stmt.whileDo B S, s) ⇒ (T, t)
Tactic:
apply Exists.intro
  (Stmt.ifThenElse B (S; Stmt.whileDo B S)
     Stmt.skip)
State after:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ ∃ t, (Stmt.whileDo B S, s) ⇒ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, t)

State before:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ ∃ t, (Stmt.whileDo B S, s) ⇒ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, t)
Tactic:
apply Exists.intro s
State after:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ (Stmt.whileDo B S, s) ⇒ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s)

State before:
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ (Stmt.whileDo B S, s) ⇒ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s)
Tactic:
apply SmallStep.whileDo
State after:
no goals