internlm/Lean-Github huggingface dataset:
Theorem: A3
Proof state before:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    (∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y) →
      (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M a w x → evaluate M x Y
Tactic:
intro W M w hyp
Proof state after:
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M a w x → evaluate M x Y
Theorem: A3
Proof state before:
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M a w x → evaluate M x Y
Tactic:
constructor
Proof state after:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ ∀ (v : W), relate M a w v → evaluate M v X

case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ ∀ (x : W), relate M a w x → evaluate M x Y
Theorem: A3
Proof state before:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ ∀ (v : W), relate M a w v → evaluate M v X
Tactic:
intro v
Proof state after:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
v : W
⊢ relate M a w v → evaluate M v X
Theorem: A3
Proof state before:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
v : W
⊢ relate M a w v → evaluate M v X
Tactic:
specialize hyp v
Proof state after:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w v : W
hyp : relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ relate M a w v → evaluate M v X
Theorem: A3
Proof state before:
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w v : W
hyp : relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ relate M a w v → evaluate M v X
Tactic:
tauto
Proof state after:
no goals
Theorem: A3
Proof state before:
case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ ∀ (x : W), relate M a w x → evaluate M x Y
Tactic:
intro v
Proof state after:
case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
v : W
⊢ relate M a w v → evaluate M v Y
Theorem: A3
Proof state before:
case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
v : W
⊢ relate M a w v → evaluate M v Y
Tactic:
specialize hyp v
Proof state after:
case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w v : W
hyp : relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ relate M a w v → evaluate M v Y
Theorem: A3
Proof state before:
case right
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w v : W
hyp : relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ relate M a w v → evaluate M v Y
Tactic:
tauto
Proof state after:
no goals
Theorem: A4
Proof state before:
a b : Program
p : ℕ
⊢ tautology ((~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p))⋀(~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p)))
Tactic:
unfold tautology evaluate
Proof state after:
a b : Program
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Theorem: A4
Proof state before:
a b : Program
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Tactic:
intro W M w
Proof state after:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Theorem: A4
Proof state before:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Tactic:
simp
Proof state after:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ (∀ (x x_1 : W), relate M a w x_1 → relate M b x_1 x → M.val x p) →
    ∀ (x : W), relate M a w x → ∀ (x_1 : W), relate M b x x_1 → M.val x_1 p
Theorem: A4
Proof state before:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ (∀ (x x_1 : W), relate M a w x_1 → relate M b x_1 x → M.val x p) →
    ∀ (x : W), relate M a w x → ∀ (x_1 : W), relate M b x x_1 → M.val x_1 p
Tactic:
tauto
Proof state after:
no goals
Theorem: A5
Proof state before:
a b : Program
X : Formula
⊢ tautology ((~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))⋀(~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X)))
Tactic:
unfold tautology evaluate
Proof state after:
a b : Program
X : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X)) ∧ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Theorem: A5
Proof state before:
a b : Program
X : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X)) ∧ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Tactic:
intro W M w
Proof state after:
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X)) ∧ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Theorem: A5
Proof state before:
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X)) ∧ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Tactic:
constructor
Proof state after:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))

case right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Theorem: A5
Proof state before:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))
Tactic:
by_contra hyp
Proof state after:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
hyp : ¬evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))
⊢ False
Theorem: A5
Proof state before:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
hyp : ¬evaluate M w (~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))
⊢ False
Tactic:
simp at *
Proof state after:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
hyp :
  (∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X) ∧
    ((∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X)
⊢ False
Theorem: A5
Proof state before:
case left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
hyp :
  (∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X) ∧
    ((∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X)
⊢ False
Tactic:
cases' hyp with lhs rhs
Proof state after:
case left.intro
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : (∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X
⊢ False
Theorem: A5
Proof state before:
case left.intro
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : (∀ (v : W), relate M a w v → evaluate M v X) → ∃ x, relate M b w x ∧ ¬evaluate M x X
⊢ False
Tactic:
contrapose! rhs
Proof state after:
case left.intro
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M b w x → evaluate M x X
Theorem: A5
Proof state before:
case left.intro
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ (∀ (v : W), relate M a w v → evaluate M v X) ∧ ∀ (x : W), relate M b w x → evaluate M x X
Tactic:
constructor
Proof state after:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ ∀ (v : W), relate M a w v → evaluate M v X

case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ ∀ (x : W), relate M b w x → evaluate M x X
Theorem: A5
Proof state before:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ ∀ (v : W), relate M a w v → evaluate M v X
Tactic:
intro v
Proof state after:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
v : W
⊢ relate M a w v → evaluate M v X
Theorem: A5
Proof state before:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
v : W
⊢ relate M a w v → evaluate M v X
Tactic:
specialize lhs v
Proof state after:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
⊢ relate M a w v → evaluate M v X
Theorem: A5
Proof state before:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
⊢ relate M a w v → evaluate M v X
Tactic:
intro (w_a_v : relate M a w v)
Proof state after:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ evaluate M v X
Theorem: A5
Proof state before:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ evaluate M v X
Tactic:
apply lhs
Proof state after:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ relate M a w v ∨ relate M b w v
Theorem: A5
Proof state before:
case left.intro.left
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ relate M a w v ∨ relate M b w v
Tactic:
left
Proof state after:
case left.intro.left.h
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ relate M a w v
Theorem: A5
Proof state before:
case left.intro.left.h
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ relate M a w v
Tactic:
exact w_a_v
Proof state after:
no goals
Theorem: A5
Proof state before:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
⊢ ∀ (x : W), relate M b w x → evaluate M x X
Tactic:
intro v
Proof state after:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
v : W
⊢ relate M b w v → evaluate M v X
Theorem: A5
Proof state before:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ (v : W), relate M a w v ∨ relate M b w v → evaluate M v X
rhs : ¬False
v : W
⊢ relate M b w v → evaluate M v X
Tactic:
specialize lhs v
Proof state after:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
⊢ relate M b w v → evaluate M v X
Theorem: A5
Proof state before:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
⊢ relate M b w v → evaluate M v X
Tactic:
intro (w_b_v : relate M b w v)
Proof state after:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ evaluate M v X
Theorem: A5
Proof state before:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ evaluate M v X
Tactic:
apply lhs
Proof state after:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ relate M a w v ∨ relate M b w v
Theorem: A5
Proof state before:
case left.intro.right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ relate M a w v ∨ relate M b w v
Tactic:
right
Proof state after:
case left.intro.right.h
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ relate M b w v
Theorem: A5
Proof state before:
case left.intro.right.h
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_b_v : relate M b w v
⊢ relate M b w v
Tactic:
exact w_b_v
Proof state after:
no goals
Theorem: A5
Proof state before:
case right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a⋓b⌉X)⋀(~⌈a⋓b⌉X))
Tactic:
simp only [evaluate]
Proof state after:
case right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ ¬((∀ (v : W), relate M (a⋓b) w v → evaluate M v X) ∧ ¬∀ (v : W), relate M (a⋓b) w v → evaluate M v X)
Theorem: A5
Proof state before:
case right
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ ¬((∀ (v : W), relate M (a⋓b) w v → evaluate M v X) ∧ ¬∀ (v : W), relate M (a⋓b) w v → evaluate M v X)
Tactic:
tauto
Proof state after:
no goals
Theorem: A6
Proof state before:
a : Program
X : Formula
⊢ tautology ((~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X))⋀(~(⌈∗a⌉X)⋀(~⌈∗a⌉X)))
Tactic:
unfold tautology evaluate
Proof state after:
a : Program
X : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X)) ∧ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Theorem: A6
Proof state before:
a : Program
X : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X)) ∧ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Tactic:
intro W M w
Proof state after:
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X)) ∧ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Theorem: A6
Proof state before:
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X)) ∧ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Tactic:
constructor
Proof state after:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X))

