/- ════════════════════════════════════════════════════════════════════════════
   第一部分：自然语言到一阶逻辑的翻译
   ════════════════════════════════════════════════════════════════════════════ -/

/-
  题目 1

  使用以下语言：
    • ∀  ：表示 "for all things"
    • N x ：表示 "x is a number"
    • I x ：表示 "x is interesting"
    • lt x y ：表示 "x is less than y"
    • zero ：常元，表示 "0"

  请将下列英文句子翻译为 Lean 命题，填入对应 def 的右侧。
  若英文句子有歧义，请用 _1、_2 后缀给出多种翻译。
-/

namespace Q1
  axiom α : Type
  axiom N : α → Prop
  axiom I : α → Prop
  axiom lt : α → α → Prop
  axiom zero : α

  -- (a) Zero is less than any number.
  def sentence_a : Prop := sorry

  -- (b) If any number is interesting, then zero is interesting.
  def sentence_b : Prop := sorry

  -- (c) No number is less than zero.
  def sentence_c : Prop := sorry

  -- (d) Any uninteresting number with the property that
  --     all smaller numbers are interesting certainly is interesting.
  def sentence_d : Prop := sorry

  -- (e) There is no number such that all numbers are less than it.
  def sentence_e : Prop := sorry

  -- (f) There is no number such that no number is less than it.
  def sentence_f : Prop := sorry
end Q1


/-
  题目 2

    "Neither a nor b is a member of every set."

  语言：
    • ∀ 量化所有集合
    • mem x s ：表示 "x is a member of s"（即 x ∈ s）
    • a, b ：常元
-/

namespace Q2

  def sentence : Prop := sorry
end Q2


/-
  题目 3 —— 改编自林肯名言（含歧义）

  语言：
    • P x ：表示 "x is a person"
    • T t ：表示 "t is a time"
    • F x t ：表示 "you can fool x at time t"

  请按提示给出对应翻译。原句存在歧义的，请分别给出。
-/

namespace Q3

  -- (a) You can fool some of the people all of the time.
  --     ("存在一些人，他们在任何时间都可能被愚弄")
  def sentence_a : Prop := sorry

  -- (b) You can fool all of the people some of the time.
  --     歧义 1："对每个人，都存在某个时间他在那时被愚弄"
  def sentence_b1 : Prop := sorry
  --     歧义 2："存在某个时间，所有人在那时都被愚弄"
  def sentence_b2 : Prop := sorry

  -- (c) You can't fool all of the people all of the time.
  --     ("不可能在所有时间愚弄所有人")
  def sentence_c : Prop := sorry
end Q3


/- ════════════════════════════════════════════════════════════════════════════
   第二部分：一阶逻辑的语法树与自由变元
   ════════════════════════════════════════════════════════════════════════════ -/

/-
  我们定义一阶逻辑（FOL）的项（Term）和公式（FOL）的归纳类型。
  为简化，项只包含变元和常元（没有函数符号）。
-/

inductive Term : Type
  | var   : String → Term     -- 变元，由变量名标识
  | const : String → Term     -- 常元，由常量名标识
  deriving Repr

inductive FOL : Type
  | atom    : String → List Term → FOL    -- P(t₁, …, tₙ)：谓词应用
  | neg     : FOL → FOL                    -- ¬φ
  | imp     : FOL → FOL → FOL              -- φ → ψ
  | and     : FOL → FOL → FOL              -- φ ∧ ψ
  | or      : FOL → FOL → FOL              -- φ ∨ ψ
  | forall_ : String → FOL → FOL           -- ∀x φ
  | exists_ : String → FOL → FOL           -- ∃x φ
  deriving Repr

open Term FOL


/-
  题目 4

  请实现以下两个函数，递归地判定变元 x 是否在公式 α 中"自由出现"。
  （参考课件中"自由出现"的定义）

  递归规则：
    1. 对原子公式 P(t₁, …, tₙ)：x 自由出现 ↔ 某个 tᵢ 中出现变元 x
    2. x 在 (¬α) 中自由出现 ↔ x 在 α 中自由出现
    3. x 在 (α □ β) 中自由出现 ↔ x 在 α 或 β 中自由出现
       （□ ∈ {→, ∧, ∨}）
    4. x 在 ∀y α 中自由出现 ↔ x 在 α 中自由出现 且 x ≠ y
    5. x 在 ∃y α 中自由出现 ↔ x 在 α 中自由出现 且 x ≠ y
-/

/-- 项 t 中是否含有变元 x。-/
def Term.hasVar (x : String) : Term → Bool
  | Term.var y   => sorry
  | Term.const _ => sorry

/-- 项列表 ts 中是否含有变元 x。（已实现，无需修改）-/
def Term.hasVarInList (x : String) (ts : List Term) : Bool :=
  ts.any (Term.hasVar x)

/-- 变元 x 是否在公式 α 中自由出现。-/
def FOL.occursFree (x : String) : FOL → Bool
  | FOL.atom _ ts    => sorry
  | FOL.neg α        => sorry
  | FOL.imp α β      => sorry
  | FOL.and α β      => sorry
  | FOL.or  α β      => sorry
  | FOL.forall_ y α  => sorry
  | FOL.exists_ y α  => sorry


/-
  题目 5

  请用上面定义的 AST 表示以下两个公式：

    (a) ∃v₁ P v₁ ∧ P v₁
        按"量词只作用于紧跟的最小公式"约定，等价于：
        (∃v₁ (P v₁)) ∧ (P v₁)

    (b) ∀v₁ A v₁ ∧ B v₁ → ∃v₂ ¬ C v₂ ∨ D v₂
        按相同约定及"¬ > ∧ > ∨ > →"的优先级，等价于：
        ((∀v₁ (A v₁)) ∧ (B v₁)) → ((∃v₂ (¬ C v₂)) ∨ (D v₂))

  最后用 #eval 验证自由变元判定（每个 #eval 都应返回 true）。
-/

def v₁ : Term := var "v1"
def v₂ : Term := var "v2"

-- (a) (∃v₁ (P v₁)) ∧ (P v₁)
def formula_a : FOL := sorry

-- (b) ((∀v₁ (A v₁)) ∧ (B v₁)) → ((∃v₂ (¬ C v₂)) ∨ (D v₂))
def formula_b : FOL := sorry

-- 期望：true（第二个 P v₁ 中的 v₁ 自由出现）
#eval FOL.occursFree "v1" formula_a

-- 期望：true（B v₁ 中的 v₁ 自由出现）
#eval FOL.occursFree "v1" formula_b

-- 期望：true（D v₂ 中的 v₂ 自由出现）
#eval FOL.occursFree "v2" formula_b