internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
intro notP_in_X
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (·pp)
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
simp only [evaluate]
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp
Tactic:
rw [← ii X pp]
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
rcases i X with ⟨_, _, P_in_then_notP_not_in⟩
Proof state after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
specialize P_in_then_notP_not_in pp
Proof state after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
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
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
tauto
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
have ⟨plus,minus⟩ := loadedTruthLemma MG X Q
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
repeat' constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)
Tactic:
intro notQ_in_X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ evaluate (↑MG) X (~Q)
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ evaluate (↑MG) X (~Q)
Tactic:
simp only [evaluate]
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X Q
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X Q
Tactic:
exact minus notQ_in_X
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)
Tactic:
intro notnotQ_in_X
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X (~Q)
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X (~Q)
Tactic:
simp only [instBot, evaluate, not_not]
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ evaluate (↑MG) X Q
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ evaluate (↑MG) X Q
Tactic:
have ⟨M,⟨i,_,_,_⟩⟩ := MG
Proof state after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
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
left✝ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
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
left✝ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
rcases i X with ⟨X_saturated, _, _⟩
Proof state after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
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
left✝¹ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Theorem: loadedTruthLemma
Proof state before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
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
left✝¹ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
exact plus ((X_saturated Q Q (?'Q)).1 notnotQ_in_X)
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨plus_Q, minus_Q⟩ := loadedTruthLemma MG X Q
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨plus_R, minus_R⟩ := loadedTruthLemma MG X R
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
plus_R : R ∈ ↑X → evaluate (↑MG) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑MG) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
plus_R : R ∈ ↑X → evaluate (↑MG) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑MG) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨M,⟨i,_,iii,_⟩⟩ := MG
Proof state after:
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
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Theorem: loadedTruthLemma
Proof state before:
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
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
rcases i X with ⟨X_saturated, _, _⟩
Proof state after:
case intro.intro
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
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Theorem: loadedTruthLemma
Proof state before:
case intro.intro
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
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
rcases X_saturated Q R (?'Q) with ⟨_, ⟨andSplit, ⟨notAndSplit, _⟩⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
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
notAndSplit : (~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)
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left
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
notAndSplit : (~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)
⊢ Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
intro QandR_in_X
Proof state after:
case intro.intro.intro.intro.intro.left
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
notAndSplit : (~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)
QandR_in_X : Q⋀R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)