Theorem: notSat_iff_semImplies (Pdl/Semantics.lean)

State before:
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) ↔ X⊨[φ]
Tactic:
constructor
State after:
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]

case mpr
X : List Formula
φ : Formula
⊢ X⊨[φ] → ¬satisfiable (X ∪ [~φ])

State before:
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]
Tactic:
simp only [satisfiable, not_exists, not_forall, exists_prop, setCanSemImplySet, semImpliesSets, forall_eq]
State after:
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]

State before:
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]
Tactic:
intro nSat W M w satX
State after:
case mp
X : List Formula
φ : Formula
nSat : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
⊢ ∀ ψ ∈ [φ], evaluate M w ψ

State before:
case mp
X : List Formula
φ : Formula
nSat : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Tactic:
specialize nSat W M w
State after:
case mp
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
nSat : ∃ x ∈ X ∪ [~φ], ¬evaluate M w x
⊢ ∀ ψ ∈ [φ], evaluate M w ψ

State before:
case mp
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
nSat : ∃ x ∈ X ∪ [~φ], ¬evaluate M w x
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Tactic:
rcases nSat with ⟨φ, phi_in, not_phi⟩
State after:
case mp.intro.intro
X : List Formula
φ✝ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
φ : Formula
phi_in : φ ∈ X ∪ [~φ✝]
not_phi : ¬evaluate M w φ
⊢ ∀ ψ ∈ [φ✝], evaluate M w ψ

State before:
case mp.intro.intro
X : List Formula
φ✝ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
φ : Formula
phi_in : φ ∈ X ∪ [~φ✝]
not_phi : ¬evaluate M w φ
⊢ ∀ ψ ∈ [φ✝], evaluate M w ψ
Tactic:
aesop
State after:
no goals

State before:
case mpr
X : List Formula
φ : Formula
⊢ X⊨[φ] → ¬satisfiable (X ∪ [~φ])
Tactic:
intro X_φ
State after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
⊢ ¬satisfiable (X ∪ [~φ])

State before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
⊢ ¬satisfiable (X ∪ [~φ])
Tactic:
by_contra hyp
State after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : satisfiable (X ∪ [~φ])
⊢ False

State before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : satisfiable (X ∪ [~φ])
⊢ False
Tactic:
simp only [satisfiable, setCanSemImplySet, semImpliesSets] at hyp
State after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False

State before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Tactic:
rcases hyp with ⟨W, M, w, w_⟩
State after:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
X_φ : X⊨[φ]
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False

State before:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
X_φ : X⊨[φ]
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Tactic:
specialize X_φ W M w
State after:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False

State before:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
cases X
State after:
case mpr.intro.intro.intro.nil
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ [] ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ [], evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False

case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False

State before:
case mpr.intro.intro.intro.nil
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ [] ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ [], evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
have := w_ (~φ)
State after:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
this : (~φ) ∈ head✝ :: tail✝ ∪ [~φ] → evaluate M w (~φ)
⊢ False

State before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
this : (~φ) ∈ head✝ :: tail✝ ∪ [~φ] → evaluate M w (~φ)
⊢ False
Tactic:
simp at *
State after:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : evaluate M w head✝ ∧ ∀ (a : Formula), a ∈ tail✝ ∨ a = (~φ) → evaluate M w a
X_φ : evaluate M w head✝ → (∀ a ∈ tail✝, evaluate M w a) → evaluate M w φ
this : ¬evaluate M w φ
⊢ False

State before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : evaluate M w head✝ ∧ ∀ (a : Formula), a ∈ tail✝ ∨ a = (~φ) → evaluate M w a
X_φ : evaluate M w head✝ → (∀ a ∈ tail✝, evaluate M w a) → evaluate M w φ
this : ¬evaluate M w φ
⊢ False
Tactic:
simp_all
State after:
no goals