internlm/Lean-Github huggingface dataset:
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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
⊢ evaluate M w ρ
Tactic:
have := repl_w_ (~⌈⌈δ⌉⌉~ρ) (by simp)
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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
this : 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
this : evaluate M w (~⌈⌈δ⌉⌉~ρ)
⊢ evaluate M w ρ
Tactic:
simp [evalBoxes] at this
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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
this : ∃ x, relateSeq M δ w x ∧ evaluate M x ρ
⊢ 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
this : ∃ x, relateSeq M δ w x ∧ evaluate M x ρ
⊢ evaluate M w ρ
Tactic:
rcases this with ⟨v, w_ρ_v, v_ρ⟩
Proof state after:
case intro.intro
ψ : 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
v : W
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w ρ
Theorem: localDiamondTruth
Proof state before:
case intro.intro
ψ : 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
v : W
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w ρ
Tactic:
unfold_let ρ
Proof state after:
case intro.intro
ψ : 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
v : W
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Theorem: localDiamondTruth
Proof state before:
case intro.intro
ψ : 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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
v : W
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β))))
Tactic:
simp_all [disEval, helper]
Proof state after:
case intro.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ f, (∃ a b, (a, b) ∈ H (∗β) ∧ Con (Yset (a, b) ψ) = f) ∧ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case intro.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ f, (∃ a b, (a, b) ∈ H (∗β) ∧ Con (Yset (a, b) ψ) = f) ∧ evaluate M w f
Tactic:
simp [H]
Proof state after:
case intro.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ f,
    (∃ a b,
        (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
          Con (Yset (a, b) ψ) = f) ∧
      evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case intro.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ f,
    (∃ a b,
        (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
          Con (Yset (a, b) ψ) = f) ∧
      evaluate M w f
Tactic:
use Con (Yset (Fs, δ ++ [∗β]) ψ)
Proof state after:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (∃ a b,
      (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
        Con (Yset (a, b) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)) ∧
    evaluate M w (Con (Yset (Fs, δ ++ [∗β]) ψ))
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (∃ a b,
      (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
        Con (Yset (a, b) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)) ∧
    evaluate M w (Con (Yset (Fs, δ ++ [∗β]) ψ))
Tactic:
constructor
Proof state after:
case h.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ a b,
    (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
      Con (Yset (a, b) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)

case h.right
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ evaluate M w (Con (Yset (Fs, δ ++ [∗β]) ψ))
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 (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ∀ f ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs, evaluate M w f
⊢ (~⌈⌈δ⌉⌉~ρ) ∈ (~⌈⌈δ⌉⌉~ρ) :: Fs
Tactic:
simp
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ a b,
    (a = [] ∧ b = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
      Con (Yset (a, b) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)
Tactic:
use Fs, δ ++ [∗β]
Proof state after:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (Fs = [] ∧ δ ++ [∗β] = [] ∨
      ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l) ∧
    Con (Yset (Fs, δ ++ [∗β]) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (Fs = [] ∧ δ ++ [∗β] = [] ∨
      ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l) ∧
    Con (Yset (Fs, δ ++ [∗β]) ψ) = Con (Yset (Fs, δ ++ [∗β]) ψ)
Tactic:
simp_all
Proof state after:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Tactic:
use [(Fs, δ ++ [∗β])]
Proof state after:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]) ∧
    (Fs, δ ++ [∗β]) ∈ [(Fs, δ ++ [∗β])]
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]) ∧
    (Fs, δ ++ [∗β]) ∈ [(Fs, δ ++ [∗β])]
Tactic:
simp
Proof state after:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]