-- 题目 1
namespace Exercise1

-- 原子命题符号集合 S
inductive SentSym
  | p | q | r
  deriving Repr, DecidableEq

open SentSym

-- 真值表：使用 Prop 作为真值类型，包含所有原子命题符号的真值赋值
variable (env : SentSym → Prop)

-- WFF 定义（符号版本）
inductive WFF
  | p_atm : SentSym → 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
  deriving Repr, DecidableEq

open WFF

-- v̄ 是 env 的扩展，递归定义 v̄(φ)：WFF φ 在 v̄ 下的真值
def vbar : WFF → Prop
  | p_atm s     => env s
  | p_not φ     => ¬ vbar φ
  | p_and φ ψ   => vbar φ ∧ vbar ψ
  | p_or φ ψ    => vbar φ ∨ vbar ψ
  | p_imp φ ψ   => vbar φ → vbar ψ
  | p_iff φ ψ   => vbar φ ↔ vbar ψ

-- 证明：对任意 env，它的扩展是唯一的。
-- 注：我们将“是 env 的扩展”这一条件作为前提显式列出
theorem vbar_equiv (vbar1 vbar2 : WFF → Prop)
  (h1_atm : ∀ s, vbar1 (p_atm s) ↔ env s)
  (h1_not : ∀ φ, vbar1 (p_not φ) ↔ ¬ vbar1 φ)
  (h1_and : ∀ φ ψ, vbar1 (p_and φ ψ) ↔ vbar1 φ ∧ vbar1 ψ)
  (h1_or  : ∀ φ ψ, vbar1 (p_or φ ψ) ↔ vbar1 φ ∨ vbar1 ψ)
  (h1_imp : ∀ φ ψ, vbar1 (p_imp φ ψ) ↔ (vbar1 φ → vbar1 ψ))
  (h1_iff : ∀ φ ψ, vbar1 (p_iff φ ψ) ↔ (vbar1 φ ↔ vbar1 ψ))
  (h2_atm : ∀ s, vbar2 (p_atm s) ↔ env s)
  (h2_not : ∀ φ, vbar2 (p_not φ) ↔ ¬ vbar2 φ)
  (h2_and : ∀ φ ψ, vbar2 (p_and φ ψ) ↔ vbar2 φ ∧ vbar2 ψ)
  (h2_or  : ∀ φ ψ, vbar2 (p_or φ ψ) ↔ vbar2 φ ∨ vbar2 ψ)
  (h2_imp : ∀ φ ψ, vbar2 (p_imp φ ψ) ↔ (vbar2 φ → vbar2 ψ))
  (h2_iff : ∀ φ ψ, vbar2 (p_iff φ ψ) ↔ (vbar2 φ ↔ vbar2 ψ)) :
  ∀ φ : WFF, vbar1 φ ↔ vbar2 φ := by
  intro φ
  induction φ with
  | p_atm s => rw [h1_atm, h2_atm]
  | p_not φ ih => rw [h1_not, h2_not, ih]
  | p_and φ ψ ih1 ih2 => rw [h1_and, h2_and, ih1, ih2]
  | p_or φ ψ ih1 ih2 => rw [h1_or, h2_or, ih1, ih2]
  | p_imp φ ψ ih1 ih2 => rw [h1_imp, h2_imp, ih1, ih2]
  | p_iff φ ψ ih1 ih2 => rw [h1_iff, h2_iff, ih1, ih2]

end Exercise1

-- 题目 2

namespace Exercise2

inductive WFF
  | 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
  deriving Repr, DecidableEq

open WFF

-- 对任意WFF α，定义其对偶 α*
def dual : WFF → WFF
  | p_atm p     => p_not (p_atm p)
  | p_not φ     => p_not (dual φ)
  | p_and φ ψ   => p_or (dual φ) (dual ψ)
  | p_or φ ψ    => p_and (dual φ) (dual ψ)
  | p_imp φ ψ   => p_and (p_not (dual φ)) (dual ψ)
  | p_iff φ ψ   => p_iff (p_not (dual φ)) (dual ψ)

