internlm/Lean-Github huggingface dataset:
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
exact hab
Proof state after:
case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.left
Proof state after:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop
Theorem: LoVe.ForwardProofs.And_swap_tactical
Proof state before:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop
Tactic:
exact hab
Proof state after:
no goals
Theorem: LoVe.reverse_append
Proof state before:
α : Type
ys : List α
⊢ reverse ([] ++ ys) = reverse ys ++ reverse []
Tactic:
simp [reverse]
Proof state after:
no goals
Theorem: LoVe.reverse_append
Proof state before:
α : Type
x : α
xs ys : List α
⊢ reverse (x :: xs ++ ys) = reverse ys ++ reverse (x :: xs)
Tactic:
simp [reverse, reverse_append xs]
Proof state after:
no goals
Theorem: LoVe.reverse_append_tactical
Proof state before:
α : Type
xs ys : List α
⊢ reverse (xs ++ ys) = reverse ys ++ reverse xs
Tactic:
induction xs with
| nil           => simp [reverse]
| cons x xs' ih => simp [reverse, ih]
Proof state after:
no goals
Theorem: LoVe.reverse_append_tactical
Proof state before:
case nil
α : Type
ys : List α
⊢ reverse ([] ++ ys) = reverse ys ++ reverse []
Tactic:
simp [reverse]
Proof state after:
no goals
Theorem: LoVe.reverse_append_tactical
Proof state before:
case cons
α : Type
ys : List α
x : α
xs' : List α
ih : reverse (xs' ++ ys) = reverse ys ++ reverse xs'
⊢ reverse (x :: xs' ++ ys) = reverse ys ++ reverse (x :: xs')
Tactic:
simp [reverse, ih]
Proof state after:
no goals
Theorem: LoVe.reverse_reverse
Proof state before:
α : Type
⊢ reverse (reverse []) = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.reverse_reverse
Proof state before:
α : Type
x : α
xs : List α
⊢ reverse (reverse (x :: xs)) = x :: xs
Tactic:
simp [reverse, reverse_append, reverse_reverse xs]
Proof state after:
no goals
Theorem: LoVe.about_Impl
Proof state before:
⊢ ∀ (a b : Prop), ¬a ∨ b → a → b
Tactic:
intros a b hor ha
Proof state after:
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b
Theorem: LoVe.about_Impl
Proof state before:
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b
Tactic:
apply Or.elim hor
Proof state after:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b

case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Theorem: LoVe.about_Impl
Proof state before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b

case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
{ intro hna
  apply False.elim
  apply hna
  exact ha }
Proof state after:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Theorem: LoVe.about_Impl
Proof state before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
{ intro hb
  exact hb }
Proof state after:
no goals
Theorem: LoVe.about_Impl
Proof state before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b
Tactic:
intro hna
Proof state after:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ b
Theorem: LoVe.about_Impl
Proof state before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ b
Tactic:
apply False.elim
Proof state after:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ False
Theorem: LoVe.about_Impl
Proof state before:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ False
Tactic:
apply hna
Proof state after:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ a
Theorem: LoVe.about_Impl
Proof state before:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.about_Impl
Proof state before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
intro hb
Proof state after:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
hb : b
⊢ b
Theorem: LoVe.about_Impl
Proof state before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
hb : b
⊢ b
Tactic:
exact hb
Proof state after:
no goals
Theorem: LoVe.GCL.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.GCL.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 hasn
  cases hasn
  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.GCL.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 heq
  rw [heq]
  apply BigStep.assign }
Proof state after:
no goals
Theorem: LoVe.GCL.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 hasn
Proof state after:
case mp
x : String
a : State → ℕ
s t : State
hasn : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s
Theorem: LoVe.GCL.BigStep_assign_iff
Proof state before:
case mp
x : String
a : State → ℕ
s t : State
hasn : (Stmt.assign x a, s) ⟹ t
⊢ t = State.update x (a s) s
Tactic:
cases hasn
Proof state after:
case mp.assign
x : String
a : State → ℕ
s : State
⊢ State.update x (a s) s = State.update x (a s) s
Theorem: LoVe.GCL.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.GCL.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 heq
Proof state after:
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Theorem: LoVe.GCL.BigStep_assign_iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ t
Tactic:
rw [heq]
Proof state after:
case mpr
x : String
a : State → ℕ
s t : State
heq : t = State.update x (a s) s
⊢ (Stmt.assign x a, s) ⟹ State.update x (a s) s
Theorem: LoVe.GCL.BigStep_assign_iff
Proof state before:
case mpr
x : String
a : State → ℕ
s t : State
heq : 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.GCL.BigStep_assert
Proof state before:
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t ↔ t = s ∧ B s
Tactic:
apply Iff.intro
Proof state after:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s

case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s

case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
{ intro hast
  cases hast
  simp [*] }
