/--
`inductive` 用来“归纳地定义一个类型”。
意思是：我们先说明最基本的对象有哪些，再说明如何从旧对象构造新对象。

这里定义的 `WFF` 是 “well-formed formula”，即良构公式。
冒号后面的 `Type` 表示 `WFF` 本身是一个类型。
-/
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` 的作用是把命名空间 `WFF` 打开。
-- 这样后面可以直接写 `p_atm`、`p_not`，而不用每次都写成 `WFF.p_atm`、`WFF.p_not`。
open WFF

/--
`def` 用来定义常量、函数或对象。

这里 `WFF_to_String : WFF → String` 表示：
这是一个函数，输入一个 `WFF`，输出一个 `String`。
箭头 `→` 可以读作“映射到”或“输入……输出……”。

下面不是按普通变量来写函数，而是直接按 `WFF` 的不同构造子分情况定义，
这叫做“模式匹配”（pattern matching）。
-/
def WFF_to_String : WFF → String
  -- 原子公式直接输出其名字
  | p_atm s   => s
  -- `=>` 读作“映射为”。
  -- 复合公式递归地转成字符串，并补上括号以消除歧义。
  | p_not φ   => "(¬" ++ WFF_to_String φ ++  ")"
  | p_and φ ψ => "(" ++ WFF_to_String φ ++ " ∧ " ++ WFF_to_String ψ ++ ")"
  | p_or  φ ψ => "(" ++ WFF_to_String φ ++ " ∨ " ++ WFF_to_String ψ ++ ")"
  | p_imp φ ψ => "(" ++ WFF_to_String φ ++ " → " ++ WFF_to_String ψ ++ ")"
  | p_iff φ ψ => "(" ++ WFF_to_String φ ++ " ↔ " ++ WFF_to_String ψ ++ ")"

/--
`instance` 用来声明一个类型类实例。
这里我们告诉 Lean：`WFF` 可以被转成字符串，所以以后 `#eval` 或输出时会更好看。

`where` 后面是在填写这个实例需要提供的字段。
这里 `toString := WFF_to_String` 的意思是：
把 `WFF` 转字符串的具体实现，就使用我们刚定义好的 `WFF_to_String`。
-/
instance : ToString WFF where
  toString := WFF_to_String

-- 一组样例原子命题，便于后面直接拼装例子
-- `:=` 可以读作“定义为”。
def A₁ : WFF := p_atm "A₁"
def A₂ : WFF := p_atm "A₂"
def A₃ : WFF := p_atm "A₃"
def A₄ : WFF := p_atm "A₄"
def A₅ : WFF := p_atm "A₅"
def A₆ : WFF := p_atm "A₆"
def A₇ : WFF := p_atm "A₇"
def A₈ : WFF := p_atm "A₈"
def A₉ : WFF := p_atm "A₉"
def A₁₀ : WFF := p_atm "A₁₀"

-- 例子：(A₁ ∧ ¬A₂) → A₃
def complex_WFF : WFF :=
  p_imp (p_and A₁ (p_not A₂)) A₃

-- `#eval` 会让 Lean 直接计算后面的表达式，并显示结果。
#eval WFF_to_String complex_WFF

/--
这个函数给每个公式生成一个“构造序列”。
你可以把它理解成：按构造公式的先后顺序，把中间步骤都记录下来。

输出类型 `List WFF` 表示“一个由 `WFF` 组成的列表”。
-/
def construct_seq : WFF → List WFF
  -- 原子公式的构造序列只包含它自身
  | p_atm s   => [p_atm s]
  -- 复合公式先列出子公式的构造，再把当前公式放到末尾
  -- `++` 是列表拼接。
  | p_not φ   => (construct_seq φ) ++ [p_not φ]
  | p_and φ ψ => (construct_seq φ) ++ (construct_seq ψ) ++ [p_and φ ψ]
  | p_or  φ ψ => (construct_seq φ) ++ (construct_seq ψ) ++ [p_or φ ψ]
  | p_imp φ ψ => (construct_seq φ) ++ (construct_seq ψ) ++ [p_imp φ ψ]
  | p_iff φ ψ => (construct_seq φ) ++ (construct_seq ψ) ++ [p_iff φ ψ]

