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'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim : ∀ (i : Fin (X :: l ++ [Z]).length), (⌈⌈List.drop (↑i) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get i)
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
specialize loadClaim (Fin.last _)
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'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Z]).length)) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get (Fin.last (l.append [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑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'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Z]).length)) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get (Fin.last (l.append [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
simp [length_def] at loadClaim
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'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑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'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Tactic:
convert loadClaim
Proof state after:
case h.e'_5.h.e'_3
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]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
⊢ Z = (X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length)
Theorem: loadedTruthLemmaProg
Proof state before:
case h.e'_5.h.e'_3
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]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
⊢ Z = (X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length)
Tactic:
have := @List.get_last _ Z (X :: l) (Fin.last _)
Proof state after:
case h.e'_5.h.e'_3
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]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
this : ¬↑(Fin.last (l.append [Z]).length) < (X :: l).length → (X :: l ++ [Z]).get (Fin.last (l.append [Z]).length) = Z
⊢ Z = (X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length)
Theorem: loadedTruthLemmaProg
Proof state before:
case h.e'_5.h.e'_3
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]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
this : ¬↑(Fin.last (l.append [Z]).length) < (X :: l).length → (X :: l ++ [Z]).get (Fin.last (l.append [Z]).length) = Z
⊢ Z = (X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length)
Tactic:
simp_all [eq_comm]
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ Z = YS.tail.head
Tactic:
unfold_let Z
Proof state after:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.tail.head
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.tail.head
Tactic:
rw [← Vector.get_zero]
Proof state after:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.tail.get 0
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.tail.get 0
Tactic:
rw [Vector.get_tail_succ]
Proof state after:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.get (Fin.succ 0)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.get (Fin.succ 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_2
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.last = YS.tail.last
Tactic:
rw [Vector.last_def, Vector.last_def]
Proof state after:
case refine_2
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get (Fin.last (m + 1)) = YS.tail.get (Fin.last m)
Theorem: loadedTruthLemmaProg
Proof state before:
case refine_2
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get (Fin.last (m + 1)) = 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 : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get (Fin.last (m + 1)) = 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 : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get (Fin.last (m + 1)) = YS.get (Fin.last m).succ
Tactic:
rfl
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 : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑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 : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
i : Fin m
⊢ relate (↑MG) β (YS.tail.get i.castSucc) (YS.tail.get i.succ)