internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | inl hex =>
    cases hex with
    | intro t h =>
      cases h with
      | intro hB h =>
        cases h with
        | intro hS hwhile =>
          apply BigStep.while_true <;>
            assumption
  | inr h =>
    cases h with
    | intro hB hus =>
      rw [hus]
      apply BigStep.while_false
      assumption}
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp
B : State → Prop
S : Stmt
s u : State
⊢ (Stmt.whileDo B S, s) ⟹ u → (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
intro h
Proof state after:
case mp
B : State → Prop
S : Stmt
s u : State
h : (Stmt.whileDo B S, s) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp
B : State → Prop
S : Stmt
s u : State
h : (Stmt.whileDo B S, s) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
cases h with
| while_true _ _ _ t _ hB hS hw =>
  apply Or.intro_left
  apply Exists.intro t
  aesop
| while_false _ _ _ hB =>
  apply Or.intro_right
  aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp.while_true
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
Tactic:
apply Or.intro_left
Proof state after:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
apply Exists.intro t
Proof state after:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp.while_false
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ s) ∨ ¬B s ∧ s = s
Tactic:
apply Or.intro_right
Proof state after:
case mp.while_false.h
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s ∧ s = s
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mp.while_false.h
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s ∧ s = s
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr
B : State → Prop
S : Stmt
s u : State
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s → (Stmt.whileDo B S, s) ⟹ u
Tactic:
intro h
Proof state after:
case mpr
B : State → Prop
S : Stmt
s u : State
h : (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr
B : State → Prop
S : Stmt
s u : State
h : (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| inl hex =>
  cases hex with
  | intro t h =>
    cases h with
    | intro hB h =>
      cases h with
      | intro hS hwhile =>
        apply BigStep.while_true <;>
          assumption
| inr h =>
  cases h with
  | intro hB hus =>
    rw [hus]
    apply BigStep.while_false
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inl
B : State → Prop
S : Stmt
s u : State
hex : ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases hex with
| intro t h =>
  cases h with
  | intro hB h =>
    cases h with
    | intro hS hwhile =>
      apply BigStep.while_true <;>
        assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inl.intro
B : State → Prop
S : Stmt
s u t : State
h : B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hB h =>
  cases h with
  | intro hS hwhile =>
    apply BigStep.while_true <;>
      assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inl.intro.intro
B : State → Prop
S : Stmt
s u t : State
hB : B s
h : (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hS hwhile =>
  apply BigStep.while_true <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inl.intro.intro.intro
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hwhile : (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
apply BigStep.while_true <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inr
B : State → Prop
S : Stmt
s u : State
h : ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
cases h with
| intro hB hus =>
  rw [hus]
  apply BigStep.while_false
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
Tactic:
rw [hus]
Proof state after:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ s
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inr.intro
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ (Stmt.whileDo B S, s) ⟹ s
Tactic:
apply BigStep.while_false
Proof state after:
case mpr.inr.intro.hcond
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ ¬B s
Theorem: LoVe.BigStep_while_Iff
Proof state before:
case mpr.inr.intro.hcond
B : State → Prop
S : Stmt
s u : State
hB : ¬B s
hus : u = s
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_true_Iff
Proof state before:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (Stmt.whileDo B S, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
rw [BigStep_while_Iff]
Proof state after:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Theorem: LoVe.BigStep_while_true_Iff
Proof state before:
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
Tactic:
simp [hcond]
Proof state after:
no goals
Theorem: LoVe.BigStep_while_false_Iff
Proof state before:
B : State → Prop
S : Stmt
s t : State
hcond : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ t ↔ t = s
Tactic:
rw [BigStep_while_Iff]
Proof state after:
B : State → Prop
S : Stmt
s t : State
hcond : ¬B s
⊢ (∃ t_1, B s ∧ (S, s) ⟹ t_1 ∧ (Stmt.whileDo B S, t_1) ⟹ t) ∨ ¬B s ∧ t = s ↔ t = s
Theorem: LoVe.BigStep_while_false_Iff
Proof state before:
B : State → Prop
S : Stmt
s t : State
hcond : ¬B s
⊢ (∃ t_1, B s ∧ (S, s) ⟹ t_1 ∧ (Stmt.whileDo B S, t_1) ⟹ t) ∨ ¬B s ∧ t = s ↔ t = s
Tactic:
simp [hcond]
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
⊢ RTC SmallStep (sillyLoop, State.update "x" 1 fun x => 0) (Stmt.skip, fun x => 0)
Tactic:
rw [sillyLoop]
Proof state after:
⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
Proof state after:
case hab

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

case hbc

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

case b

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

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

case hbc

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

case b

⊢ Stmt × State
Tactic:
{ apply SmallStep.whileDo }
Proof state after:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.if_true
    simp }
  { apply RTC.head
    { apply SmallStep.seq_step
      apply SmallStep.seq_skip }
    { apply RTC.head
      { apply SmallStep.seq_step
        apply SmallStep.assign }
      { apply RTC.head
        { apply SmallStep.seq_skip }
        { apply RTC.head
          { apply SmallStep.whileDo }
          { apply RTC.head
            { apply SmallStep.if_false
              simp }
            { simp
              apply RTC.refl } } } } } } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hab

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⇒
    ?b
Tactic:
apply SmallStep.whileDo
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case 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" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
Proof state after:
case 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" 1 fun x => 0) ⇒
    ?hbc.b

case hbc.hbc

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

case hbc.b

⊢ Stmt × State
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case 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" 1 fun x => 0) ⇒
    ?hbc.b

case hbc.hbc

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

case hbc.b

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

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

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.seq_step
    apply SmallStep.seq_skip }
  { apply RTC.head
    { apply SmallStep.seq_step
      apply SmallStep.assign }
    { apply RTC.head
      { apply SmallStep.seq_skip }
      { apply RTC.head
        { apply SmallStep.whileDo }
        { apply RTC.head
          { apply SmallStep.if_false
            simp }
          { simp
            apply RTC.refl } } } } } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case 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" 1 fun x => 0) ⇒
    ?hbc.b
Tactic:
apply SmallStep.if_true
Proof state after:
case hbc.hab.hcond

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

⊢ State.update "x" 1 (fun x => 0) "x" > 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

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
Proof state after:
case hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b

case hbc.hbc.hbc

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

case hbc.hbc.b

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

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b

case hbc.hbc.hbc

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

case hbc.hbc.b

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

⊢ RTC SmallStep
    ((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),
      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

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
{ apply RTC.head
  { apply SmallStep.seq_step
    apply SmallStep.assign }
  { apply RTC.head
    { apply SmallStep.seq_skip }
    { apply RTC.head
      { apply SmallStep.whileDo }
      { apply RTC.head
        { apply SmallStep.if_false
          simp }
        { simp
          apply RTC.refl } } } } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.b
Tactic:
apply SmallStep.seq_step
Proof state after:
case hbc.hbc.hab.hS

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hab.S', ?hbc.hbc.hab.s')

case hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hab.s'

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

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hab.S', ?hbc.hbc.hab.s')

case hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hab.s'

⊢ State
Tactic:
apply SmallStep.seq_skip
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc

⊢ RTC SmallStep
    ((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),
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
Tactic:
apply RTC.head
Proof state after:
case hbc.hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.b

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

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b

case hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.b

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

⊢ RTC SmallStep
    (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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

⊢ RTC SmallStep
    (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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
  { apply SmallStep.seq_skip }
  { apply RTC.head
    { apply SmallStep.whileDo }
    { apply RTC.head
      { apply SmallStep.if_false
        simp }
      { simp
        apply RTC.refl } } } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hab

⊢ ((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),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b
Tactic:
apply SmallStep.seq_step
Proof state after:
case hbc.hbc.hbc.hab.hS

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hbc.hab.S', ?hbc.hbc.hbc.hab.s')

case hbc.hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hbc.hab.s'

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

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hbc.hab.S', ?hbc.hbc.hbc.hab.s')

case hbc.hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hbc.hab.s'

⊢ State
Tactic:
apply SmallStep.assign
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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.hab

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

case hbc.hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.hbc.b

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

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

case hbc.hbc.hbc.hbc.hbc

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

case hbc.hbc.hbc.hbc.b

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

⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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

⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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
  { apply SmallStep.whileDo }
  { apply RTC.head
    { apply SmallStep.if_false
      simp }
    { simp
      apply RTC.refl } } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hab

⊢ (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⇒
    ?hbc.hbc.hbc.hbc.b
Tactic:
apply SmallStep.seq_skip
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      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.hab

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

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

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

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

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

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

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

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

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

⊢ Stmt × State
Tactic:
{ apply SmallStep.whileDo }
Proof state after:
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)
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
  { apply SmallStep.if_false
    simp }
  { simp
    apply RTC.refl } }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_SmallStep
Proof state before:
case hbc.hbc.hbc.hbc.hbc.hab

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