Theorem: oneSidedLocalRuleTruth (Pdl/LocalTableau.lean)

State before:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
⊢ Con X≡discon B
Tactic:
intro W M w
State after:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con X) ↔ evaluate M w (discon B)

State before:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con X) ↔ evaluate M w (discon B)
Tactic:
cases lr
State after:
case bot
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [⊥]) ↔ evaluate M w (discon ∅)

case not
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [φ✝, ~φ✝]) ↔ evaluate M w (discon ∅)

case neg
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [~~φ✝]) ↔ evaluate M w (discon [[φ✝]])

case con
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [φ✝⋀ψ✝]) ↔ evaluate M w (discon [[φ✝, ψ✝]])

case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])

case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))

State before:
case bot
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [⊥]) ↔ evaluate M w (discon ∅)

case not
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [φ✝, ~φ✝]) ↔ evaluate M w (discon ∅)

case neg
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [~~φ✝]) ↔ evaluate M w (discon [[φ✝]])

case con
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [φ✝⋀ψ✝]) ↔ evaluate M w (discon [[φ✝, ψ✝]])

case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])

case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
all_goals try (simp; done)
State after:
case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [~⌈α⌉φ]) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
case dia α φ =>
  rw [conEval]
  simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
  rw [localDiamondTruth α φ W M w, disEval, disconEval]
  apply mapCon_mapForall
State after:
no goals

State before:
case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])
Tactic:
try (simp; done)
State after:
no goals

State before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
(simp; done)
State after:
no goals

State before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
simp
State after:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ (∃ x, relate M α✝ w x ∧ ¬evaluate M x φ✝) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))

State before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ (∃ x, relate M α✝ w x ∧ ¬evaluate M x φ✝) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
done
State after:
no goals

State before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
(aesop; done)
State after:
no goals

State before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
aesop
State after:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
w_1 : W
left : relate M α w w_1
right : ¬evaluate M w_1 φ
⊢ evaluate M w (discon (unfoldDiamond α φ))

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
a : evaluate M w (discon (unfoldDiamond α φ))
⊢ ∃ x, relate M α w x ∧ ¬evaluate M x φ

State before:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
w_1 : W
left : relate M α w w_1
right : ¬evaluate M w_1 φ
⊢ evaluate M w (discon (unfoldDiamond α φ))

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
a : evaluate M w (discon (unfoldDiamond α φ))
⊢ ∃ x, relate M α w x ∧ ¬evaluate M x φ
Tactic:
done
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [⌈α⌉φ]) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
rw [conEval]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldBox α φ))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
simp only [List.mem_singleton, forall_eq]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (⌈α⌉φ) ↔ evaluate M w (discon (unfoldBox α φ))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (⌈α⌉φ) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
rw [localBoxTruth α φ W M w]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset α ℓ φ)) (allTP α))) ↔ evaluate M w (discon (unfoldBox α φ))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset α ℓ φ)) (allTP α))) ↔ evaluate M w (discon (unfoldBox α φ))
Tactic:
simp only [disEval, List.mem_map, exists_exists_and_eq_and, unfoldBox, disconEval]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
constructor
State after:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f) → ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))

State before:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
rintro ⟨l,hyp⟩
State after:
case mp.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f

State before:
case mp.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
Tactic:
use l
State after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Tactic:
rw [conEval] at hyp
State after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
Tactic:
tauto
State after:
no goals

State before:
case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f) → ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Tactic:
rintro ⟨l,hyp⟩
State after:
case mpr.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))

State before:
case mpr.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
Tactic:
use l
State after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))

State before:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
Tactic:
rw [conEval]
State after:
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [~⌈α⌉φ]) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
rw [conEval]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [~⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldDiamond α φ))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∀ f ∈ [~⌈α⌉φ], evaluate M w f) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (~⌈α⌉φ) ↔ evaluate M w (discon (List.map (fun Fδ => Yset Fδ φ) (H α)))
Tactic:
rw [localDiamondTruth α φ W M w, disEval, disconEval]
State after:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ φ)) (H α), evaluate M w f) ↔
    ∃ Y ∈ List.map (fun Fδ => Yset Fδ φ) (H α), ∀ f ∈ Y, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (Yset Fδ φ)) (H α), evaluate M w f) ↔
    ∃ Y ∈ List.map (fun Fδ => Yset Fδ φ) (H α), ∀ f ∈ Y, evaluate M w f
Tactic:
apply mapCon_mapForall
State after:
no goals