internlm/Lean-Github huggingface dataset:
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: 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: vDashSingleton_iff_vDash_formula
Proof state before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ (φ : Formula), (M, w)⊨[φ] ↔ evaluate M w φ
Tactic:
intro phi
Proof state after:
W : Type
M : KripkeModel W
w : W
phi : Formula
⊢ (M, w)⊨[phi] ↔ evaluate M w phi
Theorem: vDashSingleton_iff_vDash_formula
Proof state before:
W : Type
M : KripkeModel W
w : W
phi : Formula
⊢ (M, w)⊨[phi] ↔ evaluate M w phi
Tactic:
simp [modelCanSemImplyList]
Proof state after:
no goals
Theorem: forms_to_lists
Proof state before:
φ ψ : Formula
⊢ φ⊨ψ → [φ]⊨[ψ]
Tactic:
intro impTaut
Proof state after:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ [φ]⊨[ψ]
Theorem: forms_to_lists
Proof state before:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ [φ]⊨[ψ]
Tactic:
intro W M w lhs ψ psi_in_psi
Proof state after:
φ ψ✝ : Formula
impTaut : φ⊨ψ✝
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
⊢ evaluate M w ψ
Theorem: forms_to_lists
Proof state before:
φ ψ✝ : Formula
impTaut : φ⊨ψ✝
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
⊢ evaluate M w ψ
Tactic:
specialize impTaut W M w
Proof state after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
⊢ evaluate M w ψ
Theorem: forms_to_lists
Proof state before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
⊢ evaluate M w ψ
Tactic:
simp at psi_in_psi lhs
Proof state after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ
Theorem: forms_to_lists
Proof state before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ
Tactic:
rw [psi_in_psi]
Proof state after:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ✝
Theorem: forms_to_lists
Proof state before:
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ evaluate M w ψ✝
Tactic:
apply impTaut
Proof state after:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Theorem: forms_to_lists
Proof state before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Tactic:
rw [←vDashSingleton_iff_vDash_formula φ] at lhs
Proof state after:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : (M, w)⊨[φ]
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Theorem: forms_to_lists
Proof state before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : (M, w)⊨[φ]
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1
Tactic:
tauto
Proof state after:
no goals
Theorem: forms_to_lists
Proof state before:
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
Tactic:
aesop
Proof state after:
no goals
Theorem: notSat_iff_semImplies
Proof state before:
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) ↔ X⊨[φ]
Tactic:
constructor
Proof state after:
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]

case mpr
X : List Formula
φ : Formula
⊢ X⊨[φ] → ¬satisfiable (X ∪ [~φ])
Theorem: notSat_iff_semImplies
Proof state before:
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]
Tactic:
simp only [satisfiable, not_exists, not_forall, exists_prop, setCanSemImplySet, semImpliesSets, forall_eq]
Proof state after:
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]
Theorem: notSat_iff_semImplies
Proof state before:
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]
Tactic:
intro nSat W M w satX
Proof state after:
case mp
X : List Formula
φ : Formula
nSat : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Theorem: notSat_iff_semImplies
Proof state before:
case mp
X : List Formula
φ : Formula
nSat : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Tactic:
specialize nSat W M w
Proof state after:
case mp
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
nSat : ∃ x ∈ X ∪ [~φ], ¬evaluate M w x
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Theorem: notSat_iff_semImplies
Proof state before:
case mp
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
nSat : ∃ x ∈ X ∪ [~φ], ¬evaluate M w x
⊢ ∀ ψ ∈ [φ], evaluate M w ψ
Tactic:
rcases nSat with ⟨φ, phi_in, not_phi⟩
Proof state after:
case mp.intro.intro
X : List Formula
φ✝ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
φ : Formula
phi_in : φ ∈ X ∪ [~φ✝]
not_phi : ¬evaluate M w φ
⊢ ∀ ψ ∈ [φ✝], evaluate M w ψ
Theorem: notSat_iff_semImplies
Proof state before:
case mp.intro.intro
X : List Formula
φ✝ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
φ : Formula
phi_in : φ ∈ X ∪ [~φ✝]
not_phi : ¬evaluate M w φ
⊢ ∀ ψ ∈ [φ✝], evaluate M w ψ
Tactic:
aesop
Proof state after:
no goals
Theorem: notSat_iff_semImplies
Proof state before:
case mpr
X : List Formula
φ : Formula
⊢ X⊨[φ] → ¬satisfiable (X ∪ [~φ])
Tactic:
intro X_φ
Proof state after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
⊢ ¬satisfiable (X ∪ [~φ])
Theorem: notSat_iff_semImplies
Proof state before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
⊢ ¬satisfiable (X ∪ [~φ])
Tactic:
by_contra hyp
Proof state after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : satisfiable (X ∪ [~φ])
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : satisfiable (X ∪ [~φ])
⊢ False
Tactic:
simp only [satisfiable, setCanSemImplySet, semImpliesSets] at hyp
Proof state after:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Tactic:
rcases hyp with ⟨W, M, w, w_⟩
Proof state after:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
X_φ : X⊨[φ]
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
X_φ : X⊨[φ]
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
Tactic:
specialize X_φ W M w
Proof state after:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro
X : List Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
cases X
Proof state after:
case mpr.intro.intro.intro.nil
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ [] ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ [], evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False