#eval construct_seq complex_WFF

/-- Example --/
def super_complex_WFF : WFF :=
  p_imp (p_and A₁ A₁₀) (p_or (p_not A₃) (p_iff A₈ A₃))

#eval super_complex_WFF
#eval construct_seq super_complex_WFF

/--
下面两个函数分别统计一个公式字符串表示中左括号和右括号的个数。
它们的定义方式仍然是对 `WFF` 做递归。
-/
def WFF_num_left_brackets : WFF → Nat
  -- `Nat` 是自然数类型。
  -- 原子公式没有括号，所以计数是 `0`。
  | p_atm _   => 0
  -- 这里的 `_` 表示“这个参数存在，但这里不关心它具体是什么”。
  -- 每加入一个联结词的外层表示，就会新增一对括号中的左括号
  | p_not φ   => WFF_num_left_brackets φ + 1
  | p_and φ ψ => WFF_num_left_brackets φ + WFF_num_left_brackets ψ + 1
  | p_or  φ ψ => WFF_num_left_brackets φ + WFF_num_left_brackets ψ + 1
  | p_imp φ ψ => WFF_num_left_brackets φ + WFF_num_left_brackets ψ + 1
  | p_iff φ ψ => WFF_num_left_brackets φ + WFF_num_left_brackets ψ + 1

def WFF_num_right_brackets : WFF → Nat
  -- 右括号的计数方式完全平行
  | p_atm _   => 0
  -- 每一层复合构造同样贡献一个右括号
  | p_not φ   => WFF_num_right_brackets φ + 1
  | p_and φ ψ => WFF_num_right_brackets φ + WFF_num_right_brackets ψ + 1
  | p_or  φ ψ => WFF_num_right_brackets φ + WFF_num_right_brackets ψ + 1
  | p_imp φ ψ => WFF_num_right_brackets φ + WFF_num_right_brackets ψ + 1
  | p_iff φ ψ => WFF_num_right_brackets φ + WFF_num_right_brackets ψ + 1

#eval super_complex_WFF
#eval WFF_num_right_brackets super_complex_WFF

/--
`theorem` 用来陈述并证明一个定理。

这里 `∀ f : WFF, ...` 中的 `∀` 读作“对于任意”。
整个命题的意思是：对于任意公式 `f`，左括号数等于右括号数。

`:= by` 表示接下来进入 tactic proof，也就是“用策略一步步构造证明”。
-/
theorem WFF_balance_of_brackets : ∀ f : WFF, WFF_num_left_brackets f = WFF_num_right_brackets f := by
  -- `intro f` 的意思是：把前面 `∀ f : WFF` 中任意给定的 `f` 引入到当前证明上下文里。
  intro f
  -- 对公式的归纳和 `WFF` 的定义方式完全一致
  -- `induction f` 表示对 `f` 做归纳。因为 `WFF` 是归纳定义的，
  -- 所以会自动生成与各个构造子对应的证明目标。
  induction f
  -- `case p_atm => ...` 表示现在处理原子命题这一种情形。
  -- `rfl` 表示“左右两边按定义就是同一个东西”，因此可直接完成证明。
  case p_atm => rfl
  case p_not f' IH_not =>
    -- `unfold` 会把一个定义展开。
    unfold WFF_num_left_brackets
    unfold WFF_num_right_brackets
    -- `rewrite [IH_not]` 用归纳假设 `IH_not` 改写当前目标中的表达式。
    rewrite [IH_not]
    rfl
  case p_and f' g' IH_and_1 IH_and_2 =>
    unfold WFF_num_left_brackets
    unfold WFF_num_right_brackets
    rewrite [IH_and_1, IH_and_2]
    rfl
  case p_or f' g' IH_or_1 IH_or_2 =>
    unfold WFF_num_left_brackets
    unfold WFF_num_right_brackets
    rewrite [IH_or_1, IH_or_2]
    rfl
  case p_imp f' g' IH_imp_1 IH_imp_2 =>
    unfold WFF_num_left_brackets
    unfold WFF_num_right_brackets
    rewrite [IH_imp_1, IH_imp_2]
    rfl
  case p_iff f' g' IH_iff_1 IH_iff_2 =>
    unfold WFF_num_left_brackets
    unfold WFF_num_right_brackets
    rewrite [IH_iff_1, IH_iff_2]
    rfl