Proof state after:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
{ intro hand
  cases hand with
  | intro hts hB =>
    rw [hts]
    apply BigStep.assert
    exact hB }
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s
Tactic:
intro hast
Proof state after:
case mp
B : State → Prop
s t : State
hast : (Stmt.assert B, s) ⟹ t
⊢ t = s ∧ B s
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mp
B : State → Prop
s t : State
hast : (Stmt.assert B, s) ⟹ t
⊢ t = s ∧ B s
Tactic:
cases hast
Proof state after:
case mp.assert
B : State → Prop
s : State
hB✝ : B s
⊢ s = s ∧ B s
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mp.assert
B : State → Prop
s : State
hB✝ : B s
⊢ s = s ∧ B s
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
Tactic:
intro hand
Proof state after:
case mpr
B : State → Prop
s t : State
hand : t = s ∧ B s
⊢ (Stmt.assert B, s) ⟹ t
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr
B : State → Prop
s t : State
hand : t = s ∧ B s
⊢ (Stmt.assert B, s) ⟹ t
Tactic:
cases hand with
| intro hts hB =>
  rw [hts]
  apply BigStep.assert
  exact hB
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ t
Tactic:
rw [hts]
Proof state after:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ s
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr.intro
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ (Stmt.assert B, s) ⟹ s
Tactic:
apply BigStep.assert
Proof state after:
case mpr.intro.hB
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ B s
Theorem: LoVe.GCL.BigStep_assert
Proof state before:
case mpr.intro.hB
B : State → Prop
s t : State
hts : t = s
hB : B s
⊢ B s
Tactic:
exact hB
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
S₁ S₂ : Stmt
s t : State
⊢ (S₁; S₂, s) ⟹ t ↔ ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
S₁ S₂ : Stmt
s t : State
⊢ (S₁; S₂, s) ⟹ t → ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t

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

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

case mp.seq.w
S₁ S₂ : Stmt
s t t✝ : State
hS✝ : (S₁, s) ⟹ t✝
hT✝ : (S₂, t✝) ⟹ t
⊢ State
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
case mp.seq.h
S₁ S₂ : Stmt
s t t✝ : State
hS✝ : (S₁, s) ⟹ t✝
hT✝ : (S₂, t✝) ⟹ t
⊢ (S₁, s) ⟹ ?mp.seq.w ∧ (S₂, ?mp.seq.w) ⟹ t

case mp.seq.w
S₁ S₂ : Stmt
s t t✝ : State
hS✝ : (S₁, s) ⟹ t✝
hT✝ : (S₂, t✝) ⟹ t
⊢ State
Tactic:
apply And.intro <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
case mpr
S₁ S₂ : Stmt
s t : State
⊢ (∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t) → (S₁; S₂, s) ⟹ t
Tactic:
intro hseq
Proof state after:
case mpr
S₁ S₂ : Stmt
s t : State
hseq : ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
⊢ (S₁; S₂, s) ⟹ t
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
case mpr
S₁ S₂ : Stmt
s t : State
hseq : ∃ u, (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
⊢ (S₁; S₂, s) ⟹ t
Tactic:
cases hseq with
| intro u hand =>
  cases hand with
  | intro hS₁ hS₂ =>
    apply BigStep.seq <;>
      assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
case mpr.intro
S₁ S₂ : Stmt
s t u : State
hand : (S₁, s) ⟹ u ∧ (S₂, u) ⟹ t
⊢ (S₁; S₂, s) ⟹ t
Tactic:
cases hand with
| intro hS₁ hS₂ =>
  apply BigStep.seq <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_seq_iff
Proof state before:
case mpr.intro.intro
S₁ S₂ : Stmt
s t u : State
hS₁ : (S₁, s) ⟹ u
hS₂ : (S₂, u) ⟹ t
⊢ (S₁; S₂, s) ⟹ t
Tactic:
apply BigStep.seq <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u ↔ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
apply Iff.intro
Proof state after:
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
{ intro hloop
  cases hloop with
  | loop_base S s =>
    apply Or.inl
    rfl
  | loop_step S s t u hS hl =>
    apply Or.inr
    apply Exists.intro t
    aesop }
Proof state after:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
{ intro hor
  cases hor with
  | inl hsu =>
    rw [hsu]
    apply BigStep.loop_base
  | inr hex =>
    cases hex with
    | intro t hand =>
      cases hand with
      | intro hS hl =>
        apply BigStep.loop_step <;>
          assumption }
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
intro hloop
Proof state after:
case mp
S : Stmt
s u : State
hloop : (Stmt.loop S, s) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp
S : Stmt
s u : State
hloop : (Stmt.loop S, s) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
cases hloop with
| loop_base S s =>
  apply Or.inl
  rfl
| loop_step S s t u hS hl =>
  apply Or.inr
  apply Exists.intro t
  aesop
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp.loop_base
S : Stmt
s : State
⊢ s = s ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ s
Tactic:
apply Or.inl
Proof state after:
case mp.loop_base.h
S : Stmt
s : State
⊢ s = s
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp.loop_base.h
S : Stmt
s : State
⊢ s = s
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp.loop_step
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
apply Or.inr
Proof state after:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
apply Exists.intro t
Proof state after:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u
Tactic:
intro hor
Proof state after:
case mpr
S : Stmt
s u : State
hor : s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr
S : Stmt
s u : State
hor : s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
cases hor with
| inl hsu =>
  rw [hsu]
  apply BigStep.loop_base
| inr hex =>
  cases hex with
  | intro t hand =>
    cases hand with
    | intro hS hl =>
      apply BigStep.loop_step <;>
        assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
rw [hsu]
Proof state after:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, u) ⟹ u
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr.inl
S : Stmt
s u : State
hsu : s = u
⊢ (Stmt.loop S, u) ⟹ u
Tactic:
apply BigStep.loop_base
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr.inr
S : Stmt
s u : State
hex : ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
cases hex with
| intro t hand =>
  cases hand with
  | intro hS hl =>
    apply BigStep.loop_step <;>
      assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr.inr.intro
