internlm/Lean-Github huggingface dataset:
Theorem: LoVe.SmallStep_skip
Proof state before:
S : Stmt
s t : State
⊢ ¬(Stmt.skip, s) ⇒ (S, t)
Tactic:
intro h
Proof state after:
S : Stmt
s t : State
h : (Stmt.skip, s) ⇒ (S, t)
⊢ False
Theorem: LoVe.SmallStep_skip
Proof state before:
S : Stmt
s t : State
h : (Stmt.skip, s) ⇒ (S, t)
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut ↔ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
apply Iff.intro
Proof state after:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
{ intro hST
  cases hST with
  | seq_step _ S' _ _ s' hS =>
    apply Or.intro_left
    apply Exists.intro S'
    apply Exists.intro s'
    aesop
  | seq_skip =>
    apply Or.intro_right
    aesop }
Proof state after:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
{
  intro hor
  cases hor with
  | inl hex =>
    cases hex with
    | intro S' hex' =>
      cases hex' with
      | intro s' hand =>
        cases hand with
        | intro hS hUt =>
          rw [hUt]
          apply SmallStep.seq_step
          assumption
  | inr hand =>
    cases hand with
    | intro hS hUt =>
      rw [hS, hUt]
      apply SmallStep.seq_skip }
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
intro hST
Proof state after:
case mp
S T : Stmt
s : State
Ut : Stmt × State
hST : (S; T, s) ⇒ Ut
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
hST : (S; T, s) ⇒ Ut
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
cases hST with
| seq_step _ S' _ _ s' hS =>
  apply Or.intro_left
  apply Exists.intro S'
  apply Exists.intro s'
  aesop
| seq_skip =>
  apply Or.intro_right
  aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_step
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)) ∨ S = Stmt.skip ∧ (S'; T, s') = (T, s)
Tactic:
apply Or.intro_left
Proof state after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)
Tactic:
apply Exists.intro S'
Proof state after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S, s) ⇒ (S', t) ∧ (S'; T, s') = (S'; T, t)
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S, s) ⇒ (S', t) ∧ (S'; T, s') = (S'; T, t)
Tactic:
apply Exists.intro s'
Proof state after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s') ∧ (S'; T, s') = (S'; T, s')
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s') ∧ (S'; T, s') = (S'; T, s')
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_skip
T : Stmt
s : State
⊢ (∃ S' t, (Stmt.skip, s) ⇒ (S', t) ∧ (T, s) = (S'; T, t)) ∨ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)
Tactic:
apply Or.intro_right
Proof state after:
case mp.seq_skip.h
T : Stmt
s : State
⊢ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mp.seq_skip.h
T : Stmt
s : State
⊢ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
intro hor
Proof state after:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
hor : (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
hor : (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hor with
| inl hex =>
  cases hex with
  | intro S' hex' =>
    cases hex' with
    | intro s' hand =>
      cases hand with
      | intro hS hUt =>
        rw [hUt]
        apply SmallStep.seq_step
        assumption
| inr hand =>
  cases hand with
  | intro hS hUt =>
    rw [hS, hUt]
    apply SmallStep.seq_skip
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl
S T : Stmt
s : State
Ut : Stmt × State
hex : ∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hex with
| intro S' hex' =>
  cases hex' with
  | intro s' hand =>
    cases hand with
    | intro hS hUt =>
      rw [hUt]
      apply SmallStep.seq_step
      assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
hex' : ∃ t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hex' with
| intro s' hand =>
  cases hand with
  | intro hS hUt =>
    rw [hUt]
    apply SmallStep.seq_step
    assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hand : (S, s) ⇒ (S', s') ∧ Ut = (S'; T, s')
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hand with
| intro hS hUt =>
  rw [hUt]
  apply SmallStep.seq_step
  assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ Ut
Tactic:
rw [hUt]
Proof state after:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ (S'; T, s')
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ (S'; T, s')
Tactic:
apply SmallStep.seq_step
Proof state after:
case mpr.inl.intro.intro.intro.hS
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S, s) ⇒ (S', s')
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inl.intro.intro.intro.hS
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S, s) ⇒ (S', s')
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inr
S T : Stmt
s : State
Ut : Stmt × State
hand : S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hand with
| intro hS hUt =>
  rw [hS, hUt]
  apply SmallStep.seq_skip
Proof state after:
no goals
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
rw [hS, hUt]
Proof state after:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (Stmt.skip; T, s) ⇒ (T, s)
Theorem: LoVe.SmallStep_seq_Iff
Proof state before:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (Stmt.skip; T, s) ⇒ (T, s)
Tactic:
apply SmallStep.seq_skip
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us ↔ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
apply Iff.intro
Proof state after:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
{ intro h
  cases h with
  | if_true _ _ _ _ hB  => aesop
  | if_false _ _ _ _ hB => aesop }
Proof state after:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
{ intro hor
  cases hor with
  | inl hand =>
    cases hand with
    | intro hB hUs =>
      rw [hUs]
      apply SmallStep.if_true
      assumption
  | inr hand =>
    cases hand with
    | intro hB hUs =>
      rw [hUs]
      apply SmallStep.if_false
      assumption }
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
intro h
Proof state after:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
h : (Stmt.ifThenElse B S T, s) ⇒ Us
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
h : (Stmt.ifThenElse B S T, s) ⇒ Us
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
Tactic:
cases h with
| if_true _ _ _ _ hB  => aesop
| if_false _ _ _ _ hB => aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mp.if_true
B : State → Prop
S T : Stmt
s : State
hB : B s
⊢ B s ∧ (S, s) = (S, s) ∨ ¬B s ∧ (S, s) = (T, s)
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mp.if_false
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
⊢ B s ∧ (T, s) = (S, s) ∨ ¬B s ∧ (T, s) = (T, s)
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
intro hor
Proof state after:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hor : B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hor : B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hor with
| inl hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_true
    assumption
| inr hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_false
    assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inl
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hand : B s ∧ Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hand with
| intro hB hUs =>
  rw [hUs]
  apply SmallStep.if_true
  assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
rw [hUs]
Proof state after:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (S, s)
Tactic:
apply SmallStep.if_true
Proof state after:
case mpr.inl.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ B s
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inl.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : B s
hUs : Us = (S, s)
⊢ B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hand : ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
cases hand with
| intro hB hUs =>
  rw [hUs]
  apply SmallStep.if_false
  assumption
Proof state after:
no goals
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
Tactic:
rw [hUs]
Proof state after:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ (T, s)
Tactic:
apply SmallStep.if_false
Proof state after:
case mpr.inr.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ ¬B s
Theorem: LoVe.SmallStep_if_Iff
Proof state before:
case mpr.inr.intro.hcond
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hB : ¬B s
hUs : Us = (T, s)
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip; T, u)
Tactic:
apply RTC.lift (fun Ss ↦ (Prod.fst Ss; T, Prod.snd Ss)) _ h
Proof state after:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ ∀ (a b : Stmt × State), a ⇒ b → (fun Ss => (Ss.fst; T, Ss.snd)) a ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) b
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ ∀ (a b : Stmt × State), a ⇒ b → (fun Ss => (Ss.fst; T, Ss.snd)) a ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) b
Tactic:
intro Ss Ss' hrtc
Proof state after:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
Ss Ss' : Stmt × State
hrtc : Ss ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) Ss ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
Ss Ss' : Stmt × State
hrtc : Ss ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) Ss ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
Tactic:
cases Ss with
| mk S s =>
  cases Ss' with
  | mk S' s' =>
    apply SmallStep.seq_step
    assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
