internlm/Lean-Github huggingface dataset:
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 → ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
specialize minus_Y nP_in_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 : ¬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 : ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
convert minus_Y
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
⊢ ∀ (X : { x // x ∈ Worlds }) (φ : Formula), (⌈α⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y
Tactic:
intro X φ boxP_in_X
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
⊢ ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
⊢ ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y
Tactic:
cases α_def : α <;> intro Y X_rel_Y
Proof state after:
case atom_prog
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : ℕ
α_def : α = ·a✝
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a✝) X Y
⊢ φ ∈ ↑Y

case sequence
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝¹ a✝ : Program
α_def : α = (a✝¹;'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (a✝¹;'a✝) X Y
⊢ φ ∈ ↑Y

case union
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝¹ a✝ : Program
α_def : α = (a✝¹⋓a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (a✝¹⋓a✝) X Y
⊢ φ ∈ ↑Y

case star
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Program
α_def : α = (∗a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (∗a✝) X Y
⊢ φ ∈ ↑Y

case test
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a : ℕ
α_def : α = ·a
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
⊢ φ ∈ ↑Y
Tactic:
case atom_prog a =>
  subst α_def
  simp only [instBot, relate] at X_rel_Y
  have ⟨_,⟨_,_,iii,_⟩⟩ := MG
  exact iii X Y _ _ X_rel_Y boxP_in_X
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a : ℕ
α_def : α = ·a
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
⊢ φ ∈ ↑Y
Tactic:
subst α_def
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Tactic:
simp only [instBot, relate] at X_rel_Y
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
X_rel_Y : (↑MG).Rel a X Y
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
X_rel_Y : (↑MG).Rel a X Y
⊢ φ ∈ ↑Y
Tactic:
have ⟨_,⟨_,_,iii,_⟩⟩ := MG
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ val✝.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q val✝.Rel α X Y ∧ (~P) ∈ ↑Y
X_rel_Y : (↑⟨val✝, ⋯⟩).Rel a X Y
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ val✝.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q val✝.Rel α X Y ∧ (~P) ∈ ↑Y
X_rel_Y : (↑⟨val✝, ⋯⟩).Rel a X Y
⊢ φ ∈ ↑Y
Tactic:
exact iii X Y _ _ X_rel_Y boxP_in_X
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
β : Program
α_def : α = (∗β)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (∗β) X Y
⊢ φ ∈ ↑Y
Tactic:
subst α_def
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (∗β) X Y
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (∗β) X Y
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Tactic:
simp at X_rel_Y
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : Relation.ReflTransGen (relate (↑MG) β) X Y
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : Relation.ReflTransGen (relate (↑MG) β) X Y
⊢ φ ∈ ↑Y
Tactic:
rw [ReflTransGen.iff_finitelyManySteps] at X_rel_Y
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : ∃ n ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : ∃ n ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
rcases X_rel_Y with ⟨n, claim⟩
Proof state after:
case intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
n : ℕ
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
n : ℕ
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
induction n generalizing X φ
Proof state after:
case intro.zero
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin 0), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y

case intro.succ
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
n✝ : ℕ
a✝ :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n✝), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin (n✝ + 1)), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin 0), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
rcases claim with ⟨YS, X_def, Y_def, _⟩
Proof state after:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
have : YS.head = YS.last := by
  have := Vector.exists_eq_cons YS
  aesop
Proof state after:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
⊢ φ ∈ ↑Y
Tactic:
rw [this] at X_def
Proof state after:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.last
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.last
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
⊢ φ ∈ ↑Y
Tactic:
subst X_def Y_def
Proof state after:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
⊢ φ ∈ ↑YS.last
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
⊢ φ ∈ ↑YS.last
Tactic:
have := ((MG.2.1 (YS.last)).1 φ φ (∗β)).right.right.right.left boxP_in_X
Proof state after:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this✝ : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
this : ∃ l, ((Xset (∗β) l φ).all fun y => decide (y ∈ ↑YS.last)) = true
⊢ φ ∈ ↑YS.last
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this✝ : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
this : ∃ l, ((Xset (∗β) l φ).all fun y => decide (y ∈ ↑YS.last)) = true
⊢ φ ∈ ↑YS.last
Tactic:
rcases this with ⟨ℓ, mysat⟩
Proof state after:
case intro.zero.intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
ℓ : TP (∗β)
mysat : ((Xset (∗β) ℓ φ).all fun y => decide (y ∈ ↑YS.last)) = true
⊢ φ ∈ ↑YS.last
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.zero.intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
ℓ : TP (∗β)
mysat : ((Xset (∗β) ℓ φ).all fun y => decide (y ∈ ↑YS.last)) = true
⊢ φ ∈ ↑YS.last
Tactic:
simp_all [Xset, F, P]
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ YS.head = YS.last
Tactic:
have := Vector.exists_eq_cons YS
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : ∃ a as, YS = a ::ᵥ as
⊢ YS.head = YS.last
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : ∃ a as, YS = a ::ᵥ as
⊢ YS.head = YS.last
Tactic:
aesop
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin (m + 1)), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
rcases claim with ⟨YS, X_def, Y_def, relSteps⟩
Proof state after:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ φ ∈ ↑Y
Tactic:
let Z := YS.get 1
Proof state after:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
⊢ φ ∈ ↑Y
Tactic:
have X_β_Z : relate MG.1 β X Z := by
  specialize relSteps 0
  unfold_let Z
  unfold_let X
  convert relSteps
  aesop
Proof state after:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
⊢ φ ∈ ↑Y
Tactic:
have := ((MG.2.1 X).1 φ φ (∗β)).right.right.right.left boxP_in_X
Proof state after:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
this : ∃ l, ((Xset (∗β) l φ).all fun y => decide (y ∈ ↑X)) = true
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
this : ∃ l, ((Xset (∗β) l φ).all fun y => decide (y ∈ ↑X)) = true
⊢ φ ∈ ↑Y
Tactic:
rcases this with ⟨ℓ, mysat⟩
Proof state after:
case intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ((Xset (∗β) ℓ φ).all fun y => decide (y ∈ ↑X)) = true
⊢ φ ∈ ↑Y