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
6
7
Require Import PeanoNat.   (* nat 上的 =? 记号需要它 *)

(* 错误：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).

第一行的 Require Import PeanoNat. 不能省。=? 是 Nat.eqb 的中缀记号，声明在 Coq.Init.Nat 里，但 prelude 只 Require 了这个模块而没有 Import 它（该文件的设计意图就是「整体使用、不导入」，所以定义都得写成 Nat.pred 这种限定形式）。裸写 m =? 0 会先撞上 Unknown interpretation for notation "_ =? _".——那就不是在演示 termination checker 了，教学点会整个跑偏。PeanoNat 在模块外重新声明了这个记号，所以导入它就好。

Fail 命令断言后续命令应当失败。它不是静默的：命令确实失败时 Coq 会打印 The command has indeed failed with message: 再跟上真正的报错正文，这里是 Cannot guess decreasing argument of fix.。如果被断言的命令其实成功了，Fail 自己会报 The command has not failed!。修正方式是重新对构造子做结构归纳：

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)).

Prop、Set 与 Type 该选哪个

前面 MyNat 写的是 : Type，Even 写的是 : Prop，这个选择不是随手定的。Coq 的 sort 分三支：

sort 含义 提取后
Prop 只关心「能不能证」，居民之间的差别不携带信息 被完整擦除
Set 有计算内容的数据类型，nat、bool、list 都在这里 保留
Type(i) 分层的大宇宙，Prop : Type(1)、Set : Type(1)、Type(i) : Type(i+1) 保留

注意 Set 是与 Prop 并列的 base sort，不是「Type(0) 的别名」——层级从 i ≥ 1 起，没有 Type(0)。

选择的判据是「这个东西的居民需不需要在运行时被区分」。判定一个数是否为偶数，只要知道「是」就够了，具体走了哪条推导路径不影响任何计算结果，所以 Even 放 Prop。而 MyNat 的 O 和 S O 必须能被区分，所以放 Type。

这个选择有个硬后果：Prop 里的归纳类型默认不能消去到 Set/Type，也就是不能对它 match 出一个 nat。唯一的例外是 singleton elimination——构造子不超过一个、且其参数全在 Prop 里的类型（eq、False、and 属于这类，or、ex 不属于）。写 Prop 上的 match 想拿出计算结果时会撞上 Incorrect elimination ... 报错，第 14 篇讲程序提取时会把这条规则用到底。

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、Corollary

Lemma、Theorem、Corollary 三者之间对类型检查器确实没有区别，纯粹是语义约定；Let 和 Example 则各有实质差异：

关键字 典型用途 作用域与差异
Let Section 内的局部名称 Section 关闭时会被 zeta 展开进用到它的定义里，不只是「外部不可见」
Example 具体可计算的示例 全局；默认 transparent，Compute 可求值
Lemma 辅助引理 全局；默认 opaque，后续证明可 apply
Theorem 主要定理 全局；与 Lemma 无本质区别
Corollary 推论 全局；与 Theorem 无本质区别

证明语法这里有个硬约束容易记反：只有 Definition、Example、Let 接受 := term 直接给项，Lemma、Theorem、Corollary（以及 Fact、Remark、Proposition、Property）在语法上根本没有 := 分支，只能走 Proof. ... Qed.。想直接写项就把关键字换成 Definition。

另外 Lemma/Theorem 默认产出 opaque 常量而 Definition 默认 transparent，这个差别决定了后续能不能 unfold 它——见本篇末尾关于 Qed 与 Defined 的说明。

模式匹配

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
9
10
11
Require Import List.
Import ListNotations.   (* [1; 2; 3] 这种字面量由它提供 *)

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 *)

:: 和 nil 在 prelude 里（Init/Datatypes），所以 mymap 本身不需要额外导入。坏掉的只有 [1; 2; 3; 4] 这种方括号字面量：它的记号声明在 List.v 的 ListNotations 模块里，不 Import 就用不了。

隐式参数

{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 改为隐式 *)

前面 Arguments Leaf {A}. 用的 {} 默认是 maximally inserted，这正是 Leaf 能不带任何参数直接出现在 match 分支里的原因。

隐式参数是「看不见的东西影响行为」，所以配套的反查手段必须先会：

1
2
3
4
About mymap.        (* 看隐式性标注、scope、opaque/transparent *)
Print mymap.        (* 看定义体本身 *)
Locate "=?".        (* 反查一个记号是哪个模块声明的 *)
Search (_ + 0 = _). (* 按结论形状反查引理，顺带查出它所在的库 *)

本篇第一个 Fail 示例里 =? 不可用的问题，用 Locate "=?" 一句就能自己定位到 Coq.Init.Nat。

贯穿案例：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
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.

(* 验证公理依赖 *)
Print Assumptions node_size_pos.
(* Closed under the global context *)

Print Assumptions 只有两种输出形态：Closed under the global context，或者 Axioms: 后面跟一串条目。看到前者意味着该证明在直觉主义逻辑下完全成立，不依赖排中律、函数外延性或其他非构造性公理。

这里不建议对 lia 产出的引理用 Print 看证明项。lia 走反射式证书检查（它自己就是一行 Ltac：Zify.zify; xlia zchecker），打出来的项以 ZMicromega.ZTautoChecker_sound 为头，后面挂一整棵 reify 之后的语法树加见证列表，肉眼没法读。这也正是 lia 跑得快但证明项巨大的原因。想看人类可读的证明项，挑手写 tactic 证的引理。

Qed 关键字将证明项标记为不透明（opaque），后续推断不会展开其定义；若改用 Defined，则证明项对外透明，可被后续 simpl/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 : length items = sz。用 {| ... |} 语法构造一个包含 [1; 2; 3] 的具体 Stack 值，pf 字段用 ltac:(reflexivity) 填充。注意开头要写 Require Import List. 和 Import ListNotations.——length 虽然在 prelude 里，[1; 2; 3] 的字面量记号不在。

练习 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，按升序插入一个元素到已排序列表中。

参考资料