internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
right
Proof state after:
case intro.intro.intro.intro.intro.right.inr.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X R
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right.inr.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
exact minus_R notR_in_X
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ ((⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)) ∧ ((~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P))
Tactic:
repeat' constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Tactic:
all_goals simp
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → ∀ (a_2 : Finset Formula) (b : a_2 ∈ Worlds), relate (↑MG) a X ⟨a_2, b⟩ → evaluate ↑MG ⟨a_2, b⟩ P

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ ((⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)) ∧ ((~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P))
Tactic:
constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Tactic:
simp
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → ∀ (a_2 : Finset Formula) (b : a_2 ∈ Worlds), relate (↑MG) a X ⟨a_2, b⟩ → evaluate ↑MG ⟨a_2, b⟩ P
Tactic:
intro boxP_in_X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
⊢ ∀ (a_1 : Finset Formula) (b : a_1 ∈ Worlds), relate (↑MG) a X ⟨a_1, b⟩ → evaluate ↑MG ⟨a_1, b⟩ P
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
⊢ ∀ (a_1 : Finset Formula) (b : a_1 ∈ Worlds), relate (↑MG) a X ⟨a_1, b⟩ → evaluate ↑MG ⟨a_1, b⟩ P
Tactic:
intro Y Y_in X_rel_Y
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
have ⟨plus_Y, _⟩ := loadedTruthLemma MG ⟨Y, Y_in⟩ P
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
have oh_a := loadedTruthLemmaProg MG a X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
apply plus_Y
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ P ∈ ↑⟨Y, Y_in⟩
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ P ∈ ↑⟨Y, Y_in⟩
Tactic:
apply oh_a P boxP_in_X ⟨Y,Y_in⟩ X_rel_Y
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Tactic:
intro notBoxP_in_X
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Tactic:
have ⟨M,⟨i,ii,iii,iv⟩⟩ := MG
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
have my_iv := iv X a P notBoxP_in_X
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
my_iv : ∃ Y, Q M.Rel a X Y ∧ (~P) ∈ ↑Y
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
my_iv : ∃ Y, Q M.Rel a X Y ∧ (~P) ∈ ↑Y
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
rcases my_iv with ⟨⟨Y, Y_in⟩, X_a_Y, nP_in_Y⟩
Proof state after:
case right.intro.mk.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case right.intro.mk.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
use Y, Y_in
Proof state after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
constructor
Proof state after:
case h.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩

case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case h.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩
Tactic:
exact Q_then_relate ⟨M,⟨i,ii,iii,iv⟩⟩ a X ⟨Y,Y_in⟩ X_a_Y
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
have ⟨_, minus_Y⟩ := loadedTruthLemma ⟨M,⟨i,ii,iii,iv⟩⟩ ⟨Y, Y_in⟩ P
Proof state after:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Theorem: loadedTruthLemma
Proof state before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
simp only at minus_Y
Proof state after:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ Y → ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P