internlm/Lean-Github huggingface dataset:
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t

case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, ?hbody.t) ⟹ ?t

case hbody.t

⊢ State
Tactic:
{ apply BigStep.skip }
Proof state after:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
{ apply BigStep.assign }
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
apply BigStep.assign
Proof state after:
no goals
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hrest

⊢ (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)) ⟹
    fun x => 0
Tactic:
simp
Proof state after:
case hrest

⊢ (Stmt.whileDo (fun s => s "y" < s "x") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), fun x => 0) ⟹ fun x => 0
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hrest

⊢ (Stmt.whileDo (fun s => s "y" < s "x") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), fun x => 0) ⟹ fun x => 0
Tactic:
apply BigStep.while_false
Proof state after:
case hrest.hcond

⊢ ¬0 < 0
Theorem: LoVe.sillyLoop_from_1_BigStep
Proof state before:
case hrest.hcond

⊢ ¬0 < 0
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
Ss : Stmt × State
l r : State
hl : Ss ⟹ l
hr : Ss ⟹ r
⊢ l = r
Tactic:
induction hl generalizing r with
| skip s =>
  cases hr with
  | skip => rfl
| assign x a s =>
  cases hr with
  | assign => rfl
| seq S T s l₀ l hS hT ihS ihT =>
  cases hr with
  | seq _ _ _ r₀ _ hS' hT' =>
    cases ihS hS' with
    | refl =>
      cases ihT hT' with
      | refl => rfl
| if_true B S T s l hB hS ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => apply ih hS'
  | if_false _ _ _ _ _ hB' hS' => aesop
| if_false B S T s l hB hT ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => aesop
  | if_false _ _ _ _ _ hB' hS' => apply ih hS'
| while_true B S s l₀ l hB hS hw ihS ihw =>
  cases hr with
  | while_true _ _ _ r₀ hB' hB' hS' hw' =>
    cases ihS hS' with
    | refl =>
      cases ihw hw' with
      | refl => rfl
  | while_false _ _ _ hB' => aesop
| while_false B S s hB =>
  cases hr with
  | while_true _ _ _ s' _ hB' hS hw => aesop
  | while_false _ _ _ hB'           => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case skip