def eval (env : String → Prop) : WFF → Prop
  | p_atm p     => env p
  | p_not φ     => ¬ eval env φ
  | p_and φ ψ   => eval env φ ∧ eval env ψ
  | p_or φ ψ    => eval env φ ∨ eval env ψ
  | p_imp φ ψ   => eval env φ → eval env ψ
  | p_iff φ ψ   => eval env φ ↔ eval env ψ

-- 证明：对任意 WFF α，α* 和 ¬α 等价
theorem dual_equiv (α : WFF) :
  ∀ env : String → Prop,
    eval env (dual α) ↔ ¬ eval env α := by
  intro env
  induction α with
  | p_atm p =>
    simp [dual, eval]
  | p_not φ ih =>
    simp [dual, eval, ih]
  | p_and φ ψ ih1 ih2 =>
    by_cases hφ : eval env φ <;> by_cases hψ : eval env ψ <;>
      simp [dual, eval, ih1, ih2, hφ, hψ]
  | p_or φ ψ ih1 ih2 =>
    by_cases hφ : eval env φ <;> by_cases hψ : eval env ψ <;>
      simp [dual, eval, ih1, ih2, hφ, hψ]
  | p_imp φ ψ ih1 ih2 =>
    by_cases hφ : eval env φ <;> by_cases hψ : eval env ψ <;>
      simp [dual, eval, ih1, ih2, hφ, hψ]
  | p_iff φ ψ ih1 ih2 =>
    by_cases hφ : eval env φ <;> by_cases hψ : eval env ψ <;>
      simp [dual, eval, ih1, ih2, hφ, hψ]

end Exercise2

-- 题目 3

namespace Exercise3

inductive WFF
  | p_atm : String → WFF
  | p_not : WFF → WFF
  | p_and : WFF → WFF → WFF
  | p_or  : WFF → WFF → WFF
  | nand  : WFF → WFF → WFF
  | nor   : WFF → WFF → WFF
  deriving Repr, DecidableEq

open WFF

def eval (env : String → Prop) : WFF → Prop
  | p_atm p     => env p
  | p_not φ     => ¬ eval env φ
  | p_and φ ψ   => eval env φ ∧ eval env ψ
  | p_or φ ψ    => eval env φ ∨ eval env ψ
  | nand φ ψ    => ¬ (eval env φ ∧ eval env ψ)
  | nor φ ψ     => ¬ (eval env φ ∨ eval env ψ)

-- 为了严格定义 "仅用 f 构造"，我们定义抽象的二元操作树语法
inductive FTerm
| var1
| var2
| op (x y : FTerm)

def applyFTerm (f : WFF → WFF → WFF) (α β : WFF) : FTerm → WFF
| FTerm.var1 => α
| FTerm.var2 => β
| FTerm.op x y => f (applyFTerm f α β x) (applyFTerm f α β y)

-- 定义自身完备性：存在操作树使得其语义上等同于 ¬, ∧, ∨
def is_self_complete (f : WFF → WFF → WFF) : Prop :=
  (∃ t : FTerm, ∀ env α, eval env (applyFTerm f α α t) ↔ ¬ eval env α) ∧
  (∃ t : FTerm, ∀ env α β, eval env (applyFTerm f α β t) ↔ eval env α ∧ eval env β) ∧
  (∃ t : FTerm, ∀ env α β, eval env (applyFTerm f α β t) ↔ eval env α ∨ eval env β)