/-- The five formation operations appearing in Theorem 1.11. -/
-- 这些函数把“加一个联结词”视为对公式的构造操作
def E_not : WFF → WFF := p_not
-- `WFF × WFF` 表示一个有序对，里面放两个公式。
-- `fun ⟨φ, ψ⟩ => ...` 是匿名函数的写法：
-- `fun` 可以理解为“给定输入，返回输出”；
-- `⟨φ, ψ⟩` 表示把输入这个二元组拆成两个分量 `φ` 和 `ψ`。
def E_and : WFF × WFF → WFF := fun ⟨φ, ψ⟩ => p_and φ ψ
def E_or : WFF × WFF → WFF := fun ⟨φ, ψ⟩ => p_or φ ψ
def E_imp : WFF × WFF → WFF := fun ⟨φ, ψ⟩ => p_imp φ ψ
def E_iff : WFF × WFF → WFF := fun ⟨φ, ψ⟩ => p_iff φ ψ

/-- Part (b): each formation operation is injective. -/
theorem E_not_injective : Function.Injective E_not := by
  intro φ ψ h
  -- 构造子相等时，其参数也必须相等
  -- `exact` 的意思是：后面给出的这一项，正好就是当前目标所需的证明。
  -- `injection h` 利用构造子单射性：若 `p_not φ = p_not ψ`，则可推出 `φ = ψ`。
  exact by injection h

theorem E_and_injective : Function.Injective E_and := by
  intro x y h
  -- `rcases` 用来按模式拆解对象。
  -- 这里把 `x`、`y` 这两个二元组分别拆成两个分量。
  rcases x with ⟨φ₁, ψ₁⟩
  rcases y with ⟨φ₂, ψ₂⟩
  -- `dsimp` 会做直接的化简和定义展开。
  -- `at h ⊢` 表示：既在假设 `h` 中化简，也在当前目标中化简。
  -- 这里的 `⊢` 表示“当前证明目标”。
  dsimp [E_and] at h ⊢
  -- `injection ... with h₁ h₂` 会从构造子相等中提取出分量相等。
  injection h with h₁ h₂
  -- `subst h₁` 表示把等式 `h₁` 对应的变量替换掉。
  -- 替换后，目标通常会变得更简单。
  subst h₁
  subst h₂
  rfl

theorem E_or_injective : Function.Injective E_or := by
  intro x y h
  rcases x with ⟨φ₁, ψ₁⟩
  rcases y with ⟨φ₂, ψ₂⟩
  dsimp [E_or] at h ⊢
  injection h with h₁ h₂
  subst h₁
  subst h₂
  rfl

theorem E_imp_injective : Function.Injective E_imp := by
  intro x y h
  rcases x with ⟨φ₁, ψ₁⟩
  rcases y with ⟨φ₂, ψ₂⟩
  dsimp [E_imp] at h ⊢
  injection h with h₁ h₂
  subst h₁
  subst h₂
  rfl

theorem E_iff_injective : Function.Injective E_iff := by
  intro x y h
  rcases x with ⟨φ₁, ψ₁⟩
  rcases y with ⟨φ₂, ψ₂⟩
  dsimp [E_iff] at h ⊢
  injection h with h₁ h₂
  subst h₁
  subst h₂
  rfl

