Theorem: A3 (Pdl/Examples.lean)

State before:
a : Program
X Y : Formula
⊢ tautology (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))
Tactic:
unfold tautology
State after:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))

State before:
a : Program
X Y : Formula
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))
Tactic:
simp
State after:
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

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

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

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

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

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

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

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

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