Ss : Stmt × State
l s r : State
hr : (Stmt.skip, s) ⟹ r
⊢ s = r
Tactic:
cases hr with
| skip => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case skip.skip
Ss : Stmt × State
l s : State
⊢ s = s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case assign
Ss : Stmt × State
l : State
x : String
a : State → ℕ
s r : State
hr : (Stmt.assign x a, s) ⟹ r
⊢ State.update x (a s) s = r
Tactic:
cases hr with
| assign => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case assign.assign
Ss : Stmt × State
l : State
x : String
a : State → ℕ
s : State
⊢ State.update x (a s) s = State.update x (a s) s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case seq
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r : State
hr : (S; T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| seq _ _ _ r₀ _ hS' hT' =>
  cases ihS hS' with
  | refl =>
    cases ihT hT' with
    | refl => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case seq.seq
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r r₀ : State
hS' : (S, s) ⟹ r₀
hT' : (T, r₀) ⟹ r
⊢ l = r
Tactic:
cases ihS hS' with
| refl =>
  cases ihT hT' with
  | refl => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case seq.seq.refl
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r : State
hS' : (S, s) ⟹ l₀
hT' : (T, l₀) ⟹ r
⊢ l = r
Tactic:
cases ihT hT' with
| refl => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case seq.seq.refl.refl
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
hS' : (S, s) ⟹ l₀
hT' : (T, l₀) ⟹ l
⊢ l = l
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hr : (Stmt.ifThenElse B S T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| if_true _ _ _ _ _ hB' hS'  => apply ih hS'
| if_false _ _ _ _ _ hB' hS' => aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_true.if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ r
⊢ l = r
Tactic:
apply ih hS'
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_true.if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hB' : ¬B s
hS' : (T, s) ⟹ r
⊢ l = r
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hr : (Stmt.ifThenElse B S T, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| if_true _ _ _ _ _ hB' hS'  => aesop
| if_false _ _ _ _ _ hB' hS' => apply ih hS'
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_false.if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ r
⊢ l = r
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case if_false.if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hB' : ¬B s
hS' : (T, s) ⟹ r
⊢ l = r
Tactic:
apply ih hS'
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ l = r
Tactic:
cases hr with
| while_true _ _ _ r₀ hB' hB' hS' hw' =>
  cases ihS hS' with
  | refl =>
    cases ihw hw' with
    | refl => rfl
| while_false _ _ _ hB' => aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_true.while_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r r₀ : State
hB' : B s
hS' : (S, s) ⟹ r₀
hw' : (Stmt.whileDo B S, r₀) ⟹ r
⊢ l = r
Tactic:
cases ihS hS' with
| refl =>
  cases ihw hw' with
  | refl => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_true.while_true.refl
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
r : State
hB' : B s
hS' : (S, s) ⟹ l₀
hw' : (Stmt.whileDo B S, l₀) ⟹ r
⊢ l = r
Tactic:
cases ihw hw' with
| refl => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_true.while_true.refl.refl
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
hB' : B s
hS' : (S, s) ⟹ l₀
hw' : (Stmt.whileDo B S, l₀) ⟹ l
⊢ l = l
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_true.while_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
hB' : ¬B s
⊢ l = s
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_false
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ s = r
Tactic:
cases hr with
| while_true _ _ _ s' _ hB' hS hw => aesop
| while_false _ _ _ hB'           => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_false.while_true
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB : ¬B s
r s' : State
hB' : B s
hS : (S, s) ⟹ s'
hw : (Stmt.whileDo B S, s') ⟹ r
⊢ s = r
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_deterministic
Proof state before:
case while_false.while_false
Ss : Stmt × State
l : State
B : State → Prop
S : Stmt
s : State
hB hB' : ¬B s
⊢ s = s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
s t : State
⊢ (Stmt.skip, s) ⟹ t ↔ t = s
Tactic:
apply Iff.intro
Proof state after:
case mp
s t : State
⊢ (Stmt.skip, s) ⟹ t → t = s

case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mp
s t : State
⊢ (Stmt.skip, s) ⟹ t → t = s

case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | skip => rfl }
Proof state after:
case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  rw [h]
  apply BigStep.skip }
Proof state after:
no goals
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mp
s t : State
⊢ (Stmt.skip, s) ⟹ t → t = s
Tactic:
intro h
Proof state after:
case mp
s t : State
h : (Stmt.skip, s) ⟹ t
⊢ t = s
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mp
s t : State
h : (Stmt.skip, s) ⟹ t
⊢ t = s
Tactic:
cases h with
| skip => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mp.skip
s : State
⊢ s = s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Tactic:
intro h
Proof state after:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ t
Tactic:
rw [h]
Proof state after:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ s
Theorem: LoVe.BigStep_skip_Iff
Proof state before:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ s
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t ↔ t = State.update x (a s) s
Tactic:
apply Iff.intro
Proof state after:
case mp
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t → t = State.update x (a s) s

case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mp
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t → t = State.update x (a s) s

case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | assign => rfl }
Proof state after:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
{ intro h
  rw [h]
  apply BigStep.assign }
Proof state after:
no goals
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mp
x : String
a : State → ℕ
s t : State
⊢ (Stmt.assign x a, s) ⟹ t → t = State.update x (a s) s
Tactic:
intro h
Proof state after:
case mp
x : String
a : State → ℕ
s t : State
h : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mp
x : String
a : State → ℕ
s t : State
h : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s
Tactic:
cases h with
| assign => rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mp.assign
x : String
a : State → ℕ
s : State
⊢ State.update x (a s) s = State.update x (a s) s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
⊢ t = State.update x (a s) s → (Stmt.assign x a, s) ⟹ t
Tactic:
intro h
Proof state after:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Tactic:
rw [h]
Proof state after:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s
Theorem: LoVe.BigStep_assign_Iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
h : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s
Tactic:
apply BigStep.assign
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
apply Iff.intro
Proof state after:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u

case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | seq =>
    apply Exists.intro
    apply And.intro <;>
      assumption }
Proof state after:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
{ intro h
  cases h with
  | intro s' h' =>
    cases h' with
    | intro hS hT =>
      apply BigStep.seq <;>
        assumption }
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s u : State
⊢ (S; T, s) ⟹ u → ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
intro h
Proof state after:
case mp
S T : Stmt
s u : State
h : (S; T, s) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mp
S T : Stmt
s u : State
h : (S; T, s) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
cases h with
| seq =>
  apply Exists.intro
  apply And.intro <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mp.seq
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
Tactic:
apply Exists.intro
Proof state after:
case mp.seq.h
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ (S, s) ⟹ ?mp.seq.w ∧ (T, ?mp.seq.w) ⟹ u