case mk
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
Ss' : Stmt × State
S : Stmt
s : State
hrtc : (S, s) ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) (S, s) ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
Tactic:
cases Ss' with
| mk S' s' =>
  apply SmallStep.seq_step
  assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
case mk.mk
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) (S, s) ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) (S', s')
Tactic:
apply SmallStep.seq_step
Proof state after:
case mk.mk.hS
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ ((S, s).fst, (S, s).snd) ⇒ ((S', s').fst, (S', s').snd)
Theorem: LoVe.RTC_SmallStep_seq
Proof state before:
case mk.mk.hS
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ ((S, s).fst, (S, s).snd) ⇒ ((S', s').fst, (S', s').snd)
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
Ss : Stmt × State
t : State
hS : Ss ⟹ t
⊢ RTC SmallStep Ss (Stmt.skip, t)
Tactic:
induction hS with
| skip => exact RTC.refl
| assign =>
  apply RTC.single
  apply SmallStep.assign
| seq S T s t u hS hT ihS ihT =>
  apply RTC.trans
  { exact RTC_SmallStep_seq ihS }
  { apply RTC.head
    apply SmallStep.seq_skip
    assumption }
| if_true B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_true
    assumption }
  { assumption }
| if_false B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_false
    assumption }
  { assumption }
| while_true B S s t u hB hS hw ihS ihw =>
  apply RTC.head
  { apply SmallStep.whileDo }
  { apply RTC.head
    { apply SmallStep.if_true
      assumption }
    { apply RTC.trans
      { exact RTC_SmallStep_seq ihS }
      { apply RTC.head
        apply SmallStep.seq_skip
        assumption } } }
| while_false B S s hB =>
  apply RTC.tail
  apply RTC.single
  apply SmallStep.whileDo
  apply SmallStep.if_false
  assumption
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case skip
Ss : Stmt × State
t s✝ : State
⊢ RTC SmallStep (Stmt.skip, s✝) (Stmt.skip, s✝)
Tactic:
exact RTC.refl
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case assign
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ RTC SmallStep (Stmt.assign x✝ a✝, s✝) (Stmt.skip, State.update x✝ (a✝ s✝) s✝)
Tactic:
apply RTC.single
Proof state after:
case assign.hab
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : State
⊢ (Stmt.assign x✝ a✝, s✝) ⇒ (Stmt.skip, State.update x✝ (a✝ s✝) s✝)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case assign.hab
Ss : Stmt × State
t : State
x✝ : String
a✝ : State → ℕ
s✝ : 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.RTC_SmallStep_of_BigStep
Proof state before:
case seq
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip, u)
Tactic:
apply RTC.trans
Proof state after:
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b

case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.b (Stmt.skip, u)

case seq.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b

case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.b (Stmt.skip, u)

case seq.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
{ exact RTC_SmallStep_seq ihS }
Proof state after:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, t) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, 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 seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b
Tactic:
exact RTC_SmallStep_seq ihS
Proof state after:
no goals
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (Stmt.skip; T, t) (Stmt.skip, u)
Tactic:
apply RTC.head
Proof state after:
case seq.hbc.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ (Stmt.skip; T, t) ⇒ ?seq.hbc.b

case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.hbc.b (Stmt.skip, u)

case seq.hbc.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case seq.hbc.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ (Stmt.skip; T, t) ⇒ ?seq.hbc.b

case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.hbc.b (Stmt.skip, u)

case seq.hbc.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State
Tactic:
apply SmallStep.seq_skip
Proof state after:
case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (T, t) (Stmt.skip, u)
Theorem: LoVe.RTC_SmallStep_of_BigStep
Proof state before:
case seq.hbc.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (T, t) (Stmt.skip, u)
Tactic:
assumption
Proof state after:
no goals