import Mathlib.Data.Set.Basic

/-!
课堂展示版：引理 1.31。

目标不是重做前面所有形式化证明，而是把 `07_consist.lean` 中已经证明的
定理当作结论使用，集中展示下面两个命题的等价性：

1. 若 `Γ` 一致，则 `Γ` 可满足；
2. 若 `Γ ⊨ α`，则 `Γ ⊢ α`。
-/

namespace Satisfy

/-- 本节只需要矛盾常元、否定和蕴涵。 -/
inductive WFF : Type
  | p_atm : String → WFF
  | p_contra : WFF
  | p_not : WFF → WFF
  | p_imp : WFF → WFF → WFF

open WFF

infixr:60 " -> " => WFF.p_imp
notation "異議あり！" => WFF.p_contra

/-- 对象语言中的否定。 -/
def not (α : WFF) : WFF := WFF.p_not α

/--
`Γ |- α`：`α` 可由前提集 `Γ` 语法推出。

这里不展开 Hilbert 证明系统的归纳定义；前一节已经负责这件事。
-/
axiom Derivable : Set WFF → WFF → Prop

notation:50 Γ " |- " φ => Derivable Γ φ

/-- 一致性：不推出矛盾常元。 -/
def Consistent (Γ : Set WFF) : Prop := ¬ Γ |- 異議あり！

/-- 不一致：推出矛盾常元。 -/
def Inconsistent (Γ : Set WFF) : Prop := Γ |- 異議あり！

/--
定理 1.30，来自 `07_consist.lean`：

`Γ ⊢ α` 当且仅当 `Γ ∪ {¬α}` 不一致。
-/
axiom derivable_iff_inconsistent_union_not {Γ : Set WFF} {α : WFF} :
    (Γ |- α) ↔ Inconsistent (Γ ∪ ({not α} : Set WFF))

/-- 真值指派。 -/
def Valuation := String → Bool

/-- 公式在真值指派下的取值。 -/
def p_v (v : Valuation) : WFF → Bool
  | p_atm s => v s
  | p_contra => false
  | p_not φ => !(p_v v φ)
  | p_imp φ ψ => !(p_v v φ) || (p_v v ψ)

/-- `v` 满足公式 `φ`。 -/
def p_satisfies (v : Valuation) (φ : WFF) : Prop := p_v v φ = true

/-- `v` 满足公式集 `Γ`。 -/
def p_satisfies_set (v : Valuation) (Γ : Set WFF) : Prop :=
  ∀ φ ∈ Γ, p_satisfies v φ

/-- `Γ` 可满足。 -/
def p_satisfiable (Γ : Set WFF) : Prop :=
  ∃ v : Valuation, p_satisfies_set v Γ

/-- 语义后承：若 `v` 满足 `Γ`，则 `v` 满足 `α`。 -/
def p_entails (Γ : Set WFF) (α : WFF) : Prop :=
  ∀ v : Valuation, p_satisfies_set v Γ → p_satisfies v α

notation:50 Γ " |= " φ => p_entails Γ φ

/-- 不可满足的前提集语义蕴涵任意公式。 -/
theorem entails_of_not_satisfiable {Γ : Set WFF} {α : WFF} :
    ¬ p_satisfiable Γ → p_entails Γ α := by
  intro h_unsat v hΓ
  exact False.elim (h_unsat ⟨v, hΓ⟩)

/--
引理 1.31：

“一致则可满足”等价于“语义后承推出语法可推”。
-/
theorem lemma_1_31 :
    (∀ Γ : Set WFF, Consistent Γ → p_satisfiable Γ) ↔
      (∀ (Γ : Set WFF) (α : WFF), p_entails Γ α → Γ |- α) := by
  constructor
  · intro h_consistent_satisfiable Γ α h_entails
    by_contra h_not_derivable
    -- 由定理 1.30 的逆否命题：
    -- 若 `Γ ⊬ α`，则 `Γ ∪ {¬α}` 一致。
    have h_union_consistent : Consistent (Γ ∪ ({not α} : Set WFF)) := by
      intro h_inconsistent
      exact h_not_derivable
        ((derivable_iff_inconsistent_union_not).mpr h_inconsistent)
    -- 由命题 1 得到 `Γ ∪ {¬α}` 可满足。
    rcases h_consistent_satisfiable (Γ ∪ ({not α} : Set WFF)) h_union_consistent with
      ⟨v, h_union_sat⟩
    have hΓ : p_satisfies_set v Γ := by
      intro φ hφ
      exact h_union_sat φ (Or.inl hφ)
    have hα_true : p_satisfies v α :=
      h_entails v hΓ
    have hnotα_true : p_satisfies v (not α) :=
      h_union_sat (not α) (Or.inr rfl)
    -- 同一个指派既满足 `α` 又满足 `¬α`，矛盾。
    unfold p_satisfies at hα_true hnotα_true
    simp [not, p_v, hα_true] at hnotα_true
  · intro h_semantic_complete Γ h_consistent
    by_contra h_not_satisfiable
    -- 若 `Γ` 不可满足，则它语义蕴涵任意公式，特别是矛盾常元。
    have h_entails_contra : p_entails Γ 異議あり！ :=
      entails_of_not_satisfiable h_not_satisfiable
    -- 由命题 2 得 `Γ ⊢ 異議あり！`，与一致性矛盾。
    have h_derives_contra : Γ |- 異議あり！ :=
      h_semantic_complete Γ 異議あり！ h_entails_contra
    exact h_consistent h_derives_contra

end Satisfy