internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
⊢ (Fs, δ) ∈ H β ∧ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
constructor
Proof state after:
case h.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
⊢ (Fs, δ) ∈ H β

case h.right
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case h.left
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
⊢ (Fs, δ) ∈ H β
Tactic:
exact Fδ_in
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case h.right
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
cases em (δ = ε)
Proof state after:
case h.right.inl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
h✝ : δ = ε
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f

case h.right.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
h✝ : ¬δ = ε
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
δ_is_ε : δ = ε
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
case inl δ_is_ε => exfalso; simp_all
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
δ_is_ε : δ = ε
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
exfalso
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
δ_is_ε : δ = ε
⊢ False
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
δ_is_ε : δ = ε
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : evaluate M w (if δ = [] then Formula.bottom else Con ((~⌈⌈δ⌉⌉~·x) :: Fs))
δ_notEmpty : ¬δ = ε
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
simp_all [conEval]
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x) → evaluate M w f
Tactic:
intro f f_in
Proof state after:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
f_in : f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉~·x)
⊢ evaluate M w f
Tactic:
cases f_in
Proof state after:
case inl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M w f

case inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f = (~⌈⌈δ⌉⌉~·x)
⊢ evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case inl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M w f
Tactic:
apply w_.2
Proof state after:
case inl.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f ∈ Fs
⊢ f ∈ Fs
Theorem: localDiamondTruth
Proof state before:
case inl.a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f ∈ Fs
⊢ f ∈ Fs
Tactic:
assumption
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
f : Formula
h✝ : f = (~⌈⌈δ⌉⌉~·x)
⊢ evaluate M w f
Tactic:
subst_eqs
Proof state after:
case inr.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ evaluate M w (~⌈⌈δ⌉⌉~·x)
Theorem: localDiamondTruth
Proof state before:
case inr.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ evaluate M w (~⌈⌈δ⌉⌉~·x)
Tactic:
simp
Proof state after:
case inr.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ ¬evaluate M w (⌈⌈δ⌉⌉~·x)
Theorem: localDiamondTruth
Proof state before:
case inr.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
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 β
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
w_ : ¬evaluate M w (⌈⌈δ⌉⌉~·x) ∧ ∀ a ∈ Fs, evaluate M w a
δ_notEmpty : ¬δ = []
⊢ ¬evaluate M w (⌈⌈δ⌉⌉~·x)
Tactic:
exact w_.1
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mp.repl_imp_rho
ψ : 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
⊢ evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
Tactic:
unfold_let σ1
Proof state after:
case mp.repl_imp_rho
ψ : 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
⊢ evaluate M w
      (repl_in_F x ρ
        (dis
          (List.map
            (fun x_1 =>
              match x_1 with
              | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
            (H β)))) →
    evaluate M w ρ