Gallina 是 Coq 的规范语言（specification language），负责定义类型、函数和命题；tactic 语言（Ltac/Ltac2）只是证明搜索的外壳，最终生成的证明项本质上仍是 Gallina 表达式。本篇是一张速查表，覆盖 Definition、Fixpoint、Inductive、Record、Section、Module 六个核心构造，以及模式匹配、匿名函数、隐式参数的基本用法，目标是让读者能独立写出完整的 .v 文件并通过 coqc 零 warning 编译。前置阅读：形式化方法系列《归纳类型与递归——把数据嵌入证明》和《依值类型——从命题逻辑到一阶逻辑》。

Definition

Definition 引入一个全局名称，绑定到一个 Gallina 表达式。类型标注可选；省略时 Coq 从右侧推断。

1
2
3
4
5
6
7
8
(* 带类型标注 *)
Definition double : nat -> nat := fun n => n + n.

(* 省略类型标注，Coq 推断 *)
Definition triple n := n + n + n.

(* 常量 *)
Definition answer : nat := 42.

Definition 支持多参数的语法糖，下面两行等价：

1
2
Definition add (m n : nat) : nat := m + n.
Definition add' : nat -> nat -> nat := fun m n => m + n.

Print 命令查看 Coq 内部展开后的表示：

1
2
Print double.
(* double = fun n : nat => n + n : nat -> nat *)

Fixpoint

Fixpoint 用于结构递归函数。Coq 的 termination checker 要求每次递归调用的某个参数必须在结构上严格变小；若无法自动判定，需要用 {struct arg} 显式指定递减参数。

1
2
3
4
5
Fixpoint plus (m n : nat) : nat :=
  match m with
  | O    => n
  | S m' => S (plus m' n)
  end.

失败示例：不按结构递减的写法会被 Coq 拒绝。

1
2
3
4
5
(* 错误：Coq 无法确认 m - 2 是结构上变小的 *)
Fail Fixpoint bad_half (m : nat) : nat :=
  if m =? 0 then 0
  else if m =? 1 then 0
  else 1 + bad_half (m - 2).

Fail 命令断言后续命令应当失败，常用于文档化不合法的写法。修正方式是重新对构造子做结构归纳：

1
2
3
4
5
6
7
(* 正确：对 nat 构造子做嵌套 match，每次递减两步 *)
Fixpoint half (m : nat) : nat :=
  match m with
  | O        => O
  | S O      => O
  | S (S m') => S (half m')
  end.

{struct arg} 标注在参数顺序不明显时有用：

1
2
3
4
5
Fixpoint size_list {A : Type} (l : list A) {struct l} : nat :=
  match l with
  | nil    => O
  | _ :: t => S (size_list t)
  end.

Inductive

Inductive 定义归纳类型，语法是列出构造子及其签名。前置系列第《归纳类型与递归》篇已从类型论角度解释了归纳类型的消去规则；本节只列实用写法。

自然数（标准库已有 nat，此处仅示例语法）：

1
2
3
Inductive MyNat : Type :=
  | Z    : MyNat
  | Succ : MyNat -> MyNat.

多态列表：

1
2
3
4
5
6
Inductive MyList (A : Type) : Type :=
  | Nil  : MyList A
  | Cons : A -> MyList A -> MyList A.

Arguments Nil  {A}.
Arguments Cons {A}.

二叉树（本篇贯穿案例）：

1
2
3
4
5
6
Inductive BTree (A : Type) : Type :=
  | Leaf : BTree A
  | Node : BTree A -> A -> BTree A -> BTree A.

Arguments Leaf {A}.
Arguments Node {A}.

命题（Prop 宇宙中的归纳类型）：

1
2
3
4
(* 偶数的归纳定义 *)
Inductive Even : nat -> Prop :=
  | Even_O  : Even 0
  | Even_SS : forall n, Even n -> Even (S (S n)).

Record

Record 是有名字段的乘积类型的语法糖，编译后展开为单构造子的 Inductive。

1
2
3
4
Record Point2D : Type := Build_Point2D {
  px : nat;
  py : nat
}.

构造一个 Point2D：

1
2
3
4
Definition origin : Point2D := Build_Point2D 0 0.

(* 也可用 record 表达式语法 *)
Definition p1 : Point2D := {| px := 3; py := 4 |}.

字段投影函数由 Coq 自动生成，名称即字段名：

1
2
Compute px p1.   (* = 3 : nat *)
Compute py p1.   (* = 4 : nat *)

