internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case h.right.intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs ∨ f = (~⌈β⌉ψ)
⊢ evaluate M w f
Tactic:
cases f_in
Proof state after:
case h.right.intro.refl.refl.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
h✝ : f ∈ Gs
⊢ evaluate M w f

case h.right.intro.refl.refl.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
h✝ : f = (~⌈β⌉ψ)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
⊢ evaluate M w f
Tactic:
case inl f_in =>
  rw [conEval] at w_Con
  simp [Yset] at *
  specialize w_Con f
  tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_def : f = (~⌈β⌉ψ)
⊢ evaluate M w f
Tactic:
case inr f_def =>
  subst f_def
  have IHβ := localDiamondTruth β ψ W M w
  rw [IHβ, disEval, helper]
  clear IHβ
  refine ⟨⟨aaa, δ⟩, ⟨_in_Hβ, ?_⟩⟩
  rw [conEval]
  rw [conEval] at w_Con
  simp [Yset] at *
  intro f
  specialize w_Con f
  tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
⊢ evaluate M w f
Tactic:
rw [conEval] at w_Con
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : ∀ f ∈ Yset (Gs ∪ aaa, δ) ψ, evaluate M w f
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : ∀ f ∈ Yset (Gs ∪ aaa, δ) ψ, evaluate M w f
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
⊢ evaluate M w f
Tactic:
simp [Yset] at *
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
Tactic:
specialize w_Con f
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
Tactic:
tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_def : f = (~⌈β⌉ψ)
⊢ evaluate M w f
Tactic:
subst f_def
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ evaluate M w (~⌈β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ evaluate M w (~⌈β⌉ψ)
Tactic:
have IHβ := localDiamondTruth β ψ W M w
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ evaluate M w (~⌈β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ evaluate M w (~⌈β⌉ψ)
Tactic:
rw [IHβ, disEval, helper]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
Tactic:
clear IHβ
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
Tactic:
refine ⟨⟨aaa, δ⟩, ⟨_in_Hβ, ?_⟩⟩
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ evaluate M w (Con (Yset (aaa, δ) ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ evaluate M w (Con (Yset (aaa, δ) ψ))
Tactic:
rw [conEval]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∀ f ∈ Yset (aaa, δ) ψ, evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∀ f ∈ Yset (aaa, δ) ψ, evaluate M w f
Tactic:
rw [conEval] at w_Con
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : ∀ f ∈ Yset (Gs ∪ aaa, δ) ψ, evaluate M w f
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∀ f ∈ Yset (aaa, δ) ψ, evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : ∀ f ∈ Yset (Gs ∪ aaa, δ) ψ, evaluate M w f
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∀ f ∈ Yset (aaa, δ) ψ, evaluate M w f
Tactic:
simp [Yset] at *
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Tactic:
intro f
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
f : Formula
⊢ f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
f : Formula
⊢ f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Tactic:
specialize w_Con f
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
w_Con : (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
w_Con : (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ f ∈ aaa ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
Tactic:
tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]
δ_not_ε : ¬γ = ε
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
simp_all
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Gs : List Formula
γ : List Program
w_Con : evaluate M w (Con (Yset (Gs, γ ++ [β]) ψ))
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : Fs = Gs ∧ δ = γ ++ [β]
δ_not_ε : ¬γ = []
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Gs : List Formula
γ : List Program
w_Con : evaluate M w (Con (Yset (Gs, γ ++ [β]) ψ))
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : Fs = Gs ∧ δ = γ ++ [β]
δ_not_ε : ¬γ = []
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Tactic:
cases Gγ_in_l
Proof state after:
case intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Gs : List Formula
γ : List Program
w_Con : evaluate M w (Con (Yset (Gs, γ ++ [β]) ψ))
Gγ_in : (Gs, γ) ∈ H α
δ_not_ε : ¬γ = []
left✝ : Fs = Gs
right✝ : δ = γ ++ [β]
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Gs : List Formula
γ : List Program
w_Con : evaluate M w (Con (Yset (Gs, γ ++ [β]) ψ))
Gγ_in : (Gs, γ) ∈ H α
δ_not_ε : ¬γ = []
left✝ : Fs = Gs
right✝ : δ = γ ++ [β]
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Tactic:
subst_eqs
Proof state after:
case intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
γ : List Program
δ_not_ε : ¬γ = []
w_Con : evaluate M w (Con (Yset (Fs, γ ++ [β]) ψ))
Gγ_in : (Fs, γ) ∈ H α
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
γ : List Program
δ_not_ε : ¬γ = []
w_Con : evaluate M w (Con (Yset (Fs, γ ++ [β]) ψ))
Gγ_in : (Fs, γ) ∈ H α
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Tactic:
simp_all [Yset, conEval, boxes_append]
Proof state after:
case intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
γ : List Program
δ_not_ε : ¬γ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ⌉⌉⌈β⌉ψ) → evaluate M w f
Gγ_in : (Fs, γ) ∈ H α
⊢ ∃ a b, (a, b) ∈ H α ∧ ∀ (f : Formula), f ∈ a ∨ f = (~⌈⌈b⌉⌉⌈β⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
γ : List Program
δ_not_ε : ¬γ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ⌉⌉⌈β⌉ψ) → evaluate M w f
Gγ_in : (Fs, γ) ∈ H α
⊢ ∃ a b, (a, b) ∈ H α ∧ ∀ (f : Formula), f ∈ a ∨ f = (~⌈⌈b⌉⌉⌈β⌉ψ) → evaluate M w f
Tactic:
use Fs, γ
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
let ρ := dis ((H (∗β)).map (fun Fδ => Con (Yset Fδ ψ)))
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
suffices goal : (~⌈∗β⌉ψ) ≡ ρ by
  have := @equiv_iff _ _ goal W M w
  simp only [modelCanSemImplyForm, evaluatePoint] at this
  rw [this]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ (~⌈∗β⌉ψ)≡ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ (~⌈∗β⌉ψ)≡ρ
Tactic:
have right_to_left_claim : ∀ W M (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ) := by
  clear W M w; intro W M w
  unfold_let ρ
  rw [disEval, helper]
  rintro ⟨⟨Fs,δ⟩, ⟨Fδ_in, w_Con⟩⟩
  rw [conEval] at w_Con
  simp [H] at Fδ_in
  cases Fδ_in
  case inl hyp =>
    cases hyp
    subst_eqs
    simp_all [Yset]
    use w
  case inr hyp =>
    have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs,γ) ∈ H β := by aesop
    rcases this with ⟨γ, ⟨δ_def, _, Fγ_in⟩⟩
    subst δ_def
    simp only [Yset, List.mem_union_iff, List.mem_singleton] at w_Con
    have := w_Con (~⌈⌈γ ++ [∗β]⌉⌉ψ)
    simp at this
    suffices evaluate M w (~⌈β⌉⌈∗β⌉ψ) by
      simp at *
      rcases this with ⟨v, ⟨w_β_v, ⟨u, ⟨v_Sβ_u, u_nPsi⟩⟩⟩⟩
      refine ⟨u, ?_, u_nPsi⟩
      exact Relation.ReflTransGen.head w_β_v v_Sβ_u
    have IHβ := localDiamondTruth β (⌈∗β⌉ψ) W M w
    rw [disEval, helper] at IHβ
    rw [IHβ]
    refine ⟨⟨Fs, γ⟩, ⟨Fγ_in, ?_⟩⟩
    simp_all [conEval, Yset, boxes_append]
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
⊢ (~⌈∗β⌉ψ)≡ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
⊢ (~⌈∗β⌉ψ)≡ρ
Tactic:
clear W M w
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
⊢ (~⌈∗β⌉ψ)≡ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
⊢ (~⌈∗β⌉ψ)≡ρ
Tactic:
intro W M w
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w ρ
Tactic:
constructor
Proof state after:
case mp
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ

case mpr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
goal : (~⌈∗β⌉ψ)≡ρ
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
have := @equiv_iff _ _ goal W M w
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
goal : (~⌈∗β⌉ψ)≡ρ
this : (M, w)⊨(~⌈∗β⌉ψ) ↔ (M, w)⊨ρ
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
goal : (~⌈∗β⌉ψ)≡ρ
this : (M, w)⊨(~⌈∗β⌉ψ) ↔ (M, w)⊨ρ
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
simp only [modelCanSemImplyForm, evaluatePoint] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
goal : (~⌈∗β⌉ψ)≡ρ
this : evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w ρ
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
goal : (~⌈∗β⌉ψ)≡ρ
this : evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w ρ
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
rw [this]
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Tactic:
clear W M w
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Tactic:
intro W M w
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Tactic:
unfold_let ρ
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))) → evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))) → evaluate M w (~⌈∗β⌉ψ)
Tactic:
rw [disEval, helper]
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ (∃ Fδ ∈ H (∗β), evaluate M w (Con (Yset Fδ ψ))) → evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
⊢ (∃ Fδ ∈ H (∗β), evaluate M w (Con (Yset Fδ ψ))) → evaluate M w (~⌈∗β⌉ψ)
Tactic:
rintro ⟨⟨Fs,δ⟩, ⟨Fδ_in, w_Con⟩⟩
Proof state after:
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
rw [conEval] at w_Con
Proof state after:
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
simp [H] at Fδ_in
Proof state after:
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
Fδ_in : Fs = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)