internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
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
Tactic:
simp [Xset] at 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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
⊢ φ ∈ ↑Y
Tactic:
have TP_eq : TP (∗β) = TP β := by simp [TP,testsOfProgram]
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
⊢ φ ∈ ↑Y
Tactic:
have X_ConF : evaluate MG.1 X (Con $ F β ℓ) := by
  rw [conEval]
  intro ψ ψ_in
  have _forTermination : lengthOfFormula ψ < lengthOfProgram (∗β) := by
    apply F_goes_down
    simp [F]
    convert ψ_in
  apply (loadedTruthLemma MG X ψ).1
  apply mysat; left; simp [F]; assumption
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ φ ∈ ↑Y
Tactic:
have := existsBoxFP β X_β_Z ℓ X_ConF
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
this :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq (↑MG) δ X Z
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
this :
  ∃
    δ ∈
      P β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    relateSeq (↑MG) δ X Z
⊢ φ ∈ ↑Y
Tactic:
rcases this with ⟨δ, δ_in_P, X_δ_Z⟩
Proof state after:
case intro.intro.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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro.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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
⊢ φ ∈ ↑Y
Tactic:
cases em (δ = [])
Proof state after:
case intro.intro.intro.intro.intro.intro.inl
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
h✝ : δ = []
⊢ φ ∈ ↑Y

case intro.intro.intro.intro.intro.intro.inr
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
h✝ : ¬δ = []
⊢ φ ∈ ↑Y
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
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
⊢ relate (↑MG) β X Z
Tactic:
specialize relSteps 0
Proof state after:
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
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ relate (↑MG) β X Z
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
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ relate (↑MG) β X Z
Tactic:
unfold_let Z
Proof state after:
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
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ relate (↑MG) β X (YS.get 1)
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
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ relate (↑MG) β X (YS.get 1)
Tactic:
convert relSteps
Proof state after:
case h.e'_4
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
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ X = YS.get (Fin.castSucc 0)
Theorem: loadedTruthLemmaProg
Proof state before:
case h.e'_4
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
Z : { x // x ∈ Worlds } := YS.get 1
relSteps : relate (↑MG) β (YS.get (Fin.castSucc 0)) (YS.get (Fin.succ 0))
⊢ X = YS.get (Fin.castSucc 0)
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
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
⊢ TP (∗β) = TP β
Tactic:
simp [TP,testsOfProgram]
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
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
⊢ evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
Tactic:
rw [conEval]
Proof state after:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
⊢ ∀
    f ∈
      F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    evaluate (↑MG) X f
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
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
⊢ ∀
    f ∈
      F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩,
    evaluate (↑MG) X f
Tactic:
intro ψ ψ_in
Proof state after:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ evaluate (↑MG) X ψ
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
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
⊢ evaluate (↑MG) X ψ
Tactic:
have _forTermination : lengthOfFormula ψ < lengthOfProgram (∗β) := by
  apply F_goes_down
  simp [F]
  convert ψ_in
Proof state after:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ evaluate (↑MG) X ψ
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
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ evaluate (↑MG) X ψ
Tactic:
apply (loadedTruthLemma MG X ψ).1
Proof state after:
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 : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
ψ : Formula
ψ_in :
  ψ ∈
    F β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
_forTermination : lengthOfFormula ψ < lengthOfProgram (∗β)
⊢ ψ ∈ ↑X