internlm/Lean-Github huggingface dataset:
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ ∀ (x : Finset Formula) (x_1 : x ∈ Worlds),
    Q (↑MG).Rel α X ⟨x, x_1⟩ →
      Q (↑MG).Rel β ⟨x, x_1⟩ Y → ∃ a, ∃ (b : a ∈ Worlds), relate (↑MG) α X ⟨a, b⟩ ∧ relate (↑MG) β ⟨a, b⟩ Y
Tactic:
tauto
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
have := Q_then_relate MG α
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
have := Q_then_relate MG β
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
simp only [instBot, Subtype.forall, Q, relate] at *
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ Q (↑MG).Rel α X Y ∨ Q (↑MG).Rel β X Y → relate (↑MG) α X Y ∨ relate (↑MG) β X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ Q (↑MG).Rel α X Y ∨ Q (↑MG).Rel β X Y → relate (↑MG) α X Y ∨ relate (↑MG) β X Y
Tactic:
tauto
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Q (↑MG).Rel (∗α) X Y → relate (↑MG) (∗α) X Y
Tactic:
simp only [instBot, Q, relate]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Relation.ReflTransGen (Q (↑MG).Rel α) X Y → Relation.ReflTransGen (relate (↑MG) α) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Relation.ReflTransGen (Q (↑MG).Rel α) X Y → Relation.ReflTransGen (relate (↑MG) α) X Y
Tactic:
apply Relation.ReflTransGen.lift
Proof state after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ ∀ (a b : { x // x ∈ Worlds }), Q (↑MG).Rel α a b → relate (↑MG) α a b
Theorem: Q_then_relate
Proof state before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ ∀ (a b : { x // x ∈ Worlds }), Q (↑MG).Rel α a b → relate (↑MG) α a b
Tactic:
intro a b Qab
Proof state after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
a b : { x // x ∈ Worlds }
Qab : Q (↑MG).Rel α a b
⊢ relate (↑MG) α a b
Theorem: Q_then_relate
Proof state before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
a b : { x // x ∈ Worlds }
Qab : Q (↑MG).Rel α a b
⊢ relate (↑MG) α a b
Tactic:
exact Q_then_relate MG α a b Qab
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Tactic:
have := loadedTruthLemma MG X φ
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Tactic:
simp [Q, relate, Relation.Comp] at *
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ X = Y → φ ∈ ↑X → X = Y ∧ evaluate (↑MG) X φ
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ X = Y → φ ∈ ↑X → X = Y ∧ evaluate (↑MG) X φ
Tactic:
intro X_is_Y phi_in_X
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
X_is_Y : X = Y
phi_in_X : φ ∈ ↑X
⊢ X = Y ∧ evaluate (↑MG) X φ
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
X_is_Y : X = Y
phi_in_X : φ ∈ ↑X
⊢ X = Y ∧ evaluate (↑MG) X φ
Tactic:
subst X_is_Y
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X ∧ evaluate (↑MG) X φ
Theorem: Q_then_relate
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X ∧ evaluate (↑MG) X φ
Tactic:
constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ evaluate (↑MG) X φ
Theorem: Q_then_relate
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X
Tactic:
tauto
Proof state after:
no goals
Theorem: Q_then_relate
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ evaluate (↑MG) X φ
Tactic:
tauto
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ ∀ (P : Formula), (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Tactic:
intro P
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Tactic:
cases P
Proof state after:
case bottom
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)

case atom_prop
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : ℕ
⊢ ((·a✝) ∈ ↑X → evaluate (↑MG) X (·a✝)) ∧ ((~·a✝) ∈ ↑X → ¬evaluate (↑MG) X (·a✝))

case neg
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : Formula
⊢ ((~a✝) ∈ ↑X → evaluate (↑MG) X (~a✝)) ∧ ((~~a✝) ∈ ↑X → ¬evaluate (↑MG) X (~a✝))

case and
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ a✝ : Formula
⊢ (a✝¹⋀a✝ ∈ ↑X → evaluate (↑MG) X (a✝¹⋀a✝)) ∧ ((~a✝¹⋀a✝) ∈ ↑X → ¬evaluate (↑MG) X (a✝¹⋀a✝))

case box
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ : Program
a✝ : Formula
⊢ ((⌈a✝¹⌉a✝) ∈ ↑X → evaluate (↑MG) X (⌈a✝¹⌉a✝)) ∧ ((~⌈a✝¹⌉a✝) ∈ ↑X → ¬evaluate (↑MG) X (⌈a✝¹⌉a✝))
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)
Tactic:
repeat' constructor
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ bottom ∈ ↑X → evaluate (↑MG) X bottom

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

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ bottom ∈ ↑X → evaluate (↑MG) X bottom
Tactic:
intro P_in_X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ evaluate (↑MG) X bottom
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ evaluate (↑MG) X bottom
Tactic:
apply absurd P_in_X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ bottom ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ bottom ∉ ↑X
Tactic:
have ⟨_,⟨i,_,_,_⟩⟩ := MG
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
⊢ bottom ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
⊢ bottom ∉ ↑X
Tactic:
specialize i X
Proof state after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
i : saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ bottom ∉ ↑X
Theorem: loadedTruthLemma
Proof state before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
i : saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ bottom ∉ ↑X
Tactic:
tauto
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom
Tactic:
simp only [instBot, evaluate, not_false_eq_true, implies_true]
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
⊢ ((·pp) ∈ ↑X → evaluate (↑MG) X (·pp)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑MG) X (·pp))
Tactic:
have ⟨M,⟨i,ii,_,_⟩⟩ := MG
Proof state after:
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)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))
Theorem: loadedTruthLemma
Proof state before:
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)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))
Tactic:
repeat' constructor
Proof state after:
case left
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)

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)
Theorem: loadedTruthLemma
Proof state before:
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)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))
Tactic:
constructor
Proof state after:
case left
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)

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)
Theorem: loadedTruthLemma
Proof state before:
case left
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 P_in_X
Proof state after:
case left
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
P_in_X : (·pp) ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (·pp)
Theorem: loadedTruthLemma
Proof state before:
case left
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
P_in_X : (·pp) ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
simp only [evaluate]
Proof state after:
case left
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
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp
Theorem: loadedTruthLemma
Proof state before:
case left
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
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp
Tactic:
rw [ii X pp] at P_in_X
Proof state after:
case left
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
P_in_X : M.val X pp
⊢ M.val X pp
Theorem: loadedTruthLemma
Proof state before:
case left
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
P_in_X : M.val X pp
⊢ M.val X pp
Tactic:
exact P_in_X
Proof state after:
no goals