Theorem: localBoxTruth (Pdl/Unfold.lean)

State before:
γ : Program
ψ : Formula
⊢ (⌈γ⌉ψ)≡dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))
Tactic:
intro W M w
State after:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))

State before:
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
constructor
State after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) → evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))

case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))) → evaluate M w (⌈γ⌉ψ)

State before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) → evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
intro w_γψ
State after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))

State before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
Tactic:
rw [disEval]
State after:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f

State before:
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_γψ : evaluate M w (⌈γ⌉ψ)
⊢ ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
Tactic:
sorry
State after:
no goals

State before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))) → evaluate M w (⌈γ⌉ψ)
Tactic:
intro w_Cons
State after:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rw [disEval] at w_Cons
State after:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
w_Cons : ∃ f ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ), evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rcases w_Cons with ⟨φ, φ_in, w_φ⟩
State after:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
φ_in : φ ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)
w_φ : evaluate M w φ
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
φ_in : φ ∈ List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)
w_φ : evaluate M w φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
simp at φ_in
State after:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
φ_in : ∃ a ∈ allTP γ, Con (Xset γ a ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
φ_in : ∃ a ∈ allTP γ, Con (Xset γ a ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rcases φ_in with ⟨ℓ, ℓ_in, def_φ⟩
State after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
def_φ : Con (Xset γ ℓ ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
def_φ : Con (Xset γ ℓ ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
subst def_φ
State after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : evaluate M w (Con (Xset γ ℓ ψ))
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : evaluate M w (Con (Xset γ ℓ ψ))
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
rw [conEval] at w_φ
State after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
have := localBoxTruth' γ ψ ℓ W M w
State after:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
this : evaluate M w ((⌈γ⌉ψ)⋀signature γ ℓ) ↔ evaluate M w (Con (Xset γ ℓ ψ)⋀signature γ ℓ)
⊢ evaluate M w (⌈γ⌉ψ)

State before:
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
this : evaluate M w ((⌈γ⌉ψ)⋀signature γ ℓ) ↔ evaluate M w (Con (Xset γ ℓ ψ)⋀signature γ ℓ)
⊢ evaluate M w (⌈γ⌉ψ)
Tactic:
sorry
State after:
no goals