S : Stmt
s u t : State
hand : (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
cases hand with
| intro hS hl =>
  apply BigStep.loop_step <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_loop
Proof state before:
case mpr.inr.intro.intro
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (Stmt.loop S, s) ⟹ u
Tactic:
apply BigStep.loop_step <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t ↔ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t

case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t

case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
{ intro hchoice
  cases hchoice with
  | choice _ _ _ i hless hbody =>
    apply Exists.intro i
    apply Exists.intro hless
    assumption }
Proof state after:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
{ intro hex
  cases hex with
  | intro i hex =>
    cases hex with
    | intro hless hstep =>
    apply BigStep.choice <;>
      assumption }
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp
Ss : List Stmt
s t : State
⊢ (Stmt.choice Ss, s) ⟹ t → ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
intro hchoice
Proof state after:
case mp
Ss : List Stmt
s t : State
hchoice : (Stmt.choice Ss, s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp
Ss : List Stmt
s t : State
hchoice : (Stmt.choice Ss, s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
cases hchoice with
| choice _ _ _ i hless hbody =>
  apply Exists.intro i
  apply Exists.intro hless
  assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ i hless, (Ss[i], s) ⟹ t
Tactic:
apply Exists.intro i
Proof state after:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ hless, (Ss[i], s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ ∃ hless, (Ss[i], s) ⟹ t
Tactic:
apply Exists.intro hless
Proof state after:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ (Ss[i], s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mp.choice
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hbody : (Ss[i], s) ⟹ t
⊢ (Ss[i], s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mpr
Ss : List Stmt
s t : State
⊢ (∃ i hless, (Ss[i], s) ⟹ t) → (Stmt.choice Ss, s) ⟹ t
Tactic:
intro hex
Proof state after:
case mpr
Ss : List Stmt
s t : State
hex : ∃ i hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mpr
Ss : List Stmt
s t : State
hex : ∃ i hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
cases hex with
| intro i hex =>
  cases hex with
  | intro hless hstep =>
  apply BigStep.choice <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mpr.intro
Ss : List Stmt
s t : State
i : ℕ
hex : ∃ hless, (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
cases hex with
| intro hless hstep =>
apply BigStep.choice <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.GCL.BigStep_choice
Proof state before:
case mpr.intro.intro
Ss : List Stmt
s t : State
i : ℕ
hless : i < List.length Ss
hstep : (Ss[i], s) ⟹ t
⊢ (Stmt.choice Ss, s) ⟹ t
Tactic:
apply BigStep.choice <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.refl
Proof state before:
S : Stmt
s t : State
⊢ (S, s) ⟹ t ↔ (S, s) ⟹ t
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
x : String
⊢ (Stmt.assign x fun s => s x) ~ Stmt.skip
Tactic:
intro s t
Proof state after:
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t ↔ (Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t ↔ (Stmt.skip, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t

case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t

case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
{ intro hasn
  cases hasn
  simp [*] }
Proof state after:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
{ intro hskip
  cases hskip
  simp [*] }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t
Tactic:
intro hasn
Proof state after:
case mp
x : String
s t : State
hasn : (Stmt.assign x fun s => s x, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mp
x : String
s t : State
hasn : (Stmt.assign x fun s => s x, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ t
Tactic:
cases hasn
Proof state after:
case mp.assign
x : String
s : State
⊢ (Stmt.skip, s) ⟹ State.update x ((fun s => s x) s) s
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mp.assign
x : String
s : State
⊢ (Stmt.skip, s) ⟹ State.update x ((fun s => s x) s) s
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
intro hskip
Proof state after:
case mpr
x : String
s t : State
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.assign x fun s => s x, s) ⟹ t