Lean半群结构

Lean半群结构

半群（Semigroup）是抽象代数中的基本代数结构之一，在Lean定理证明器中，半群的定义和性质通过类型类和结构进行形式化。本章将详细介绍Lean中的半群结构，包括其数学定义、Lean实现方式、代码示例以及实际应用。

数学定义

在数学中，半群是一个集合$S$配备一个二元运算$*$，满足以下性质：

• 封闭性：对于所有$a,b\in S$，有$a*b\in S$。
• 结合律：对于所有$a,b,c\in S$，有$(a*b)*c=a*(b*c)$。

在Lean中，半群通过类型类`Semigroup`定义，其核心是要求一个二元运算`mul`（通常记为`*`）并满足结合律。

Lean中的半群实现

Lean的Mathlib库中定义了`Semigroup`类型类，其结构如下：

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)

这里：

• `G`是半群的载体类型。
• `extends Mul G`表示半群继承自具有乘法运算的类型。
• `mul_assoc`是结合律的公理。

代码示例：定义半群实例

以下是一个自定义半群的例子，使用自然数加法作为运算：

import Mathlib.Algebra.Group.Defs

instance : Semigroup Nat where
  mul := Nat.add
  mul_assoc := Nat.add_assoc

解释：

• `mul := Nat.add`：将半群的乘法定义为自然数的加法。
• `mul_assoc := Nat.add_assoc`：使用`Nat.add_assoc`（自然数加法的结合律）来满足半群的结合律公理。

半群的实际应用

半群在编程和数学中有广泛的应用，以下是一些例子：

字符串拼接

字符串在拼接操作下形成一个半群：

instance : Semigroup String where
  mul := String.append
  mul_assoc := by
    intros a b c
    simp [String.append_assoc]

• `mul := String.append`：将半群的乘法定义为字符串的拼接。
• `mul_assoc`：证明字符串拼接满足结合律。

列表拼接

列表在拼接操作下也形成一个半群：

instance [α : Type] : Semigroup (List α) where
  mul := List.append
  mul_assoc := List.append_assoc

• `mul := List.append`：将半群的乘法定义为列表的拼接。
• `mul_assoc := List.append_assoc`：使用`List.append_assoc`证明结合律。

半群的结合律图示

结合律可以通过以下图示表示：

graph LR A[ (a * b) * c ] -->|结合律| B[ a * (b * c) ]

进阶：半群与幺半群的关系

半群可以扩展为幺半群（Monoid），即增加一个单位元$e$满足$e*a=a*e=a$。在Lean中，幺半群的定义如下：

class Monoid (M : Type u) extends Semigroup M, One M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

总结

• 半群是具有封闭性和结合律的代数结构。
• 在Lean中，半群通过`Semigroup`类型类实现，核心是`mul`和`mul_assoc`。
• 半群广泛应用于字符串、列表等数据结构的操作中。
• 半群可以扩展为幺半群，增加单位元性质。

理解半群是学习更复杂代数结构（如群、环、域）的基础。