/-- Part (a): the ranges of the five formation operations are pairwise disjoint. -/
theorem E_not_ne_E_and (φ α β : WFF) : E_not φ ≠ E_and (α, β) := by
  intro h
  -- `cases h` 表示对等式 `h` 分情况分析。
  -- 这里因为两个不同构造子不可能相等，所以会直接产生矛盾，目标自动完成。
  cases h

theorem E_not_ne_E_or (φ α β : WFF) : E_not φ ≠ E_or (α, β) := by
  intro h
  cases h

theorem E_not_ne_E_imp (φ α β : WFF) : E_not φ ≠ E_imp (α, β) := by
  intro h
  cases h

theorem E_not_ne_E_iff (φ α β : WFF) : E_not φ ≠ E_iff (α, β) := by
  intro h
  cases h

theorem E_and_ne_E_or (α β γ δ : WFF) : E_and (α, β) ≠ E_or (γ, δ) := by
  intro h
  cases h

theorem E_and_ne_E_imp (α β γ δ : WFF) : E_and (α, β) ≠ E_imp (γ, δ) := by
  intro h
  cases h

theorem E_and_ne_E_iff (α β γ δ : WFF) : E_and (α, β) ≠ E_iff (γ, δ) := by
  intro h
  cases h

theorem E_or_ne_E_imp (α β γ δ : WFF) : E_or (α, β) ≠ E_imp (γ, δ) := by
  intro h
  cases h

theorem E_or_ne_E_iff (α β γ δ : WFF) : E_or (α, β) ≠ E_iff (γ, δ) := by
  intro h
  cases h

theorem E_imp_ne_E_iff (α β γ δ : WFF) : E_imp (α, β) ≠ E_iff (γ, δ) := by
  intro h
  cases h

/-- Theorem 1.11 (Unique Readability): the five formation operations on `WFF`
have pairwise disjoint ranges and are injective. -/
theorem WFF_unique_readability :
    -- `∧` 表示“并且”。
    (Function.Injective E_not ∧
      Function.Injective E_and ∧
      Function.Injective E_or ∧
      Function.Injective E_imp ∧
      Function.Injective E_iff) ∧
    ((∀ φ α β, E_not φ ≠ E_and (α, β)) ∧
      (∀ φ α β, E_not φ ≠ E_or (α, β)) ∧
      (∀ φ α β, E_not φ ≠ E_imp (α, β)) ∧
      (∀ φ α β, E_not φ ≠ E_iff (α, β)) ∧
      (∀ α β γ δ, E_and (α, β) ≠ E_or (γ, δ)) ∧
      (∀ α β γ δ, E_and (α, β) ≠ E_imp (γ, δ)) ∧
      (∀ α β γ δ, E_and (α, β) ≠ E_iff (γ, δ)) ∧
      (∀ α β γ δ, E_or (α, β) ≠ E_imp (γ, δ)) ∧
      (∀ α β γ δ, E_or (α, β) ≠ E_iff (γ, δ)) ∧
      (∀ α β γ δ, E_imp (α, β) ≠ E_iff (γ, δ))) := by
  -- `constructor` 用于证明一个“并且”命题：把目标拆成左、右两个子目标。
  constructor
  -- `·` 表示一个子证明块的开始。
  · exact ⟨E_not_injective, E_and_injective, E_or_injective, E_imp_injective, E_iff_injective⟩
  -- `⟨..., ...⟩` 是构造“二元组”或“合取证明”的标准写法。
  · exact ⟨E_not_ne_E_and, E_not_ne_E_or, E_not_ne_E_imp, E_not_ne_E_iff,
      E_and_ne_E_or, E_and_ne_E_imp, E_and_ne_E_iff,
      E_or_ne_E_imp, E_or_ne_E_iff, E_imp_ne_E_iff⟩