Theorem: A5 (Pdl/Examples.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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