Theorem: forms_to_lists (Pdl/Semantics.lean)

State before:
φ ψ : Formula
⊢ φ⊨ψ → [φ]⊨[ψ]
Tactic:
intro impTaut
State after:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ [φ]⊨[ψ]

State before:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ [φ]⊨[ψ]
Tactic:
intro W M w lhs ψ psi_in_psi
State after:
φ ψ✝ : Formula
impTaut : φ⊨ψ✝
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
⊢ evaluate M w ψ

State before:
φ ψ✝ : Formula
impTaut : φ⊨ψ✝
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
⊢ evaluate M w ψ
Tactic:
specialize impTaut W M w
State after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
⊢ evaluate M w ψ

State before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
⊢ evaluate M w ψ
Tactic:
simp at psi_in_psi lhs
State after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ

State before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ
Tactic:
rw [psi_in_psi]
State after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ✝

State before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ✝
Tactic:
apply impTaut
State after:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]

State before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Tactic:
rw [←vDashSingleton_iff_vDash_formula φ] at lhs
State after:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : (M, w)⊨[φ]
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]

State before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : (M, w)⊨[φ]
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1
Tactic:
tauto
State after:
no goals

State before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Tactic:
aesop
State after:
no goals