case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro.nil
φ : Formula
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ [] ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ [], evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
Tactic:
have := w_ (~φ)
Proof state after:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
this : (~φ) ∈ head✝ :: tail✝ ∪ [~φ] → evaluate M w (~φ)
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
this : (~φ) ∈ head✝ :: tail✝ ∪ [~φ] → evaluate M w (~φ)
⊢ False
Tactic:
simp at *
Proof state after:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : evaluate M w head✝ ∧ ∀ (a : Formula), a ∈ tail✝ ∨ a = (~φ) → evaluate M w a
X_φ : evaluate M w head✝ → (∀ a ∈ tail✝, evaluate M w a) → evaluate M w φ
this : ¬evaluate M w φ
⊢ False
Theorem: notSat_iff_semImplies
Proof state before:
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : evaluate M w head✝ ∧ ∀ (a : Formula), a ∈ tail✝ ∨ a = (~φ) → evaluate M w a
X_φ : evaluate M w head✝ → (∀ a ∈ tail✝, evaluate M w a) → evaluate M w φ
this : ¬evaluate M w φ
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: equivSat
Proof state before:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
⊢ φ≡ψ → (M, w)⊨φ → (M, w)⊨ψ
Tactic:
intro φ_eq_ψ evalφ
Proof state after:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
⊢ (M, w)⊨ψ
Theorem: equivSat
Proof state before:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
⊢ (M, w)⊨ψ
Tactic:
have : evaluate M w φ := by tauto
Proof state after:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
Theorem: equivSat
Proof state before:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
Tactic:
rw [φ_eq_ψ] at this
Proof state after:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ
Theorem: equivSat
Proof state before:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ
Tactic:
tauto
Proof state after:
no goals
Theorem: equivSat
Proof state before:
W : Type
φ ψ : Formula
M : KripkeModel W
w : W
φ_eq_ψ : φ≡ψ
evalφ : (M, w)⊨φ
⊢ evaluate M w φ
Tactic:
tauto
Proof state after:
no goals
Theorem: equiv_iff
Proof state before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
⊢ ∀ {W : Type} {M : KripkeModel W} {w : W}, (M, w)⊨φ ↔ (M, w)⊨ψ
Tactic:
intro W M w
Proof state after:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ ↔ (M, w)⊨ψ
Theorem: equiv_iff
Proof state before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ ↔ (M, w)⊨ψ
Tactic:
constructor
Proof state after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ → (M, w)⊨ψ

case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨ψ → (M, w)⊨φ
Theorem: equiv_iff
Proof state before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ → (M, w)⊨ψ
Tactic:
intro
Proof state after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ (M, w)⊨ψ
Theorem: equiv_iff
Proof state before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ (M, w)⊨ψ
Tactic:
have : evaluate M w φ := by tauto
Proof state after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
Theorem: equiv_iff
Proof state before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
Tactic:
rw [φ_eq_ψ] at this
Proof state after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ
Theorem: equiv_iff
Proof state before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ
Tactic:
tauto
Proof state after:
no goals
Theorem: equiv_iff
Proof state before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ evaluate M w φ
Tactic:
tauto
Proof state after:
no goals
Theorem: equiv_iff
Proof state before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨ψ → (M, w)⊨φ
Tactic:
intro
Proof state after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ (M, w)⊨φ
Theorem: equiv_iff
Proof state before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ (M, w)⊨φ
Tactic:
have : evaluate M w ψ := by tauto
Proof state after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w ψ
⊢ (M, w)⊨φ
Theorem: equiv_iff
Proof state before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w ψ
⊢ (M, w)⊨φ
Tactic:
rw [← φ_eq_ψ] at this
Proof state after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w φ
⊢ (M, w)⊨φ
Theorem: equiv_iff
Proof state before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w φ
⊢ (M, w)⊨φ
Tactic:
tauto
Proof state after:
no goals
Theorem: equiv_iff
Proof state before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ evaluate M w ψ
Tactic:
tauto
Proof state after:
no goals
Theorem: tautImp_iff_comboNotUnsat
Proof state before:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable [φ, ~ψ]
Tactic:
simp [formCanSemImplyForm, semImpliesLists, satisfiable, evaluate]
Proof state after:
no goals
Theorem: relate_steps
Proof state before:
W✝ : Type
M : KripkeModel W✝
as bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
Tactic:
induction as
Proof state after:
case nil
W✝ : Type
M : KripkeModel W✝
bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps ([] ++ bs)) x z ↔ ∃ y, relate M (Program.steps []) x y ∧ relate M (Program.steps bs) y z

case cons
W✝ : Type
M : KripkeModel W✝
bs : List Program
head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ (x z : W✝),
    relate M (Program.steps (tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps tail✝) x y ∧ relate M (Program.steps bs) y z
⊢ ∀ (x z : W✝),
    relate M (Program.steps (head✝ :: tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps (head✝ :: tail✝)) x y ∧ relate M (Program.steps bs) y z
Theorem: relate_steps
Proof state before:
case nil
W✝ : Type
M : KripkeModel W✝
bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps ([] ++ bs)) x z ↔ ∃ y, relate M (Program.steps []) x y ∧ relate M (Program.steps bs) y z
Tactic:
simp
Proof state after:
no goals
Theorem: relate_steps
Proof state before:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
⊢ ∀ (x z : W✝),
    relate M (Program.steps (a :: as ++ bs)) x z ↔
      ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
intro x z
Proof state after:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z ↔
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Theorem: relate_steps
Proof state before:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z ↔
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
constructor
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z →
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z

case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ (∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z) →
    relate M (Program.steps (a :: as ++ bs)) x z
Theorem: relate_steps
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z →
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
intro lhs
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : relate M (Program.steps (a :: as ++ bs)) x z
⊢ ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Theorem: relate_steps
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : relate M (Program.steps (a :: as ++ bs)) x z
⊢ ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
simp at *
Proof state after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Theorem: relate_steps
Proof state before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Tactic:
rcases lhs with ⟨y, x_a_y, y_asbs_z⟩
Proof state after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y_asbs_z : relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z