case mp.seq.w
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ State
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mp.seq.h
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ (S, s) ⟹ ?mp.seq.w ∧ (T, ?mp.seq.w) ⟹ u

case mp.seq.w
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ State
Tactic:
apply And.intro <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s u : State
⊢ (∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u) → (S; T, s) ⟹ u
Tactic:
intro h
Proof state after:
case mpr
S T : Stmt
s u : State
h : ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
⊢ (S; T, s) ⟹ u
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mpr
S T : Stmt
s u : State
h : ∃ t, (S, s) ⟹ t ∧ (T, t) ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
cases h with
| intro s' h' =>
  cases h' with
  | intro hS hT =>
    apply BigStep.seq <;>
      assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mpr.intro
S T : Stmt
s u s' : State
h' : (S, s) ⟹ s' ∧ (T, s') ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
cases h' with
| intro hS hT =>
  apply BigStep.seq <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_seq_Iff
Proof state before:
case mpr.intro.intro
S T : Stmt
s u s' : State
hS : (S, s) ⟹ s'
hT : (T, s') ⟹ u
⊢ (S; T, s) ⟹ u
Tactic:
apply BigStep.seq <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
B : State → Prop
S T : Stmt
s t : State
⊢ (Stmt.ifThenElse B S T, s) ⟹ t ↔ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
B : State → Prop
S T : Stmt
s t : State
⊢ (Stmt.ifThenElse B S T, s) ⟹ t → B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t

case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s t : State
⊢ (Stmt.ifThenElse B S T, s) ⟹ t → B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t

case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | if_true _ _ _ _ _ hB hS =>
    apply Or.intro_left
    aesop
  | if_false _ _ _ _ _ hB hT =>
    apply Or.intro_right
    aesop }
Proof state after:
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | inl h =>
    cases h with
    | intro hB hS =>
      apply BigStep.if_true <;>
        assumption
  | inr h =>
    cases h with
    | intro hB hT =>
      apply BigStep.if_false <;>
        assumption }
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s t : State
⊢ (Stmt.ifThenElse B S T, s) ⟹ t → B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
intro h
Proof state after:
case mp
B : State → Prop
S T : Stmt
s t : State
h : (Stmt.ifThenElse B S T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp
B : State → Prop
S T : Stmt
s t : State
h : (Stmt.ifThenElse B S T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
cases h with
| if_true _ _ _ _ _ hB hS =>
  apply Or.intro_left
  aesop
| if_false _ _ _ _ _ hB hT =>
  apply Or.intro_right
  aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp.if_true
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
apply Or.intro_left
Proof state after:
case mp.if_true.h
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp.if_true.h
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp.if_false
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
Tactic:
apply Or.intro_right
Proof state after:
case mp.if_false.h
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ ¬B s ∧ (T, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mp.if_false.h
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ ¬B s ∧ (T, s) ⟹ t
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
intro h
Proof state after:
case mpr
B : State → Prop
S T : Stmt
s t : State
h : B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr
B : State → Prop
S T : Stmt
s t : State
h : B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
cases h with
| inl h =>
  cases h with
  | intro hB hS =>
    apply BigStep.if_true <;>
      assumption
| inr h =>
  cases h with
  | intro hB hT =>
    apply BigStep.if_false <;>
      assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr.inl
B : State → Prop
S T : Stmt
s t : State
h : B s ∧ (S, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
cases h with
| intro hB hS =>
  apply BigStep.if_true <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr.inl.intro
B : State → Prop
S T : Stmt
s t : State
hB : B s
hS : (S, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
apply BigStep.if_true <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr.inr
B : State → Prop
S T : Stmt
s t : State
h : ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
cases h with
| intro hB hT =>
  apply BigStep.if_false <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_if_Iff
Proof state before:
case mpr.inr.intro
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
Tactic:
apply BigStep.if_false <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStep_while_Iff
Proof state before:
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:
apply Iff.intro
Proof state after:
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

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
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

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
  | 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:
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