internlm/Lean-Github huggingface dataset:
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
simp at negLoad_in
Proof state after:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in :
  O =
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)) ∨
    O =
      some
        (Sum.inr
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ))
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in :
  O =
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)) ∨
    O =
      some
        (Sum.inr
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ))
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
cases negLoad_in
Proof state after:
case inl
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
h✝ :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case inr
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
hyp :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
case inl hyp => subst hyp; sorry
Proof state after:
no goals
Theorem: loadedDiamondPaths
Proof state before:
case inr
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
all_goals sorry
Proof state after:
no goals
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
hyp :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
subst hyp
Proof state after:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
v_X :
  (M, v)⊨(L, R,
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
v_X :
  (M, v)⊨(L, R,
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
sorry
Proof state after:
no goals
Theorem: loadedDiamondPaths
Proof state before:
case inr
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
sorry
Proof state after:
no goals
Theorem: loadedDiamondPaths
Proof state before:
case rep
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔNode : TNode
ΔHist : LoadHistory
rep✝ : condSixRepeat ΔNode ΔHist
h : some ⟨ΔNode, ⟨ΔHist, ClosedTableau.rep rep✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
sorry
Proof state after:
no goals
Theorem: tableauThenNotSat
Proof state before:
⊢ ∀ (X : TNode), ClosedTableau LoadHistory.nil X → ¬satisfiable X
Tactic:
intro X t
Proof state after:
X : TNode
t : ClosedTableau LoadHistory.nil X
⊢ ¬satisfiable X
Theorem: tableauThenNotSat
Proof state before:
X : TNode
t : ClosedTableau LoadHistory.nil X
⊢ ¬satisfiable X
Tactic:
sorry
Proof state after:
no goals
Theorem: correctness
Proof state before:
⊢ ∀ (LR : TNode), satisfiable LR → consistent LR
Tactic:
intro LR
Proof state after:
LR : TNode
⊢ satisfiable LR → consistent LR
Theorem: correctness
Proof state before:
LR : TNode
⊢ satisfiable LR → consistent LR
Tactic:
contrapose
Proof state after:
LR : TNode
⊢ ¬consistent LR → ¬satisfiable LR
Theorem: correctness
Proof state before:
LR : TNode
⊢ ¬consistent LR → ¬satisfiable LR
Tactic:
unfold consistent
Proof state after:
LR : TNode
⊢ (¬let LR := LR;
      ¬inconsistent LR) →
    ¬satisfiable LR
Theorem: correctness
Proof state before:
LR : TNode
⊢ (¬let LR := LR;
      ¬inconsistent LR) →
    ¬satisfiable LR
Tactic:
unfold inconsistent
Proof state after:
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR
Theorem: correctness
Proof state before:
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR
Tactic:
simp only [not_nonempty_iff, not_isEmpty_iff, not_exists, not_forall, exists_prop, Nonempty.forall]
Proof state after:
LR : TNode
⊢ ClosedTableau LoadHistory.nil LR → ¬satisfiable LR
Theorem: correctness
Proof state before:
LR : TNode
⊢ ClosedTableau LoadHistory.nil LR → ¬satisfiable LR
Tactic:
intro hyp
Proof state after:
LR : TNode
hyp : ClosedTableau LoadHistory.nil LR
⊢ ¬satisfiable LR
Theorem: correctness
Proof state before:
LR : TNode
hyp : ClosedTableau LoadHistory.nil LR
⊢ ¬satisfiable LR
Tactic:
apply tableauThenNotSat LR hyp
Proof state after:
no goals
Theorem: soundTableau
Proof state before:
⊢ ∀ (φ : Formula), provable φ → ¬satisfiable {~φ}
Tactic:
intro φ prov
Proof state after:
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Theorem: soundTableau
Proof state before:
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Tactic:
rcases prov with ⟨tabl⟩|⟨tabl⟩
Proof state after:
case byTableauL
φ : Formula
tabl : ClosedTableau ([], []) ([~φ], [], none)
⊢ ¬satisfiable {~φ}

case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Theorem: soundTableau
Proof state before:
case byTableauL
φ : Formula
tabl : ClosedTableau ([], []) ([~φ], [], none)
⊢ ¬satisfiable {~φ}

case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Tactic:
exact tableauThenNotSat ([~φ], [], none) tabl
Proof state after:
case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Theorem: soundTableau
Proof state before:
case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Tactic:
exact tableauThenNotSat ([], [~φ], none) tabl
Proof state after:
no goals
Theorem: soundness
Proof state before:
⊢ ∀ (φ : Formula), provable φ → tautology φ
Tactic:
intro φ prov
Proof state after:
φ : Formula
prov : provable φ
⊢ tautology φ
Theorem: soundness
Proof state before:
φ : Formula
prov : provable φ
⊢ tautology φ
Tactic:
apply notsatisfnotThenTaut
Proof state after:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable (~φ)
Theorem: soundness
Proof state before:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable (~φ)
Tactic:
rw [← singletonSat_iff_sat]
Proof state after:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Theorem: soundness
Proof state before:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Tactic:
apply soundTableau
Proof state after:
case a.a
φ : Formula
prov : provable φ
⊢ provable φ
Theorem: soundness
Proof state before:
case a.a
φ : Formula
prov : provable φ
⊢ provable φ
Tactic:
exact prov
Proof state after:
no goals
Theorem: conempty
Proof state before:
⊢ Con ∅ = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: consingle
Proof state before:
f : Formula
⊢ Con [f] = f
Tactic:
rfl
Proof state after:
no goals
Theorem: listEq_to_conEq
Proof state before:
l1 l2 : List Formula
⊢ l1 = l2 → Con l1 = Con l2
Tactic:
aesop
Proof state after:
no goals
Theorem: listEq_to_disEq
Proof state before:
l1 l2 : List Formula
⊢ l1 = l2 → dis l1 = dis l2
Tactic:
aesop
Proof state after:
no goals
Theorem: conEvalHT
Proof state before:
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)
Tactic:
induction' X with g X _
Proof state after:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [f]) ↔ evaluate M w f ∧ evaluate M w (Con [])

case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
tail_ih✝ : evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)
⊢ evaluate M w (Con (f :: g :: X)) ↔ evaluate M w f ∧ evaluate M w (Con (g :: X))
Theorem: conEvalHT
Proof state before:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [f]) ↔ evaluate M w f ∧ evaluate M w (Con [])
Tactic:
simp
Proof state after:
no goals
Theorem: conEvalHT
Proof state before:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
tail_ih✝ : evaluate M w (Con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (Con X)
⊢ evaluate M w (Con (f :: g :: X)) ↔ evaluate M w f ∧ evaluate M w (Con (g :: X))
Tactic:
simp
Proof state after:
no goals
Theorem: conEval
Proof state before:
W : Type
M : KripkeModel W
X : List Formula
w : W
⊢ evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
Tactic:
induction' X with f X IH
Proof state after:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con []) ↔ ∀ f ∈ [], evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w (Con (f :: X)) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Theorem: conEval
Proof state before:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con []) ↔ ∀ f ∈ [], evaluate M w f
Tactic:
simp
Proof state after:
no goals
Theorem: conEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w (Con (f :: X)) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
rw [conEvalHT]
Proof state after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f ∧ evaluate M w (Con X) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Theorem: conEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f ∧ evaluate M w (Con X) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
simp
Proof state after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f → (evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a)
Theorem: conEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f → (evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a)
Tactic:
intro _
Proof state after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
a✝ : evaluate M w f
⊢ evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a
Theorem: conEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
a✝ : evaluate M w f
⊢ evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a
Tactic:
assumption
Proof state after:
no goals
Theorem: disEvalHT
Proof state before:
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
Tactic:
induction' X with g X IH
Proof state after:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis [f]) ↔ evaluate M w f ∨ evaluate M w (dis [])

case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ evaluate M w (dis (f :: g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Theorem: disEvalHT
Proof state before:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis [f]) ↔ evaluate M w f ∨ evaluate M w (dis [])
Tactic:
simp
Proof state after:
no goals
Theorem: disEvalHT
Proof state before:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ evaluate M w (dis (f :: g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Tactic:
simp
Proof state after:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ ¬evaluate M w f → evaluate M w (dis (g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Theorem: disEvalHT
Proof state before:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ ¬evaluate M w f → evaluate M w (dis (g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Tactic:
tauto
Proof state after:
no goals
Theorem: disEval
Proof state before:
W : Type
M : KripkeModel W
X : List Formula
w : W
⊢ evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
Tactic:
induction' X with f X IH
Proof state after:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis []) ↔ ∃ f ∈ [], evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w (dis (f :: X)) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Theorem: disEval
Proof state before:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis []) ↔ ∃ f ∈ [], evaluate M w f
Tactic:
simp
Proof state after:
no goals
Theorem: disEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w (dis (f :: X)) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
rw [disEvalHT]
Proof state after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w f ∨ evaluate M w (dis X) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Theorem: disEval
Proof state before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w f ∨ evaluate M w (dis X) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
simp [IH]
Proof state after:
no goals
Theorem: disconEvalHT
Proof state before:
X : List Formula
⊢ ∀ (XS : List (List Formula)), discon (X :: XS)≡Con X⋁discon XS
Tactic:
unfold semEquiv
Proof state after:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Theorem: disconEvalHT
Proof state before:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Tactic:
intro XS W M w
Proof state after:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Theorem: disconEvalHT
Proof state before:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Tactic:
cases' XS with Y YS
Proof state after:
case nil
X : List Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon [X]) ↔ evaluate M w (Con X⋁discon [])

case cons
X : List Formula
W : Type
M : KripkeModel W
w : W
Y : List Formula
YS : List (List Formula)
⊢ evaluate M w (discon (X :: Y :: YS)) ↔ evaluate M w (Con X⋁discon (Y :: YS))
Theorem: disconEvalHT
Proof state before:
case nil
X : List Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon [X]) ↔ evaluate M w (Con X⋁discon [])
Tactic:
simp
Proof state after:
no goals
Theorem: disconEvalHT
Proof state before:
case cons
X : List Formula
W : Type
M : KripkeModel W
w : W
Y : List Formula
YS : List (List Formula)
⊢ evaluate M w (discon (X :: Y :: YS)) ↔ evaluate M w (Con X⋁discon (Y :: YS))
Tactic:
simp
Proof state after:
no goals
Theorem: disconEval'
Proof state before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ {N : ℕ} (XS : List (List Formula)), XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
Tactic:
intro N
Proof state after:
W : Type
M : KripkeModel W
w : W
N : ℕ
⊢ ∀ (XS : List (List Formula)), XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)