case right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Theorem: A6
Proof state before:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X))
Tactic:
simp
Proof state after:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X) →
    evaluate M w X ∧
      ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Theorem: A6
Proof state before:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X) →
    evaluate M w X ∧
      ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Tactic:
intro starAX
Proof state after:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ evaluate M w X ∧ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Theorem: A6
Proof state before:
case left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ evaluate M w X ∧ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Tactic:
constructor
Proof state after:
case left.left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ evaluate M w X

case left.right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Theorem: A6
Proof state before:
case left.left
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ evaluate M w X
Tactic:
apply starAX
Proof state after:
case left.left.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ Relation.ReflTransGen (relate M a) w w
Theorem: A6
Proof state before:
case left.left.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ Relation.ReflTransGen (relate M a) w w
Tactic:
exact Relation.ReflTransGen.refl
Proof state after:
no goals
Theorem: A6
Proof state before:
case left.right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
⊢ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
Tactic:
intro v w_a_v v_1 v_aS_v1
Proof state after:
case left.right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ evaluate M v_1 X
Theorem: A6
Proof state before:
case left.right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ evaluate M v_1 X
Tactic:
apply starAX
Proof state after:
case left.right.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ Relation.ReflTransGen (relate M a) w v_1
Theorem: A6
Proof state before:
case left.right.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ Relation.ReflTransGen (relate M a) w v_1
Tactic:
rw [Relation.ReflTransGen.cases_head_iff]
Proof state after:
case left.right.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ w = v_1 ∨ ∃ c, relate M a w c ∧ Relation.ReflTransGen (relate M a) c v_1
Theorem: A6
Proof state before:
case left.right.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ w = v_1 ∨ ∃ c, relate M a w c ∧ Relation.ReflTransGen (relate M a) c v_1
Tactic:
right
Proof state after:
case left.right.a.h
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ ∃ c, relate M a w c ∧ Relation.ReflTransGen (relate M a) c v_1
Theorem: A6
Proof state before:
case left.right.a.h
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ ∃ c, relate M a w c ∧ Relation.ReflTransGen (relate M a) c v_1
Tactic:
use v
Proof state after:
no goals
Theorem: A6
Proof state before:
case right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Tactic:
simp
Proof state after:
no goals
Theorem: starIffFinitelyManyStepsModel
Proof state before:
W : Type
M : KripkeModel W
x z : W
α : Program
⊢ Relation.ReflTransGen (relate M α) x z ↔
    ∃ n ys, x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), relate M α (ys.get i.castSucc) (ys.get i.succ)
Tactic:
exact ReflTransGen.iff_finitelyManySteps (relate M α) x z
Proof state after:
no goals
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
⊢ tautology (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
Tactic:
intro W M w
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))
Tactic:
simp
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ →
    (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
      ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w φ →
    (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
      ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro Mwφ
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
    ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
⊢ (∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ) →
    ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro MwStarImpHyp
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
⊢ ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Theorem: inductionAxiom
Proof state before:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
⊢ ∀ (x : W), Relation.ReflTransGen (relate M a) w x → evaluate M x φ
Tactic:
intro x w_starA_x
Proof state after:
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
w_starA_x : Relation.ReflTransGen (relate M a) w x
⊢ evaluate M x φ