internlm/Lean-Github huggingface dataset:
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
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 (~⌈∗β⌉ψ)
Tactic:
cases Fδ_in
Proof state after:
case intro.mk.intro.inl
ψ : 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
h✝ : Fs = [] ∧ δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)

case intro.mk.intro.inr
ψ : 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
h✝ : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ 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
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : Fs = [] ∧ δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
case inl hyp =>
  cases hyp
  subst_eqs
  simp_all [Yset]
  use w
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
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:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
hyp : Fs = [] ∧ δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
cases hyp
Proof state after:
case 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
left✝ : Fs = []
right✝ : δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case 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
left✝ : Fs = []
right✝ : δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
subst_eqs
Proof state after:
case intro.refl.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
w_Con : ∀ f ∈ Yset ([], []) ψ, evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.refl.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
w_Con : ∀ f ∈ Yset ([], []) ψ, evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
simp_all [Yset]
Proof state after:
case intro.refl.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
w_Con : ¬evaluate M w ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case intro.refl.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
w_Con : ¬evaluate M w ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Tactic:
use w
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs,γ) ∈ H β := by aesop
Proof state after:
ψ : 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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
this : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs, γ) ∈ 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
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
this : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs, γ) ∈ H β
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
rcases this with ⟨γ, ⟨δ_def, _, Fγ_in⟩⟩
Proof state after:
case intro.intro.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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
γ : List Program
δ_def : δ = γ ++ [∗β]
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
γ : List Program
δ_def : δ = γ ++ [∗β]
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
subst δ_def
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
w_Con : ∀ f ∈ Yset (Fs, γ ++ [∗β]) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
w_Con : ∀ f ∈ Yset (Fs, γ ++ [∗β]) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
simp only [Yset, List.mem_union_iff, List.mem_singleton] at w_Con
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
have := w_Con (~⌈⌈γ ++ [∗β]⌉⌉ψ)
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : (~⌈⌈γ ++ [∗β]⌉⌉ψ) ∈ Fs ∨ (~⌈⌈γ ++ [∗β]⌉⌉ψ) = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w (~⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : (~⌈⌈γ ++ [∗β]⌉⌉ψ) ∈ Fs ∨ (~⌈⌈γ ++ [∗β]⌉⌉ψ) = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w (~⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
simp at this
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
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
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Tactic:
have IHβ := localDiamondTruth β (⌈∗β⌉ψ) W M w
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈∗β⌉ψ))) (H β)))
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ (⌈∗β⌉ψ))) (H β)))
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Tactic:
rw [disEval, helper] at IHβ
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ evaluate M w (~⌈β⌉⌈∗β⌉ψ)
Tactic:
rw [IHβ]
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
Tactic:
refine ⟨⟨Fs, γ⟩, ⟨Fγ_in, ?_⟩⟩
Proof state after:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ evaluate M w (Con (Yset (Fs, γ) (⌈∗β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.intro.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
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ evaluate M w (Con (Yset (Fs, γ) (⌈∗β⌉ψ)))
Tactic:
simp_all [conEval, Yset, boxes_append]
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : 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
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs, γ) ∈ H β
Tactic:
aesop
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
γ : List Program
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this✝ : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
this : evaluate M w (~⌈β⌉⌈∗β⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
Tactic:
simp at *
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
γ : List Program
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this✝ : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
this : ∃ x, relate M β w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
γ : List Program
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this✝ : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
this : ∃ x, relate M β w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Tactic:
rcases this with ⟨v, ⟨w_β_v, ⟨u, ⟨v_Sβ_u, u_nPsi⟩⟩⟩⟩
Proof state after:
case intro.intro.intro.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
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
v : W
w_β_v : relate M β w v
u : W
v_Sβ_u : Relation.ReflTransGen (relate M β) v u
u_nPsi : ¬evaluate M u ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.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
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
v : W
w_β_v : relate M β w v
u : W
v_Sβ_u : Relation.ReflTransGen (relate M β) v u
u_nPsi : ¬evaluate M u ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
Tactic:
refine ⟨u, ?_, u_nPsi⟩
Proof state after:
case intro.intro.intro.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
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
v : W
w_β_v : relate M β w v
u : W
v_Sβ_u : Relation.ReflTransGen (relate M β) v u
u_nPsi : ¬evaluate M u ψ
⊢ Relation.ReflTransGen (relate M β) w u
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.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
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
v : W
w_β_v : relate M β w v
u : W
v_Sβ_u : Relation.ReflTransGen (relate M β) v u
u_nPsi : ¬evaluate M u ψ
⊢ Relation.ReflTransGen (relate M β) w u
Tactic:
exact Relation.ReflTransGen.head w_β_v v_Sβ_u
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
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 ρ
Tactic:
let x : Nat := freshVarProg β
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
x : ℕ := freshVarProg β
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
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
x : ℕ := freshVarProg β
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ
Tactic:
have x_not_in : x ∉ HasVocabulary.voc β := by apply freshVarProg_is_fresh
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
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
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
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ
Tactic:
let σ0 : Formula := dis $
  (H β).map (fun (F,δ) => if δ = ε then Con F else ⊥)
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
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