internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case mp.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
cases em (δ = ε)
Proof state after:
case mp.intro.mk.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
h✝ : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))

case mp.intro.mk.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
h✝ : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_is_ε : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
subst δ_is_ε
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
have claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ)) := by
  rw [conEval] at w_Con
  simp [Yset, Con] at w_Con
  have := w_Con (~⌈β⌉ψ)
  simp only [or_true, forall_true_left] at this
  have IHβ := localDiamondTruth β ψ W M w
  rw [IHβ] at this
  rw [disEval, helper] at this
  exact this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
rcases claim with ⟨⟨Gs,γ⟩, Gsγ_in, claim⟩
Proof state after:
case intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
case intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
unfold H
Proof state after:
case intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃
    Fδ ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join,
    evaluate M w (Con (Yset Fδ ψ))
Theorem: localDiamondTruth
Proof state before:
case intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃
    Fδ ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join,
    evaluate M w (Con (Yset Fδ ψ))
Tactic:
use ⟨Fs ∪ Gs, γ⟩
Proof state after:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs ∪ Gs, γ) ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join ∧
    evaluate M w (Con (Yset (Fs ∪ Gs, γ) ψ))
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs ∪ Gs, γ) ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join ∧
    evaluate M w (Con (Yset (Fs ∪ Gs, γ) ψ))
Tactic:
constructor
Proof state after:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs ∪ Gs, γ) ∈
    (List.map
        (fun x =>
          match x with
          | (F, δ) =>
            if δ = ε then
              (List.map
                  (fun x =>
                    match x with
                    | (G, δ') => [(F ∪ G, δ')])
                  (H β)).join
            else [(F, δ ++ [β])])
        (H α)).join

case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ evaluate M w (Con (Yset (Fs ∪ Gs, γ) ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
rw [conEval] at w_Con
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ f ∈ Yset (Fs, ε) (⌈β⌉ψ), evaluate M w f
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ f ∈ Yset (Fs, ε) (⌈β⌉ψ), evaluate M w f
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
simp [Yset, Con] at w_Con
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
have := w_Con (~⌈β⌉ψ)
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : (~⌈β⌉ψ) ∈ Fs ∨ (~⌈β⌉ψ) = (~⌈β⌉ψ) → evaluate M w (~⌈β⌉ψ)
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : (~⌈β⌉ψ) ∈ Fs ∨ (~⌈β⌉ψ) = (~⌈β⌉ψ) → evaluate M w (~⌈β⌉ψ)
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
simp only [or_true, forall_true_left] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : evaluate M w (~⌈β⌉ψ)
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : evaluate M w (~⌈β⌉ψ)
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
have IHβ := localDiamondTruth β ψ W M w
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
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 β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
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 β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
rw [IHβ] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
rw [disEval, helper] at this
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
Tactic:
exact this
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs ∪ Gs, γ) ∈
    (List.map
        (fun x =>
          match x with
          | (F, δ) =>
            if δ = ε then
              (List.map
                  (fun x =>
                    match x with
                    | (G, δ') => [(F ∪ G, δ')])
                  (H β)).join
            else [(F, δ ++ [β])])
        (H α)).join
Tactic:
simp only [List.mem_join, List.mem_map, Prod.exists]
Proof state after:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ l,
    (∃ a b, (a, b) ∈ H α ∧ (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs ∪ Gs, γ) ∈ l
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ l,
    (∃ a b, (a, b) ∈ H α ∧ (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs ∪ Gs, γ) ∈ l
Tactic:
use ((H β).map (fun ⟨Gs',δ'⟩ => [⟨Fs ∪ Gs', δ'⟩])).join
Proof state after:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
          (List.map
              (fun x =>
                match x with
                | (Gs', δ') => [(Fs ∪ Gs', δ')])
              (H β)).join) ∧
    (Fs ∪ Gs, γ) ∈
      (List.map
          (fun x =>
            match x with
            | (Gs', δ') => [(Fs ∪ Gs', δ')])
          (H β)).join
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
          (List.map
              (fun x =>
                match x with
                | (Gs', δ') => [(Fs ∪ Gs', δ')])
              (H β)).join) ∧
    (Fs ∪ Gs, γ) ∈
      (List.map
          (fun x =>
            match x with
            | (Gs', δ') => [(Fs ∪ Gs', δ')])
          (H β)).join
Tactic:
simp only [List.mem_join, List.mem_map, Prod.exists]
Proof state after:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
          (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join) ∧
    ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, γ) ∈ l
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
          (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join) ∧
    ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, γ) ∈ l
Tactic:
constructor
Proof state after:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ a b,
    (a, b) ∈ H α ∧
      (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
        (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join

case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, γ) ∈ l
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ a b,
    (a, b) ∈ H α ∧
      (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
        (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join
Tactic:
use Fs, ε
Proof state after:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs, ε) ∈ H α ∧
    (if ε = ε then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]) =
      (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs, ε) ∈ H α ∧
    (if ε = ε then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]) =
      (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join
Tactic:
simp only [reduceIte, and_true]
Proof state after:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs, ε) ∈ H α
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ (Fs, ε) ∈ H α
Tactic:
exact Fδ_in
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, γ) ∈ l
Tactic:
tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ evaluate M w (Con (Yset (Fs ∪ Gs, γ) ψ))
Tactic:
simp only [Yset, conEval, List.mem_union_iff, List.mem_singleton] at *
Proof state after:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
Tactic:
intro f f_in
Proof state after:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
⊢ evaluate M w f
Tactic:
specialize w_Con f
Proof state after:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
w_Con : f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
w_Con : f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
⊢ evaluate M w f
Tactic:
specialize claim f
Proof state after:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
w_Con : f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
w_Con : f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : f ∈ Gs ∨ 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
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
unfold H
Proof state after:
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ ∃
    Fδ ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join,
    evaluate M w (Con (Yset Fδ ψ))