Theorem: A6 (Pdl/Examples.lean)

State before:
a : Program
X : Formula
⊢ tautology ((~(⌈∗a⌉X)⋀(~X⋀⌈a⌉⌈∗a⌉X))⋀(~(⌈∗a⌉X)⋀(~⌈∗a⌉X)))
Tactic:
unfold tautology evaluate
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))

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

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

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

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

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

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

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
State after:
no goals

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

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

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

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

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
State after:
no goals

State before:
case right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈∗a⌉X)⋀(~⌈∗a⌉X))
Tactic:
simp
State after:
no goals