Record 的字段类型可以依赖之前的字段，构成依值记录。下面定义一个有界自然数类型，要求 value < bound 作为字段内嵌的证明：

1
2
3
4
5
6
7
Require Import Lia.

Record BoundedNat : Type := MkBoundedNat {
  bound : nat;
  value : nat;
  pf    : value < bound
}.

构造一个具体值，pf 字段用 ltac:(lia) 在原地生成证明项：

1
2
Definition three_lt_ten : BoundedNat :=
  MkBoundedNat 10 3 ltac:(lia).

ltac:(...) 语法允许在 term 位置内嵌一段 tactic，Coq 8.5+ 均支持。

Section 与 Variable

Section 提供局部作用域，Variable（别名 Hypothesis）在 Section 内声明局部假设；Section 关闭后，所有用到这些变量的定义会自动将它们提升为普通参数。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Section TreeOps.

  Variable A : Type.

  Fixpoint size (t : BTree A) : nat :=
    match t with
    | Leaf       => 0
    | Node l _ r => 1 + size l + size r
    end.

  Fixpoint mirror (t : BTree A) : BTree A :=
    match t with
    | Leaf       => Leaf
    | Node l v r => Node (mirror r) v (mirror l)
    end.

End TreeOps.

Section 关闭后，size 的实际类型变为 forall (A : Type), BTree A -> nat——A 被自动提升为第一个显式参数。若要让它隐式，在 Section 内用 Context {A : Type}. 代替 Variable A : Type.：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Section TreeOps2.

  Context {A : Type}.

  Fixpoint height (t : BTree A) : nat :=
    match t with
    | Leaf       => 0
    | Node l _ r => 1 + Nat.max (height l) (height r)
    end.

End TreeOps2.

(* height 的类型为 forall {A : Type}, BTree A -> nat *)
Check @height.

Module 与 Module Type

Module 提供命名空间，Module Type 定义接口（签名）。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Module Type MONOID.
  Parameter T  : Type.
  Parameter op : T -> T -> T.
  Parameter e  : T.
  Axiom assoc    : forall a b c, op a (op b c) = op (op a b) c.
  Axiom left_id  : forall a, op e a = a.
  Axiom right_id : forall a, op a e = a.
End MONOID.

Module NatAddMonoid <: MONOID.
  Definition T  := nat.
  Definition op := Nat.add.
  Definition e  := 0.
  Lemma assoc    : forall a b c, a + (b + c) = a + b + c.  Proof. lia. Qed.
  Lemma left_id  : forall a, 0 + a = a.                    Proof. lia. Qed.
  Lemma right_id : forall a, a + 0 = a.                    Proof. lia. Qed.
End NatAddMonoid.

<: 表示 NatAddMonoid 必须满足 MONOID 签名；字段缺失或类型不匹配时 Coq 在 End 处报错。

Module 内部名称通过限定符访问，或用 Import 打开：

1
Compute NatAddMonoid.op 3 4.   (* = 7 : nat *)

Let、Example、Lemma、Theorem

这五个关键字对 Coq 类型检查器没有本质区别，差异仅在语义约定和作用域：

关键字 典型用途 作用域
Let Section 内的局部名称 Section 内；外部不可见
Example 具体可计算的示例 全局；Compute 可求值
Lemma 辅助引理 全局；后续证明可 apply
Theorem 主要定理 全局；与 Lemma 无本质区别
Corollary 推论 全局；与 Theorem 无本质区别

所有这些关键字都接受相同的证明语法（:= term 直接给证明项，或 Proof. ... Qed. tactic 块）。

模式匹配

match ... with ... end 是 Gallina 的消去子，覆盖归纳类型所有构造子，Coq 要求匹配穷尽。

1
2
3
4
5
Definition is_zero (n : nat) : bool :=
  match n with
  | O   => true
  | S _ => false
  end.

嵌套模式：

