import Mathlib.Data.Set.Basic

namespace DeductionTheorem

/--
命题公式的语法。为证明演绎定理，这里只需要一个标准的命题语言。
-/
inductive WFF : Type
  | p_atm : String → WFF
  | p_not : WFF → WFF
  | p_and : WFF → WFF → WFF
  | p_or  : WFF → WFF → WFF
  | p_imp : WFF → WFF → WFF
  | p_iff : WFF → WFF → WFF

open WFF

infixr:60 " -> " => WFF.p_imp

/--
Hilbert 系统中证明演绎定理所需的两个公理模式：
`K` 和 `S`。
-/
inductive IsAxiom : WFF → Prop
  | K (α β : WFF) : IsAxiom (α -> (β -> α))
  | S (α β γ : WFF) : IsAxiom ((α -> (β -> γ)) -> ((α -> β) -> (α -> γ)))

/--
`Γ ⊢ φ` 表示：公式 `φ` 可由前提集 `Γ` 推出。
-/
inductive Derivable (Γ : Set WFF) : WFF → Prop
  | hyp {φ : WFF} : φ ∈ Γ → Derivable Γ φ
  | axm {φ : WFF} : IsAxiom φ → Derivable Γ φ
  | mp  {φ ψ : WFF} : Derivable Γ φ → Derivable Γ (φ -> ψ) → Derivable Γ ψ

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

/--
引理 1.24：若 `Γ ⊢ α` 且 `Γ ⊢ α ⟶ β`，那么 `Γ ⊢ β`。
这正是 MP 规则。
-/
theorem lemma_1_24 {Γ : Set WFF} {α β : WFF} :
    (Γ |- α) → (Γ |- (α -> β)) → (Γ |- β) := by
  intro hα hαβ
  exact Derivable.mp hα hαβ

/--
若 `Γ ⊆ Δ`，则任意从 `Γ` 可推出的公式，从 `Δ` 也可推出。
-/
theorem weakening {Γ Δ : Set WFF} {φ : WFF} (hsub : Γ ⊆ Δ) :
    (Γ |- φ) → (Δ |- φ) := by
  intro h
  induction h with
  | hyp hmem =>
      exact Derivable.hyp (hsub hmem)
  | axm hax =>
      exact Derivable.axm hax
  | mp h₁ h₂ ih₁ ih₂ =>
      exact Derivable.mp ih₁ ih₂

theorem axiomK {Γ : Set WFF} (α β : WFF) : Γ |- (α -> (β -> α)) :=
  Derivable.axm (IsAxiom.K α β)

theorem axiomS {Γ : Set WFF} (α β γ : WFF) :
    Γ |- ((α -> (β -> γ)) -> ((α -> β) -> (α -> γ))) :=
  Derivable.axm (IsAxiom.S α β γ)

/--
Hilbert 系统中的恒等律：`Γ ⊢ α ⟶ α`。
-/
theorem self_imp {Γ : Set WFF} (α : WFF) : Γ |- (α -> α) := by
  have h1 : Γ |- (α -> ((α -> α) -> α)) := axiomK α (α -> α)
  have h2 : Γ |- (α -> (α -> α)) := axiomK α α
  have h3 : Γ |- ((α -> ((α -> α) -> α)) -> ((α -> (α -> α)) -> (α -> α))) :=
    axiomS α (α -> α) α
  have h4 : Γ |- ((α -> (α -> α)) -> (α -> α)) := lemma_1_24 h1 h3
  exact lemma_1_24 h2 h4

/--
演绎定理的正向部分。
证明方法：对 `Γ ∪ {α} ⊢ β` 的证明树做归纳。
-/
theorem deduction_forward {Γ : Set WFF} {α β : WFF} :
    ((Γ ∪ ({α} : Set WFF)) |- β) → (Γ |- (α -> β)) := by
  intro h
  induction h with
  | @hyp φ hmem =>
      rcases hmem with hΓ | hα
      · have hφ : Γ |- φ := Derivable.hyp hΓ
        have hk : Γ |- (φ -> (α -> φ)) := axiomK φ α
        exact lemma_1_24 hφ hk
      · have hEq : φ = α := hα
        subst φ
        exact self_imp α
  | @axm φ hax =>
      have hφ : Γ |- φ := Derivable.axm hax
      have hk : Γ |- (φ -> (α -> φ)) := axiomK φ α
      exact lemma_1_24 hφ hk
  | @mp φ ψ hφ hφψ ihφ ihφψ =>
      have hS : Γ |- ((α -> (φ -> ψ)) -> ((α -> φ) -> (α -> ψ))) :=
        axiomS α φ ψ
      have hmid : Γ |- ((α -> φ) -> (α -> ψ)) := lemma_1_24 ihφψ hS
      exact lemma_1_24 ihφ hmid

/--
演绎定理的反向部分。
若 `Γ |- α ⟶ β`，则在 `Γ ∪ {α}` 中加入前提 `α` 后可由引理 1.24 推出 `β`。
-/
theorem deduction_backward {Γ : Set WFF} {α β : WFF} :
    (Γ |- (α -> β)) → ((Γ ∪ ({α} : Set WFF)) |- β) := by
  intro h
  have hImp : (Γ ∪ ({α} : Set WFF)) |- (α -> β) :=
    weakening (by
      intro φ hφ
      exact Or.inl hφ) h
  have hα : (Γ ∪ ({α} : Set WFF)) |- α :=
    Derivable.hyp (Or.inr rfl)
  exact lemma_1_24 hα hImp

/--
演绎定理：
`Γ ∪ {α} |- β` 当且仅当 `Γ |- α ⟶ β`。
-/
theorem deduction_theorem {Γ : Set WFF} {α β : WFF} :
    (((Γ ∪ ({α} : Set WFF)) |- β) ↔ (Γ |- (α -> β))) := by
  constructor
  · exact deduction_forward
  · exact deduction_backward

end DeductionTheorem