internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
⊢ φ ∈ ↑Y
Tactic:
have := relateSeq_toChain' X_δ_Y δ_notEmpty
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
this : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Tactic:
rcases this with ⟨l, length_def, lchain⟩
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ φ ∈ ↑Y
Tactic:
suffices loadClaim : ∀ i : Fin (X :: l ++ [Y]).length,
    (⌈⌈δ.drop i⌉⌉φ) ∈ ((X :: l ++ [Y]).get i).val by
  specialize loadClaim (Fin.last _)
  simp [length_def] at loadClaim
  convert loadClaim
  have := @List.get_last _ Y (X :: l) (Fin.last _)
  simp_all [eq_comm]
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Tactic:
intro i
Proof state after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Theorem: loadedTruthLemmaProg
Proof state before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
Tactic:
exact loadClaimHelper length_def δφ_in_X lchain IHδ i
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
⊢ φ ∈ ↑Y
Tactic:
specialize loadClaim (Fin.last _)
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Y]).length)) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get (Fin.last (l.append [Y]).length))
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Y]).length)) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get (Fin.last (l.append [Y]).length))
⊢ φ ∈ ↑Y
Tactic:
simp [length_def] at loadClaim
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ φ ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ φ ∈ ↑Y
Tactic:
convert loadClaim
Proof state after:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Theorem: loadedTruthLemmaProg
Proof state before:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Tactic:
have := @List.get_last _ Y (X :: l) (Fin.last _)
Proof state after:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
this : ¬↑(Fin.last (l.append [Y]).length) < (X :: l).length → (X :: l ++ [Y]).get (Fin.last (l.append [Y]).length) = Y
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Theorem: loadedTruthLemmaProg
Proof state before:
case h.e'_5.h.e'_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
loadClaim : φ ∈ ↑((X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length))
this : ¬↑(Fin.last (l.append [Y]).length) < (X :: l).length → (X :: l ++ [Y]).get (Fin.last (l.append [Y]).length) = Y
⊢ Y = (X :: (l ++ [Y])).get (Fin.last (l ++ [Y]).length)
Tactic:
simp_all [eq_comm]
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
⊢ ∀ (X : { x // x ∈ Worlds }), ∀ P ∈ ↑X, evaluate (↑MG) X P
Tactic:
intro X P
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ P ∈ ↑X → evaluate (↑MG) X P
Theorem: truthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ P ∈ ↑X → evaluate (↑MG) X P
Tactic:
have ⟨claim, _⟩ := loadedTruthLemma MG X P
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
claim : P ∈ ↑X → evaluate (↑MG) X P
right✝ : (~P) ∈ ↑X → ¬evaluate (↑MG) X P
⊢ P ∈ ↑X → evaluate (↑MG) X P
Theorem: truthLemma
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
claim : P ∈ ↑X → evaluate (↑MG) X P
right✝ : (~P) ∈ ↑X → ¬evaluate (↑MG) X P
⊢ P ∈ ↑X → evaluate (↑MG) X P
Tactic:
exact claim
Proof state after:
no goals
Theorem: evalDis
Proof state before:
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ evaluate M w (f⋁g) ↔ evaluate M w f ∨ evaluate M w g
Tactic:
simp
Proof state after:
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ ¬evaluate M w f → evaluate M w g ↔ evaluate M w f ∨ evaluate M w g
Theorem: evalDis
Proof state before:
W : Type
M : KripkeModel W
f g : Formula
w : W
⊢ ¬evaluate M w f → evaluate M w g ↔ evaluate M w f ∨ evaluate M w g
Tactic:
tauto
Proof state after:
no goals
Theorem: notsatisfnotThenTaut
Proof state before:
⊢ ∀ (φ : Formula), ¬satisfiable (~φ) → tautology φ
Tactic:
intro phi
Proof state after:
phi : Formula
⊢ ¬satisfiable (~phi) → tautology phi
Theorem: notsatisfnotThenTaut
Proof state before:
phi : Formula
⊢ ¬satisfiable (~phi) → tautology phi
Tactic:
unfold satisfiable
Proof state after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → tautology phi
Theorem: notsatisfnotThenTaut
Proof state before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → tautology phi
Tactic:
unfold tautology
Proof state after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w phi
Theorem: notsatisfnotThenTaut
Proof state before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w phi
Tactic:
simp
Proof state after:
no goals
Theorem: subsetSat
Proof state before:
W : Type
M : KripkeModel W
w : W
X Y : List Formula
⊢ (∀ φ ∈ X, evaluate M w φ) → Y ⊆ X → ∀ φ ∈ Y, evaluate M w φ
Tactic:
aesop
Proof state after:
no goals
Theorem: semEquiv.transitive
Proof state before:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z
Tactic:
unfold semEquiv
Proof state after:
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w y ↔ evaluate M w z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w z