internlm/Lean-Github huggingface dataset:
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
Proof state after:
case hbc.hbc.hbc.hbc.hbc.hbc.hab

⊢ (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep ?hbc.hbc.hbc.hbc.hbc.hbc.b (Stmt.skip, fun x => 0)

case hbc.hbc.hbc.hbc.hbc.hbc.b

⊢ Stmt × State
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hab

⊢ (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep ?hbc.hbc.hbc.hbc.hbc.hbc.b (Stmt.skip, fun x => 0)

case hbc.hbc.hbc.hbc.hbc.hbc.b

⊢ Stmt × State
Tactic:
{ apply SmallStep.if_false
  simp }
Proof state after:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Tactic:
{ simp
  apply RTC.refl }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hab

⊢ (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; Stmt.assign "x" fun s => s "x" - 1);
          Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1))
        Stmt.skip,
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.hbc.hbc.b
Tactic:
apply SmallStep.if_false
Proof state after:
case hbc.hbc.hbc.hbc.hbc.hbc.hab.hcond

⊢ ¬State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "x" >
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "y"
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hab.hcond

⊢ ¬State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "x" >
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0) "y"
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
Tactic:
simp
Proof state after:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, fun x => 0) (Stmt.skip, fun x => 0)
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep (Stmt.skip, fun x => 0) (Stmt.skip, fun x => 0)
Tactic:
apply RTC.refl
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof state before:
case skip
s : State
⊢ (¬∃ T t, (Stmt.skip, s) ⇒ (T, t)) ↔ Stmt.skip = Stmt.skip
Tactic:
simp
Proof state after:
case skip
s : State
⊢ ∀ (x : Stmt) (x_1 : State), ¬(Stmt.skip, s) ⇒ (x, x_1)
Theorem: LoVe.SmallStep_final
Proof state before:
case skip
s : State
⊢ ∀ (x : Stmt) (x_1 : State), ¬(Stmt.skip, s) ⇒ (x, x_1)
Tactic:
intros T t hstep
Proof state after:
case skip
s : State
T : Stmt
t : State
hstep : (Stmt.skip, s) ⇒ (T, t)
⊢ False
Theorem: LoVe.SmallStep_final
Proof state before:
case skip
s : State
T : Stmt
t : State
hstep : (Stmt.skip, s) ⇒ (T, t)
⊢ False
Tactic:
cases hstep
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ T t, (Stmt.assign x a, s) ⇒ (T, t)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
case assign
s : State
x : String
a : State → ℕ
⊢ ∃ t, (Stmt.assign x a, s) ⇒ (Stmt.skip, t)
Theorem: LoVe.SmallStep_final
Proof 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])
Proof state after:
case assign
s : State
x : String
a : State → ℕ
⊢ (Stmt.assign x a, s) ⇒ (Stmt.skip, State.update x (a s) s)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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]
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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)
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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'
Proof 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')
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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')
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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)
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof 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)
Theorem: LoVe.SmallStep_final
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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₁
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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₂
Proof 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₂)
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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₁
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof state before:
case seq_skip.seq_skip
Ss Ll : Stmt × State
T : Stmt
s : State
⊢ (T, s) = (T, s)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals
Theorem: LoVe.SmallStep_deterministic
Proof 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
Proof state after:
no goals