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

State before:
Ss : Stmt × State
l r : State
hl : Ss ⟹ l
hr : Ss ⟹ r
⊢ l = r
Tactic:
induction hl generalizing r with
| skip s =>
  cases hr with
  | skip => rfl
| assign x a s =>
  cases hr with
  | assign => rfl
| seq S T s l₀ l hS hT ihS ihT =>
  cases hr with
  | seq _ _ _ r₀ _ hS' hT' =>
    cases ihS hS' with
    | refl =>
      cases ihT hT' with
      | refl => rfl
| if_true B S T s l hB hS ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => apply ih hS'
  | if_false _ _ _ _ _ hB' hS' => aesop
| if_false B S T s l hB hT ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => aesop
  | if_false _ _ _ _ _ hB' hS' => apply ih hS'
| while_true B S s l₀ l hB hS hw ihS ihw =>
  cases hr with
  | while_true _ _ _ r₀ hB' hB' hS' hw' =>
    cases ihS hS' with
    | refl =>
      cases ihw hw' with
      | refl => rfl
  | while_false _ _ _ hB' => aesop
| while_false B S s hB =>
  cases hr with
  | while_true _ _ _ s' _ hB' hS hw => aesop
  | while_false _ _ _ hB'           => rfl
State after:
no goals

State before:
case skip
Ss : Stmt × State
l s r : State
hr : (Stmt.skip, s) ⟹ r
⊢ s = r
Tactic:
cases hr with
| skip => rfl
State after:
no goals

State before:
case skip.skip
Ss : Stmt × State
l s : State
⊢ s = s
Tactic:
rfl
State after:
no goals

State before:
case assign
Ss : Stmt × State
l : State
x : String
a : State → ℕ
s r : State
hr : (Stmt.assign x a, s) ⟹ r
⊢ State.update x (a s) s = r
Tactic:
cases hr with
| assign => rfl
State after:
no goals

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

State before:
case seq
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r : State
hr : (S; T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| seq _ _ _ r₀ _ hS' hT' =>
  cases ihS hS' with
  | refl =>
    cases ihT hT' with
    | refl => rfl
State after:
no goals

State before:
case seq.seq
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r r₀ : State
hS' : (S, s) ⟹ r₀
hT' : (T, r₀) ⟹ r
⊢ l = r
Tactic:
cases ihS hS' with
| refl =>
  cases ihT hT' with
  | refl => rfl
State after:
no goals

State before:
case seq.seq.refl
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r : State
hS' : (S, s) ⟹ l₀
hT' : (T, l₀) ⟹ r
⊢ l = r
Tactic:
cases ihT hT' with
| refl => rfl
State after:
no goals

State before:
case seq.seq.refl.refl
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
hS' : (S, s) ⟹ l₀
hT' : (T, l₀) ⟹ l
⊢ l = l
Tactic:
rfl
State after:
no goals

State before:
case if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hr : (Stmt.ifThenElse B S T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| if_true _ _ _ _ _ hB' hS'  => apply ih hS'
| if_false _ _ _ _ _ hB' hS' => aesop
State after:
no goals

State before:
case if_true.if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ r
⊢ l = r
Tactic:
apply ih hS'
State after:
no goals

State before:
case if_true.if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hB' : ¬B s
hS' : (T, s) ⟹ r
⊢ l = r
Tactic:
aesop
State after:
no goals

State before:
case if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hr : (Stmt.ifThenElse B S T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| if_true _ _ _ _ _ hB' hS'  => aesop
| if_false _ _ _ _ _ hB' hS' => apply ih hS'
State after:
no goals

State before:
case if_false.if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ r
⊢ l = r
Tactic:
aesop
State after:
no goals

State before:
case if_false.if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hB' : ¬B s
hS' : (T, s) ⟹ r
⊢ l = r
Tactic:
apply ih hS'
State after:
no goals

State before:
case while_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| while_true _ _ _ r₀ hB' hB' hS' hw' =>
  cases ihS hS' with
  | refl =>
    cases ihw hw' with
    | refl => rfl
| while_false _ _ _ hB' => aesop
State after:
no goals

State before:
case while_true.while_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r r₀ : State
hB' : B s
hS' : (S, s) ⟹ r₀
hw' : (Stmt.whileDo B S, r₀) ⟹ r
⊢ l = r
Tactic:
cases ihS hS' with
| refl =>
  cases ihw hw' with
  | refl => rfl
State after:
no goals

State before:
case while_true.while_true.refl
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ l₀
hw' : (Stmt.whileDo B S, l₀) ⟹ r
⊢ l = r
Tactic:
cases ihw hw' with
| refl => rfl
State after:
no goals

State before:
case while_true.while_true.refl.refl
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
hB' : B s
hS' : (S, s) ⟹ l₀
hw' : (Stmt.whileDo B S, l₀) ⟹ l
⊢ l = l
Tactic:
rfl
State after:
no goals

State before:
case while_true.while_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
hB' : ¬B s
⊢ l = s
Tactic:
aesop
State after:
no goals

State before:
case while_false
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ s = r
Tactic:
cases hr with
| while_true _ _ _ s' _ hB' hS hw => aesop
| while_false _ _ _ hB'           => rfl
State after:
no goals

State before:
case while_false.while_true
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
r s' : State
hB' : B s
hS : (S, s) ⟹ s'
hw : (Stmt.whileDo B S, s') ⟹ r
⊢ s = r
Tactic:
aesop
State after:
no goals

State before:
case while_false.while_false
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB hB' : ¬B s
⊢ s = s
Tactic:
rfl
State after:
no goals