internlm/Lean-Github huggingface dataset:
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (Stmt.ifThenElse B S T, s) (Stmt.skip, t)
Tactic:
apply RTC.head
Proof state after:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b

case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_true.b (Stmt.skip, t)

case if_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b

case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_true.b (Stmt.skip, t)

case if_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ Stmt × State
Tactic:
{ apply SmallStep.if_true
  assumption }
Proof state after:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)
Tactic:
{ assumption }
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b
Tactic:
apply SmallStep.if_true
Proof state after:
case if_true.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ B s
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (Stmt.ifThenElse B S T, s) (Stmt.skip, t)
Tactic:
apply RTC.head
Proof state after:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b

case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_false.b (Stmt.skip, t)

case if_false.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b

case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_false.b (Stmt.skip, t)

case if_false.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ Stmt × State
Tactic:
{ apply SmallStep.if_false
  assumption }
Proof state after:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
Tactic:
{ assumption }
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b
Tactic:
apply SmallStep.if_false
Proof state after:
case if_false.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ ¬B s
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
apply RTC.head
Proof state after:
case while_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.whileDo B S, s) ⇒ ?while_true.b

case while_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.b (Stmt.skip, u)

case while_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.whileDo B S, s) ⇒ ?while_true.b

case while_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.b (Stmt.skip, u)

case while_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
{ apply SmallStep.whileDo }
Proof state after:
case while_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)
Tactic:
{ apply RTC.head
  { apply SmallStep.if_true
    assumption }
  { apply RTC.trans
    { exact RTC_SmallStep_seq ihS }
    { apply RTC.head
      apply SmallStep.seq_skip
      assumption } } }
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.whileDo B S, s) ⇒ ?while_true.b
Tactic:
apply SmallStep.whileDo
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) (Stmt.skip, u)
Tactic:
apply RTC.head
Proof state after:
case while_true.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b

case while_true.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.b (Stmt.skip, u)

case while_true.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b

case while_true.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.b (Stmt.skip, u)

case while_true.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
{ apply SmallStep.if_true
  assumption }
Proof state after:
case while_true.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
{ apply RTC.trans
  { exact RTC_SmallStep_seq ihS }
  { apply RTC.head
    apply SmallStep.seq_skip
    assumption } }
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ ?while_true.hbc.b
Tactic:
apply SmallStep.if_true
Proof state after:
case while_true.hbc.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ B s
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hab.hcond
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) (Stmt.skip, u)
Tactic:
apply RTC.trans
Proof state after:
case while_true.hbc.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b

case while_true.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b

case while_true.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
{ exact RTC_SmallStep_seq ihS }
Proof state after:
case while_true.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
{ apply RTC.head
  apply SmallStep.seq_skip
  assumption }
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; Stmt.whileDo B S, s) ?while_true.hbc.hbc.b
Tactic:
exact RTC_SmallStep_seq ihS
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
apply RTC.head
Proof state after:
case while_true.hbc.hbc.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.skip; Stmt.whileDo B S, t) ⇒ ?while_true.hbc.hbc.hbc.b

case while_true.hbc.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hbc.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ (Stmt.skip; Stmt.whileDo B S, t) ⇒ ?while_true.hbc.hbc.hbc.b

case while_true.hbc.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep ?while_true.hbc.hbc.hbc.b (Stmt.skip, u)

case while_true.hbc.hbc.hbc.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
apply SmallStep.seq_skip
Proof state after:
case while_true.hbc.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_true.hbc.hbc.hbc.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihw : RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.whileDo B S, t) (Stmt.skip, u)
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_false
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ RTC SmallStep (Stmt.whileDo B S, s) (Stmt.skip, s)
Tactic:
apply RTC.tail
Proof state after:
case while_false.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ RTC SmallStep (Stmt.whileDo B S, s) ?while_false.b

case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ?while_false.b ⇒ (Stmt.skip, s)

case while_false.b
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_false.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ RTC SmallStep (Stmt.whileDo B S, s) ?while_false.b

case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ?while_false.b ⇒ (Stmt.skip, s)

case while_false.b
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ Stmt × State
Tactic:
apply RTC.single
Proof state after:
case while_false.hab.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⇒ ?while_false.b

case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ?while_false.b ⇒ (Stmt.skip, s)

case while_false.b
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_false.hab.hab
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⇒ ?while_false.b

case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ?while_false.b ⇒ (Stmt.skip, s)

case while_false.b
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ Stmt × State
Tactic:
apply SmallStep.whileDo
Proof state after:
case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ (Stmt.skip, s)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_false.hbc
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⇒ (Stmt.skip, s)
Tactic:
apply SmallStep.if_false
Proof state after:
case while_false.hbc.hcond
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case while_false.hbc.hcond
Ss : Stmt × State
t : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof state before:
case seq_skip
Ss₀ Ss₁ : Stmt × State
T : Stmt
s s₂ : State
⊢ (T, s) ⟹ s₂ → (Stmt.skip; T, s) ⟹ s₂
Tactic:
simp
Proof state after:
no goals