1
2
3
4
5
Definition pred2 (n : nat) : nat :=
  match n with
  | S (S n') => n'
  | _        => O
  end.

在 Fixpoint 中配合递归，match 是唯一的分支机制（bool 有 if-then-else 语法糖，但本质仍是 match）：

1
2
3
4
5
Fixpoint depth {A : Type} (t : BTree A) : nat :=
  match t with
  | Leaf       => 0
  | Node l _ r => 1 + Nat.max (depth l) (depth r)
  end.

匿名函数

fun x => body 构造一个 λ 表达式，多参数直接列出：

1
2
Definition add3 : nat -> nat -> nat -> nat :=
  fun a b c => a + b + c.

类型标注可选：

1
2
Check (fun (n : nat) => n * 2).
(* : nat -> nat *)

高阶函数常与匿名函数配合：

1
2
3
4
5
6
7
8
Fixpoint mymap {A B : Type} (f : A -> B) (l : list A) : list B :=
  match l with
  | nil    => nil
  | h :: t => f h :: mymap f t
  end.

Compute mymap (fun n => n * n) [1; 2; 3; 4].
(* = [1; 4; 9; 16] : list nat *)

隐式参数

{A : Type} 将 A 声明为隐式参数，Coq 在调用时根据其他参数的类型自动推断；(A : Type) 是显式参数，调用时必须提供。

1
2
3
4
5
Definition id_explicit (A : Type) (x : A) : A := x.
Definition id_implicit {A : Type} (x : A) : A := x.

Check id_explicit nat 3.   (* : nat *)
Check id_implicit 3.       (* : nat，A 由 3 的类型自动推断 *)

@ 前缀强制显式传递所有参数，包括隐式参数：

1
Check @id_implicit nat 3.  (* 与 id_explicit nat 3 等价 *)

Arguments 命令可以在定义之后调整隐式性：

1
Arguments mymap {A B}.   (* A B 改为隐式 *)

贯穿案例：BTree size 的正确性

下面的片段综合前面所有构造，可直接复制为 btree.v 并用 coqc btree.v 验证。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
Require Import Lia.

Inductive BTree (A : Type) : Type :=
  | Leaf : BTree A
  | Node : BTree A -> A -> BTree A -> BTree A.

Arguments Leaf {A}.
Arguments Node {A}.

Fixpoint size {A : Type} (t : BTree A) : nat :=
  match t with
  | Leaf       => 0
  | Node l _ r => 1 + size l + size r
  end.

(* 非空树的 size >= 1 *)
Lemma node_size_pos :
  forall {A : Type} (l r : BTree A) (v : A),
    size (Node l v r) >= 1.
Proof.
  intros A l r v.
  simpl.
  lia.
Qed.

(* 查看 Coq 生成的证明项 *)
Print node_size_pos.
(*
node_size_pos =
  fun (A : Type) (l r : BTree A) (v : A) =>
    Nat.le_succ_l 0 (size l + size r) ...
  : forall {A : Type} (l r : BTree A) (v : A),
      size (Node l v r) >= 1
*)

(* 验证公理依赖 *)
Print Assumptions node_size_pos.
(* Axioms: none *)

Print Assumptions 输出 Axioms: none 意味着该证明在直觉主义逻辑下完全成立，不依赖排中律、函数外延性或其他非构造性公理。Qed 关键字将证明项标记为不透明（opaque），后续推断不会展开其定义；若改用 Defined，则证明项对外透明，可被后续 simp/unfold 展开。

速查表

构造 语法骨架 典型用途
Definition Definition f (x : T) : U := body. 非递归函数、常量
Fixpoint Fixpoint f (x : T) {struct x} : U := match x with ... 结构递归函数
Inductive Inductive T : Sort := | C1 : ... | C2 : ... 新类型、归纳命题
Record Record R := Build_R { f1 : T1; f2 : T2 }. 有名字段的乘积类型
Section/Variable Section S. Variable A : Type. ... End S. 局部参数、假设
Module/Module Type Module M <: MT. ... End M. 命名空间、接口
match match e with | P1 => b1 | P2 => b2 end 模式匹配
fun fun x : T => body 匿名函数
{A : T} 隐式参数声明 自动推断类型参数
@f 显式传递全部参数 绕过隐式推断

练习

练习 1：为 BTree 定义 mirror 函数（镜像翻转左右子树），并证明 forall {A} (t : BTree A), mirror (mirror t) = t。证明思路：induction t，对 Leaf 分支 reflexivity，对 Node 分支用归纳假设加 simpl 和 congruence。

练习 2：定义一个 Stack Record，字段为 items : list nat 和 sz : nat，外加一致性证明字段 pf : List.length items = sz。用 {| ... |} 语法构造一个包含 [1; 2; 3] 的具体 Stack 值，pf 字段用 ltac:(reflexivity) 填充。

练习 3（较难）：定义 Module Type ORDERED，包含类型 T、比较函数 leb : T -> T -> bool 和自反性公理 leb_refl : forall x, leb x x = true。实现 NatOrdered <: ORDERED，并在其内部编写 Fixpoint insert : nat -> list nat -> list nat，按升序插入一个元素到已排序列表中。

参考资料