Theorem: ClassicalPropositionalLogic.soundness_theorem (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
induction h <;> intros v hv
State after:
case ax
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

State before:
case ax
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
solve_by_elim
State after:
case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)
Tactic:
case impI ih => intro hA; apply ih; simp [*]
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
case impE ih₁ ih₂ => exact ih₁ hv (ih₂ hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
case botC ih => by_contra hA; apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hv⟩)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)
Tactic:
case andI ih₁ ih₂ => exact ⟨ih₁ hv, ih₂ hv⟩
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
case andE1 ih => exact (ih hv).1
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
case andE2 ih => exact (ih hv).2
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
case orI1 ih => exact .inl (ih hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
case orI2 ih => exact .inr (ih hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : Γ✝ ⊨ A✝ || B✝
ih₂ : insert A✝ Γ✝ ⊨ C✝
ih₃ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝
Tactic:
case orE ih₁ ih₂ ih₃ => refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)
Tactic:
intro hA
State after:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ IsTrue v B✝

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ IsTrue v B✝
Tactic:
apply ih
State after:
case a
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ Satisfies v (insert A✝ Γ✝)

State before:
case a
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ Satisfies v (insert A✝ Γ✝)
Tactic:
simp [*]
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
exact ih₁ hv (ih₂ hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
by_contra hA
State after:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝
⊢ False

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝
⊢ False
Tactic:
apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hv⟩)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝¹ : Formula
a✝ : insert (~A✝¹) Γ✝ ⊢ ⊥
ih : insert (~A✝¹) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝¹
A✝ : Formula
⊢ IsTrue v ~A✝¹
Tactic:
exact hA
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)
Tactic:
exact ⟨ih₁ hv, ih₂ hv⟩
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
exact (ih hv).1
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
exact (ih hv).2
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
exact .inl (ih hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
exact .inr (ih hv)
State after:
no goals

State before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : Γ✝ ⊨ A✝ || B✝
ih₂ : insert A✝ Γ✝ ⊨ C✝
ih₃ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝
Tactic:
refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
State after:
no goals