-- 题目 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 φ 在 env 下的真值
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，它的扩展是唯一的，即：若 v̄1 和 v̄2 都是 env 的扩展，则对任意 φ，v̄1(φ) ↔ v̄2(φ)
theorem vbar_equiv (vbar1 vbar2 : WFF → Prop) :
  ∀ φ : WFF, vbar1 φ ↔ vbar2 φ := by
  sorry

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     => sorry
  | p_not φ     => sorry
  | p_and φ ψ   => sorry
  | p_or φ ψ    => sorry
  | p_imp φ ψ   => sorry
  | p_iff φ ψ   => sorry

-- 定义 WFF 的真值函数 eval
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
  sorry

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 是自身完备的，当且仅当它可以仅用 f 构造公式表示 ¬、∧、∨
def is_self_complete (f : WFF → WFF → WFF) : Prop :=
  sorry

-- 证明：| (NAND) 和 ↓ (NOR) 都是自身完备的
theorem nand_self_complete :
  is_self_complete (λ α β => nand α β) := by
  sorry

theorem nor_self_complete :
  is_self_complete (λ α β => nor α β) := by
  sorry

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 φ ψ θ     => sorry

-- 证明：{¬, #} 不完备，即：存在一个WFF α，无法仅用 ¬ 和 # 构造出与 α 等价的 WFF
theorem neg_maj_not_complete : Prop := by -- 你需要补充完整命题
  sorry

end Exercise4