internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_2
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ Y = YS.tail.get (Fin.last m)
Tactic:
rw [Vector.get_tail_succ]
Proof state after:
case refine_2
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ Y = YS.get (Fin.last m).succ
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_2
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ Y = YS.get (Fin.last m).succ
Tactic:
aesop
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
⊢ ∀ (i : Fin m), relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Tactic:
intro i
Proof state after:
case refine_3
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
i : Fin m
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
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, ⋯⟩))
δ_in_P :
  [] ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : X = Z
i : Fin m
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Tactic:
clear * -relSteps
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
i : Fin m
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
i : Fin m
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Tactic:
specialize relSteps i.succ
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Tactic:
have : ((Vector.tail YS).get i.castSucc) = (YS.get ((Fin.succ i).castSucc)) := by aesop
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.castSucc = YS.get i.succ.castSucc
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.castSucc = YS.get i.succ.castSucc
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)
Tactic:
rw [this]
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.castSucc = YS.get i.succ.castSucc
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.castSucc = YS.get i.succ.castSucc
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Tactic:
clear this
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Tactic:
have : ((Vector.tail YS).get i.succ) = (YS.get ((Fin.succ i).succ)) := by aesop
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.succ = YS.get i.succ.succ
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.succ = YS.get i.succ.succ
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
Tactic:
rw [this]
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.succ = YS.get i.succ.succ
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.succ = YS.get i.succ.succ
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
Tactic:
clear this
Proof state after:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
Tactic:
exact relSteps
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ YS.tail.get i.castSucc = YS.get i.succ.castSucc
Tactic:
aesop
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ YS.tail.get i.succ = YS.get i.succ.succ
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_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
δ_notEmpty : ¬δ = []
⊢ φ ∈ ↑Y
Tactic:
have : (δ ++ [∗β]) ∈ P (∗β) ℓ := by
  simp [P]
  apply List.mem_filter_of_mem
  all_goals simp_all
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 β
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
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
⊢ φ ∈ ↑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
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
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
⊢ φ ∈ ↑Y
Tactic:
have δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ X.1 := by
  apply mysat
  right
  use δ ++ [∗β]
  simp_all [boxes_append]
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 β
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
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
⊢ φ ∈ ↑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
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
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Tactic:
have : (⌈∗β⌉φ) ∈ Z.1 := by
  clear innerIH
  have IHδ : ∀ d ∈ δ, ∀ (X' Y' : Worlds),
      ∀ φ', (⌈d⌉φ') ∈ X'.val → relate MG.val d X' Y' → φ' ∈ Y'.val := by
    intro d d_in_δ X' Y' φ' dφ_in_X' X'_d_Y'
    have _forTermination : lengthOf d < lengthOf (∗β) := by
      have := P_goes_down d_in_δ δ_in_P
      cases em (isAtomic β) <;> cases em (isStar β)
      all_goals
        simp_all [P]
        try linarith
    exact loadedTruthLemmaProg MG d X' φ' dφ_in_X' Y' X'_d_Y'
  have := relateSeq_toChain' X_δ_Z δ_notEmpty
  rcases this with ⟨l, length_def, lchain⟩
  suffices loadClaim : ∀ i : Fin (X :: l ++ [Z]).length,
      (⌈⌈δ.drop i⌉⌉⌈∗β⌉φ) ∈ ((X :: l ++ [Z]).get i).val by
    specialize loadClaim (Fin.last _)
    simp [length_def] at loadClaim
    convert loadClaim
    have := @List.get_last _ Z (X :: l) (Fin.last _)
    simp_all [eq_comm]
  intro i
  exact loadClaimHelper length_def δβSφ_in_X lchain IHδ i
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 β
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
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ φ ∈ ↑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
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
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ φ ∈ ↑Y
Tactic:
apply innerIH Z _ this
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 β
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
δ_notEmpty : ¬δ = []
this✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ ∃ ys, Z = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)