internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
have := relateSeq_toChain' X_δ_Z δ_notEmpty
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
rcases this with ⟨l, length_def, lchain⟩
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
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]
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ ∀ (i : Fin (X :: l ++ [Z]).length), (⌈⌈List.drop (↑i) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get i)
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
⊢ ∀ (i : Fin (X :: l ++ [Z]).length), (⌈⌈List.drop (↑i) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get i)
Tactic:
intro i
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
i : Fin (X :: l ++ [Z]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get i)
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
i : Fin (X :: l ++ [Z]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get i)
Tactic:
exact loadClaimHelper length_def δβSφ_in_X lchain IHδ i
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
⊢ ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
Tactic:
intro d d_in_δ X' Y' φ' dφ_in_X' X'_d_Y'
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'
Tactic:
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
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
_forTermination : lengthOf d < lengthOf (∗β)
⊢ φ' ∈ ↑Y'
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
_forTermination : lengthOf d < lengthOf (∗β)
⊢ φ' ∈ ↑Y'
Tactic:
exact loadedTruthLemmaProg MG d X' φ' dφ_in_X' Y' X'_d_Y'
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ lengthOf d < lengthOf (∗β)
Tactic:
have := P_goes_down d_in_δ δ_in_P
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic β = true then d = β
  else if isStar β = true then lengthOfProgram d ≤ lengthOfProgram β else lengthOfProgram d < lengthOfProgram β
⊢ lengthOf d < lengthOf (∗β)
Theorem: loadedTruthLemmaProg
Proof state before:
case inr.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
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
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic β = true then d = β
  else if isStar β = true then lengthOfProgram d ≤ lengthOfProgram β else lengthOfProgram d < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOf d < lengthOf (∗β)
Tactic:
simp_all [P]
Proof state after:
case inr.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
d : Program
X' Y' : { x // x ∈ Worlds }
φ' : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
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)
X_β_Z : relate (↑MG) β YS.head Z
mysat :
  ∀ (x : Formula),
    (x ∈ F (∗β) ℓ ∨ φ = x ∨ ∃ a ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩), (⌈⌈a ++ [∗β]⌉⌉φ) = x) →
      x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
d_in_δ : d ∈ δ
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this : lengthOfProgram d < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram d < 1 + lengthOfProgram β
Theorem: loadedTruthLemmaProg
Proof state before:
case inr.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
d : Program
X' Y' : { x // x ∈ Worlds }
φ' : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
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)
X_β_Z : relate (↑MG) β YS.head Z
mysat :
  ∀ (x : Formula),
    (x ∈ F (∗β) ℓ ∨ φ = x ∨ ∃ a ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩), (⌈⌈a ++ [∗β]⌉⌉φ) = x) →
      x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
d_in_δ : d ∈ δ
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this : lengthOfProgram d < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram d < 1 + lengthOfProgram β
Tactic:
try linarith
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case inr.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
d : Program
X' Y' : { x // x ∈ Worlds }
φ' : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
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)
X_β_Z : relate (↑MG) β YS.head Z
mysat :
  ∀ (x : Formula),
    (x ∈ F (∗β) ℓ ∨ φ = x ∨ ∃ a ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩), (⌈⌈a ++ [∗β]⌉⌉φ) = x) →
      x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
d_in_δ : d ∈ δ
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this : lengthOfProgram d < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram d < 1 + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals