internlm/Lean-Github huggingface dataset:
Theorem: existsLocalTableauFor
Proof state before:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
ruleA : LocalRuleApp (LR.1, LR.2) (applyLocalRule lr (LR.1, LR.2)) := LocalRuleApp.mk C LCond RCond lr ⋯
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ LocalTableau c
Tactic:
apply Classical.choice (existsLocalTableauFor c)
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:
X Y : Finset Formula
⊢ Satisfiable X → Y ⊆ X → Satisfiable Y
Tactic:
aesop
Proof state after:
no goals
Theorem: singletonSat_iff_sat
Proof state before:
⊢ ∀ (φ : Formula), Satisfiable {φ} ↔ Satisfiable φ
Tactic:
intro phi
Proof state after:
phi : Formula
⊢ Satisfiable {phi} ↔ Satisfiable phi
Theorem: singletonSat_iff_sat
Proof state before:
phi : Formula
⊢ Satisfiable {phi} ↔ Satisfiable phi
Tactic:
simp
Proof state after:
no goals
Theorem: tautImp_iff_comboNotUnsat
Proof state before:
ϕ ψ : Formula
⊢ Tautology (ϕ↣ψ) ↔ ¬Satisfiable {ϕ, ~ψ}
Tactic:
unfold Tautology
Proof state after:
ϕ ψ : Formula
⊢ (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) (ϕ↣ψ)) ↔ ¬Satisfiable {ϕ, ~ψ}
Theorem: tautImp_iff_comboNotUnsat
Proof state before:
ϕ ψ : Formula
⊢ (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) (ϕ↣ψ)) ↔ ¬Satisfiable {ϕ, ~ψ}
Tactic:
simp
Proof state after:
no goals
Theorem: semEquiv.transitive
Proof state before:
⊢ Transitive semEquiv
Tactic:
unfold Transitive
Proof state after:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z
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
Theorem: semEquiv.transitive
Proof state before:
⊢ ∀ ⦃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
Tactic:
intro f g h f_is_g g_is_h W M w
Proof state after:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Theorem: semEquiv.transitive
Proof state before:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
specialize f_is_g W M w
Proof state after:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Theorem: semEquiv.transitive
Proof state before:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) g ↔ Evaluate (M, w) h
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
specialize g_is_h W M w
Proof state after:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : Evaluate (M, w) g ↔ Evaluate (M, w) h
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Theorem: semEquiv.transitive
Proof state before:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : Evaluate (M, w) f ↔ Evaluate (M, w) g
g_is_h : Evaluate (M, w) g ↔ Evaluate (M, w) h
⊢ Evaluate (M, w) f ↔ Evaluate (M, w) h
Tactic:
tauto
Proof state after:
no goals
Theorem: forms_to_sets
Proof state before:
φ ψ : Formula
⊢ φ⊨ψ → {φ}⊨{ψ}
Tactic:
intro impTaut
Proof state after:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ {φ}⊨{ψ}
Theorem: forms_to_sets
Proof state before:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ {φ}⊨{ψ}
Tactic:
intro W M w lhs ψ1 psi1_in_setpsi
Proof state after:
φ ψ : Formula
impTaut : φ⊨ψ
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
⊢ Evaluate (M, w) ψ1
Theorem: forms_to_sets
Proof state before:
φ ψ : Formula
impTaut : φ⊨ψ
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
⊢ Evaluate (M, w) ψ1
Tactic:
specialize impTaut W M w
Proof state after:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
impTaut : (∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1) → ∀ ψ_1 ∈ {ψ}, Evaluate (M, w) ψ_1
⊢ Evaluate (M, w) ψ1
Theorem: forms_to_sets
Proof state before:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
impTaut : (∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1) → ∀ ψ_1 ∈ {ψ}, Evaluate (M, w) ψ_1
⊢ Evaluate (M, w) ψ1
Tactic:
simp at *
Proof state after:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
psi1_in_setpsi : ψ1 = ψ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ
⊢ Evaluate (M, w) ψ1
Theorem: forms_to_sets
Proof state before:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
psi1_in_setpsi : ψ1 = ψ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ
⊢ Evaluate (M, w) ψ1
Tactic:
subst psi1_in_setpsi
Proof state after:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) ψ1
Theorem: forms_to_sets
Proof state before:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) ψ1
Tactic:
apply impTaut
Proof state after:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) φ
Theorem: forms_to_sets
Proof state before:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) φ
Tactic:
exact lhs
Proof state after:
no goals
Theorem: negation_not_cosatisfiable
Proof state before:
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
⊢ ¬Satisfiable X
Tactic:
rintro ⟨W,M,w,satX⟩
Proof state after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
⊢ False
Theorem: negation_not_cosatisfiable
Proof state before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
⊢ False
Tactic:
have := satX φ phi_in
Proof state after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this : Evaluate (M, w) φ
⊢ False
Theorem: negation_not_cosatisfiable
Proof state before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this : Evaluate (M, w) φ
⊢ False
Tactic:
have := satX (~φ) notPhi_in
Proof state after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this✝ : Evaluate (M, w) φ
this : Evaluate (M, w) (~φ)
⊢ False
Theorem: negation_not_cosatisfiable
Proof state before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this✝ : Evaluate (M, w) φ
this : Evaluate (M, w) (~φ)
⊢ False
Tactic:
tauto
Proof state after:
no goals
Theorem: sat_double_neq_invariant
Proof state before:
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) ↔ Satisfiable (X ∪ {φ})
Tactic:
constructor
Proof state after:
case mp
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) → Satisfiable (X ∪ {φ})

case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})
Theorem: sat_double_neq_invariant
Proof state before:
case mp
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) → Satisfiable (X ∪ {φ})

case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})
Tactic:
all_goals rintro ⟨W,M,w,satX⟩
Proof state after:
case mp.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {φ})

case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Theorem: sat_double_neq_invariant
Proof state before:
case mp.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {φ})

case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Tactic:
all_goals use W, M, w
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1

case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
Theorem: sat_double_neq_invariant
Proof state before:
case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})
Tactic:
rintro ⟨W,M,w,satX⟩
Proof state after:
case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Theorem: sat_double_neq_invariant
Proof state before:
case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Tactic:
use W, M, w
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
Tactic:
intro φ' is_in
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {φ}
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {φ}
⊢ Evaluate (M, w) φ'
Tactic:
simp at is_in
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = φ
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = φ
⊢ Evaluate (M, w) φ'
Tactic:
cases is_in
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'

case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = φ
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ'
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Tactic:
apply satX
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {~~φ}
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {~~φ}
Tactic:
aesop
Proof state after:
no goals
Theorem: sat_double_neq_invariant
Proof state before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = φ
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX (~~φ)
Proof state after:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = φ
satX : ~~φ ∈ X ∪ {~~φ} → Evaluate (M, w) (~~φ)
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = φ
satX : ~~φ ∈ X ∪ {~~φ} → Evaluate (M, w) (~~φ)
⊢ Evaluate (M, w) φ'
Tactic:
aesop
Proof state after:
no goals
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
Tactic:
intro φ' is_in
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {~~φ}
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {~~φ}
⊢ Evaluate (M, w) φ'
Tactic:
simp at is_in
Proof state after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = ~~φ
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = ~~φ
⊢ Evaluate (M, w) φ'
Tactic:
cases is_in
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'

case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = ~~φ
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ'
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Tactic:
apply satX
Proof state after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {φ}
Theorem: sat_double_neq_invariant
Proof state before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {φ}
Tactic:
aesop
Proof state after:
no goals
Theorem: sat_double_neq_invariant
Proof state before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = ~~φ
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ
Proof state after:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = ~~φ
satX : φ ∈ X ∪ {φ} → Evaluate (M, w) φ
⊢ Evaluate (M, w) φ'
Theorem: sat_double_neq_invariant
Proof state before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = ~~φ
satX : φ ∈ X ∪ {φ} → Evaluate (M, w) φ
⊢ Evaluate (M, w) φ'
Tactic:
aesop
Proof state after:
no goals
Theorem: tautImp_iff_TNodeUnsat
Proof state before:
φ ψ : Formula
X : TNode
⊢ X = ([φ], [~ψ], none) → (φ⊨ψ ↔ ¬satisfiable X)
Tactic:
intro defX
Proof state after:
φ ψ : Formula
X : TNode
defX : X = ([φ], [~ψ], none)
⊢ φ⊨ψ ↔ ¬satisfiable X
Theorem: tautImp_iff_TNodeUnsat
Proof state before:
φ ψ : Formula
X : TNode
defX : X = ([φ], [~ψ], none)
⊢ φ⊨ψ ↔ ¬satisfiable X
Tactic:
subst defX
Proof state after:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable ([φ], [~ψ], none)
Theorem: tautImp_iff_TNodeUnsat
Proof state before:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable ([φ], [~ψ], none)
Tactic:
simp [satisfiable,evaluate,modelCanSemImplyTNode,formCanSemImplyForm,semImpliesLists] at *
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
⊢ Con X≡discon B
Tactic:
intro W M w
Proof state after:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con X) ↔ evaluate M w (discon B)
Theorem: oneSidedLocalRuleTruth
Proof state before:
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con X) ↔ evaluate M w (discon B)
Tactic:
cases lr
Proof state after:
case bot
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [⊥]) ↔ evaluate M w (discon ∅)

case not
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [φ✝, ~φ✝]) ↔ evaluate M w (discon ∅)

case neg
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [~~φ✝]) ↔ evaluate M w (discon [[φ✝]])

case con
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [φ✝⋀ψ✝]) ↔ evaluate M w (discon [[φ✝, ψ✝]])

case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])

case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Theorem: oneSidedLocalRuleTruth
Proof state before:
case bot
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con [⊥]) ↔ evaluate M w (discon ∅)

case not
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [φ✝, ~φ✝]) ↔ evaluate M w (discon ∅)

case neg
W : Type
M : KripkeModel W
w : W
φ✝ : Formula
⊢ evaluate M w (Con [~~φ✝]) ↔ evaluate M w (discon [[φ✝]])

case con
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [φ✝⋀ψ✝]) ↔ evaluate M w (discon [[φ✝, ψ✝]])

case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])

case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
all_goals try (simp; done)
Proof state after:
case box
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldBox α✝ φ✝))

case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Theorem: oneSidedLocalRuleTruth
Proof state before:
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [~⌈α⌉φ]) ↔ evaluate M w (discon (unfoldDiamond α φ))
Tactic:
case dia α φ =>
  rw [conEval]
  simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
  rw [localDiamondTruth α φ W M w, disEval, disconEval]
  apply mapCon_mapForall
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case nCo
W : Type
M : KripkeModel W
w : W
φ✝ ψ✝ : Formula
⊢ evaluate M w (Con [~φ✝⋀ψ✝]) ↔ evaluate M w (discon [[~φ✝], [~ψ✝]])
Tactic:
try (simp; done)
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
(simp; done)
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
simp
Proof state after:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ (∃ x, relate M α✝ w x ∧ ¬evaluate M x φ✝) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Theorem: oneSidedLocalRuleTruth
Proof state before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ (∃ x, relate M α✝ w x ∧ ¬evaluate M x φ✝) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
done
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
(aesop; done)
Proof state after:
no goals
Theorem: oneSidedLocalRuleTruth
Proof state before:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (Con [~⌈α✝⌉φ✝]) ↔ evaluate M w (discon (unfoldDiamond α✝ φ✝))
Tactic:
aesop
Proof state after:
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
w_1 : W
left : relate M α w w_1
right : ¬evaluate M w_1 φ
⊢ evaluate M w (discon (unfoldDiamond α φ))

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
a : evaluate M w (discon (unfoldDiamond α φ))
⊢ ∃ x, relate M α w x ∧ ¬evaluate M x φ