internlm/Lean-Github huggingface dataset:
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δ ∈
      (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, δ ++ [β]⟩
Proof state after:
case h
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈
      (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, δ ++ [β]) ψ))
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈
      (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, δ ++ [β]) ψ))
Tactic:
constructor
Proof state after:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈
    (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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ evaluate M w (Con (Yset (Fs, δ ++ [β]) ψ))
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈
    (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
Proof state after:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ ∃ 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, δ ++ [β]) ∈ l
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ ∃ 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, δ ++ [β]) ∈ l
Tactic:
use [(Fs, δ ++ [β])]
Proof state after:
case h
ψ : 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_ε : ¬δ = ε
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = [(Fs, δ ++ [β])]) ∧
    (Fs, δ ++ [β]) ∈ [(Fs, δ ++ [β])]
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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_ε : ¬δ = ε
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = [(Fs, δ ++ [β])]) ∧
    (Fs, δ ++ [β]) ∈ [(Fs, δ ++ [β])]
Tactic:
constructor
Proof state after:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ ∃ a b,
    (a, b) ∈ H α ∧
      (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = [(Fs, δ ++ [β])]

case h.right
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ [(Fs, δ ++ [β])]
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : 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_ε : ¬δ = ε
⊢ ∃ a b,
    (a, b) ∈ H α ∧
      (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = [(Fs, δ ++ [β])]
Tactic:
use Fs, δ
Proof state after:
case h
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ) ∈ H α ∧
    (if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]) = [(Fs, δ ++ [β])]
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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_ε : ¬δ = ε
⊢ (Fs, δ) ∈ H α ∧
    (if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]) = [(Fs, δ ++ [β])]
Tactic:
simp_all
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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ [(Fs, δ ++ [β])]
Tactic:
simp_all
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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ evaluate M w (Con (Yset (Fs, δ ++ [β]) ψ))
Tactic:
simp [Yset, conEval, boxes_append] at *
Proof state after:
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), f ∈ Fs ∨ 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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), f ∈ Fs ∨ 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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
f : Formula
f_in : f ∈ Fs ∨ 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
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ)
⊢ evaluate M w f
Tactic:
apply w_Con
Proof state after:
case h.right.a
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ)
⊢ f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ)
Theorem: localDiamondTruth
Proof state before:
case h.right.a
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ)
⊢ f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ)
Tactic:
tauto
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mpr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
⊢ (∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))) → ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
rintro ⟨⟨Fs,δ⟩, ⟨Fδ_in, w_Con⟩⟩
Proof state after:
case mpr.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δ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case mpr.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:
simp [H] at Fδ_in
Proof state after:
case mpr.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Fδ_in :
  ∃ 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, δ) ∈ l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Fδ_in :
  ∃ 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, δ) ∈ l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
rcases Fδ_in with ⟨l, ⟨Gs, γ, ⟨Gγ_in, def_l⟩⟩, Gγ_in_l⟩
Proof state after:
case mpr.intro.mk.intro.intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
l : List (List Formula × List Program)
Gγ_in_l : (Fs, δ) ∈ l
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
def_l : (if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]) = l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.mk.intro.intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
l : List (List Formula × List Program)
Gγ_in_l : (Fs, δ) ∈ l
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
def_l : (if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]) = l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
subst def_l
Proof state after:
case mpr.intro.mk.intro.intro.intro.intro.intro.intro
ψ : 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, γ ++ [β])]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case mpr.intro.mk.intro.intro.intro.intro.intro.intro
ψ : 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, γ ++ [β])]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
cases em (γ = ε)
Proof state after:
case mpr.intro.mk.intro.intro.intro.intro.intro.intro.inl
ψ : 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, γ ++ [β])]
h✝ : γ = ε
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))

case mpr.intro.mk.intro.intro.intro.intro.intro.intro.inr
ψ : 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, γ ++ [β])]
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
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:
case inr δ_not_ε => simp_all
  cases Gγ_in_l
  subst_eqs
  simp_all [Yset, conEval, boxes_append]
  use Fs, γ
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, γ ++ [β])]
δ_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
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if ε = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, ε ++ [β])]
⊢ ∃ 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
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if ε = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, ε ++ [β])]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
simp at Gγ_in_l
Proof state after:
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
Gγ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Gs ∪ a, b)] = l) ∧ (Fs, δ) ∈ l
⊢ ∃ 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
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
Gγ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Gs ∪ a, b)] = l) ∧ (Fs, δ) ∈ l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
rcases Gγ_in_l with ⟨l, ⟨⟨aaa, bbb, ⟨_in_Hβ,def_l⟩ ⟩, Fsδ_in_l⟩ ⟩
Proof state after:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
l : List (List Formula × List Program)
Fsδ_in_l : (Fs, δ) ∈ l
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
def_l : [(Gs ∪ aaa, bbb)] = l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
l : List (List Formula × List Program)
Fsδ_in_l : (Fs, δ) ∈ l
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
def_l : [(Gs ∪ aaa, bbb)] = l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
subst def_l
Proof state after:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
Tactic:
simp
Proof state after:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case intro.intro.intro.intro.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ ∃ a b, (a, b) ∈ H α ∧ evaluate M w (Con (Yset (a, b) (⌈β⌉ψ)))
Tactic:
use Gs, ε
Proof state after:
case h
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ (Gs, ε) ∈ H α ∧ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case h
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ (Gs, ε) ∈ H α ∧ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Tactic:
constructor
Proof state after:
case h.left
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ (Gs, ε) ∈ H α

case h.right
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ (Gs, ε) ∈ H α
Tactic:
exact Gγ_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
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : (Fs, δ) ∈ [(Gs ∪ aaa, bbb)]
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Tactic:
simp at Fsδ_in_l
Proof state after:
case h.right
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : Fs = Gs ∪ aaa ∧ δ = bbb
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
Fsδ_in_l : Fs = Gs ∪ aaa ∧ δ = bbb
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Tactic:
cases Fsδ_in_l
Proof state after:
case h.right.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
left✝ : Fs = Gs ∪ aaa
right✝ : δ = bbb
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Theorem: localDiamondTruth
Proof state before:
case h.right.intro
ψ : 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
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
left✝ : Fs = Gs ∪ aaa
right✝ : δ = bbb
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Tactic:
subst_eqs
Proof state after:
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 β
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
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 β
⊢ evaluate M w (Con (Yset (Gs, ε) (⌈β⌉ψ)))
Tactic:
simp [conEval, Yset]
Proof state after:
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 ∈ Gs ∨ f = (~⌈β⌉ψ) → evaluate M w f
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 ∈ Gs ∨ f = (~⌈β⌉ψ) → evaluate M w f
Tactic:
intro f f_in
Proof state after:
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