-- 证明：| (NAND) 是自身完备的
theorem nand_self_complete :
  is_self_complete (fun α β => nand α β) := by
  unfold is_self_complete
  refine ⟨?_, ⟨?_, ?_⟩⟩
  · refine ⟨FTerm.op FTerm.var1 FTerm.var1, ?_⟩
    intro env α
    simp [applyFTerm, eval]
  · refine ⟨FTerm.op (FTerm.op FTerm.var1 FTerm.var2) (FTerm.op FTerm.var1 FTerm.var2), ?_⟩
    intro env α β
    by_cases hab : eval env α ∧ eval env β <;>
      simp [applyFTerm, eval, hab]
  · refine ⟨FTerm.op (FTerm.op FTerm.var1 FTerm.var1) (FTerm.op FTerm.var2 FTerm.var2), ?_⟩
    intro env α β
    by_cases hα : eval env α <;> by_cases hβ : eval env β <;>
      simp [applyFTerm, eval, hα, hβ]

-- 证明：↓ (NOR) 是自身完备的
theorem nor_self_complete :
  is_self_complete (fun α β => nor α β) := by
  unfold is_self_complete
  refine ⟨?_, ⟨?_, ?_⟩⟩
  · refine ⟨FTerm.op FTerm.var1 FTerm.var1, ?_⟩
    intro env α
    simp [applyFTerm, eval]
  · refine ⟨FTerm.op (FTerm.op FTerm.var1 FTerm.var1) (FTerm.op FTerm.var2 FTerm.var2), ?_⟩
    intro env α β
    by_cases hα : eval env α <;> by_cases hβ : eval env β <;>
      simp [applyFTerm, eval, hα, hβ]
  · refine ⟨FTerm.op (FTerm.op FTerm.var1 FTerm.var2) (FTerm.op FTerm.var1 FTerm.var2), ?_⟩
    intro env α β
    by_cases hab : eval env α ∨ eval env β <;>
      simp [applyFTerm, eval, hab]

end Exercise3

-- 题目 4

namespace Exercise4

inductive WFF
  | p_atm : String → WFF
  | p_not : WFF → WFF
  | maj   : WFF → WFF → WFF → WFF
  deriving Repr, DecidableEq

open WFF

-- 多数投票：三个中至少有两个成立
def eval (env : String → Prop) : WFF → Prop
  | p_atm p       => env p
  | p_not φ       => ¬ eval env φ
  | maj φ ψ θ     => (eval env φ ∧ eval env ψ) ∨ (eval env ψ ∧ eval env θ) ∨ (eval env θ ∧ eval env φ)

-- 辅助定理：由 {¬, #} 构造的公式全部保持对偶性（Self-Dual）
theorem self_dual (φ : WFF) (env : String → Prop) :
  eval (fun p => ¬ env p) φ ↔ ¬ eval env φ := by
  induction φ with
  | p_atm p =>
    simp [eval]
  | p_not φ ih =>
    simp [eval, ih]
  | maj φ ψ θ ih1 ih2 ih3 =>
    by_cases hφ : eval env φ <;> by_cases hψ : eval env ψ <;> by_cases hθ : eval env θ <;>
      simp [eval, ih1, ih2, ih3, hφ, hψ, hθ]

-- 证明：{¬, #} 不完备。
-- 我们完整补齐命题：存在一个真值函数 f（例如永真函数），不存在任何当前定义的 WFF φ 能在所有环境下与 f 等价。
-- 原因是当前所有公式均是自身对偶的，但永真函数不是。
theorem neg_maj_not_complete :
  ∃ f : (String → Prop) → Prop, ∀ φ : WFF, ¬ (∀ env, eval env φ ↔ f env) := by
  refine ⟨fun _ => True, ?_⟩
  intro φ h
  have h_true : eval (fun _ => True) φ := (h (fun _ => True)).mpr trivial
  have h_false : eval (fun _ => False) φ := (h (fun _ => False)).mpr trivial
  have h_sd : eval (fun _ => False) φ ↔ ¬ eval (fun _ => True) φ := by
    simpa using self_dual φ (fun _ => True)
  exact (h_sd.mp h_false) h_true

end Exercise4