深入 Coq 14：程序提取

Coq 不仅是证明助手，也是一门带有计算语义的函数式语言。通过 Extraction 机制，Gallina 程序可以被翻译成 OCaml、Haskell 或 Scheme 的可运行代码，同时抹去所有停留在 Prop 宇宙中的证明项。本文覆盖 Extraction 的核心命令、类型映射指令、内联控制、性能陷阱，以及一个从证明到编译运行的完整示例。

前置阅读：本系列前三篇（01 开发环境与项目结构、02 目标窗口与 tactic 交互模型、03 Gallina 核心语法速查）以及第 09 篇（归纳证明）提供了本文所需的 Gallina 和 tactic 基础。

Extraction 机制概览

Extraction 的基础是 Curry-Howard 同构的计算部分：类型为 A : Type 或 A : Set 的项携带运行时数据，而类型为 P : Prop 的项纯粹是逻辑断言，不携带可观察的计算内容。提取器（extractor）遍历 Gallina 的 proof term，遇到 Prop 宇宙中的构造子时直接擦除，只保留 Type/Set 宇宙的骨架，再将剩余的 CIC 项翻译成目标语言的 AST。

提取后得到的代码是纯粹的语义等价物：若 Coq 端证明了 sort_correct，提取后的 sort 函数在 OCaml 里运行时同样满足该性质——前提是提取映射本身是可信的，且没有引入不可信公理。

Coq 8.x 内置三个提取后端：

目标语言	加载命令	输出格式
OCaml	内置，无需加载	.ml / .mli
Haskell	Require Extraction.	.hs
Scheme	Require Extraction.	.scm

OCaml 后端最成熟，性能最好，也是 CompCert、Bedrock2 等项目选用的提取目标。本文以 OCaml 为主，Haskell 为辅做对比。

Extraction 与 Recursive Extraction

基本用法

Require Extraction.

(* 提取单个定义到终端 *)
Extraction plus.

(* 提取单个定义到文件 *)
Extraction "plus.ml" plus.

(* 提取定义及其全部传递依赖 *)
Recursive Extraction plus.

(* 提取到文件，包含所有依赖 *)
Extraction Library Arith.

Extraction ident 只输出 ident 本身的定义；若依赖项未被显式列出，Coq 会假定它们已在目标语言中存在。Recursive Extraction ident 则递归收集所有依赖，适合自包含的单文件输出。

简单示例

Require Extraction.

Fixpoint my_length {A : Type} (l : list A) : nat :=
  match l with
  | nil     => 0
  | _ :: t  => S (my_length t)
  end.

Extraction my_length.

提取结果（OCaml）：

(** val my_length : 'a1 list -> nat **)

let rec my_length = function
  | Nil -> O
  | Cons (_, t) -> S (my_length t)

A : Type 被擦除为多态类型变量 'a1；nat 保留为归纳类型，因为它在 Type 宇宙中。

提取到独立模块

实际项目中通常将整个 Coq 文件提取为一个 OCaml 模块：

(* Verified.v *)
Require Extraction.

(* ... 定义和证明 ... *)

Extraction "verified.ml" my_function.

在 _CoqProject 里列出 Verified.v，运行 coq_makefile 生成 Makefile 后，make 会自动触发提取并生成 verified.ml。

Prop 与 Type：擦除的边界

为什么证明消失

Coq 的宇宙层级决定了哪些项会被提取：

Check True : Prop.     (* Prop 宇宙，逻辑命题 *)
Check nat  : Set.      (* Set ⊆ Type，携带计算内容 *)
Check Type.            (* 累积宇宙层级的顶端 *)

提取器的规则很简单：

• 类型在 Prop 中的项 → 擦除（替换为 __ 或直接删除）
• 类型在 Set 或 Type 中的项 → 保留并翻译

因此一个形如 {n : nat | n > 0} 的 sigma 类型，其中的证明部分 n > 0 : Prop 会被擦除，只保留 n : nat。

Definition pos_nat := {n : nat | n > 0}.

Definition make_pos (n : nat) (H : n > 0) : pos_nat :=
  exist _ n H.

Extraction make_pos.

提取结果：

(** val make_pos : nat -> __ -> nat **)

let make_pos n _ = n

H : n > 0 变成了 __（OCaml 中 Coq 的占位类型），参数名为 _，函数体直接返回 n。这个行为是预期的——证明项在运行时没有计算意义。

证明相关性与 Prop 的特殊性

Coq 中 Prop 内的两个居民（两个证明）在提取时被视为同一对象，这来自 proof irrelevance 的语义承诺。因此依赖 Prop 居民做分支的代码在提取后行为是透明的：所有分支都被擦除。

(* 这个函数在 Prop 上做分支，提取后分支消失 *)
Definition choose (P : Prop) (H : P \/ ~P) (x y : nat) : nat :=
  match H with
  | or_introl _ => x
  | or_intror _ => y
  end.

Extraction choose.
(* 结果：let choose _ _ x _ = x   -- 提取器选第一个分支 *)

若需在提取代码中保留分支，谓词必须放在 Type 宇宙中（使用 sumbool）。

(* sumbool 在 Set 中，提取后分支保留 *)
Definition choose' (P Q : Prop) (H : {P} + {Q}) (x y : nat) : nat :=
  if H then x else y.

Extraction choose'.
(* 结果：let choose' h x y = if h then x else y *)

Extract Inductive 与 Extract Constant

将 Coq 类型映射到目标语言类型

默认情况下，nat 提取为：

type nat = O | S of nat

这是一个一元（unary）编码，计算复杂度极差：加法 O(n)，乘法 O(n²)。对于任何涉及实际数值计算的程序，必须用 Extract Inductive 将 nat 替换为机器整数。

Require Extraction.
Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.

(* ExtrOcamlNatInt 内部包含以下指令：*)
Extract Inductive nat => "int"
  [ "0" "(fun n -> n + 1)" ]
  "(fun fO fS n -> if n = 0 then fO () else fS (n - 1))".

三个参数依次是：目标语言类型名、构造子的映射列表、消去子（case 分析函数）。

标准库提供了多个预置映射文件：

文件	作用
ExtrOcamlBasic	bool、option、list、pair 映射到 OCaml 内置
ExtrOcamlNatInt	nat → int
ExtrOcamlZInt	Z → int
ExtrOcamlString	string → OCaml string
ExtrHaskellBasic	Haskell 对应版本

Extract Constant

Extract Constant 将单个 Coq 常量映射到目标语言的具体实现：

Extract Constant Nat.add => "(+)".
Extract Constant Nat.mul => "( * )".
Extract Constant Nat.eqb => "(=)".

这在替换了 nat 为 int 之后尤其重要：若只替换类型而不替换运算，加法仍然走原来的递归实现，映射不完整。

对于无法在 Coq 内部实现、只能靠目标语言提供的功能（如文件 I/O、随机数），Extract Constant 配合 Parameter 声明是标准做法：

(* Coq 端只声明类型签名 *)
Parameter random_nat : nat -> nat.

(* 提取时替换为 OCaml 实现 *)
Extract Constant random_nat => "fun n -> Random.int n".

Extraction Inline 与 NoInline

提取器默认对小函数进行内联，有时会让生成代码变得臃肿，有时则期望强制内联来消除中间层。

(* 强制内联：提取时将 succ 展开到调用点 *)
Extraction Inline Nat.succ.

(* 阻止内联：保留函数调用形式 *)
Extraction NoInline Nat.add.

Extraction Inline 对辅助函数特别有用：若 Coq 端有大量短小的 helper，提取后内联可以消除函数调用开销。Extraction NoInline 适用于需要保留函数边界以便在 OCaml 端打 patch 或替换实现的情形。

Print Assumptions：验证提取基础

提取代码的可信性依赖于证明的可信性。若某个定理依赖了 Classical 公理或 Axiom 声明，提取出的代码在逻辑上有额外假设，可能与目标语言语义不对应。

Require Import Coq.Arith.Arith.

Lemma add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m. induction n.
  - simpl. rewrite Nat.add_0_r. reflexivity.
  - simpl. rewrite IHn. rewrite Nat.add_succ_r. reflexivity.
Qed.

Print Assumptions add_comm.
(* 输出：Closed under the global context *)

Closed under the global context 表示该定理不依赖任何公理，完全在 CIC 的构造性框架内证明，提取代码是可信的。

若输出列出了公理，例如：

Axioms:
Classical.classic : forall P : Prop, P \/ ~ P

则提取出的代码隐含了排中律，程序行为在可计算性语义下不再有完整保证。对于追求可信提取的项目，应在开发过程中定期检查 Print Assumptions，确保核心定理无公理依赖。

完整示例：归并排序的提取与运行

Coq 端定义

Require Import List Arith.
Require Extraction.
Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.

Import ListNotations.

(* 归并两个有序列表 *)
Fixpoint merge (l1 l2 : list nat) : list nat :=
  match l1, l2 with
  | [], _  => l2
  | _, []  => l1
  | h1 :: t1, h2 :: t2 =>
      if Nat.leb h1 h2
      then h1 :: merge t1 l2
      else h2 :: merge l1 t2
  end.

(* 按长度分割列表 *)
Fixpoint split_list {A} (l : list A) : list A * list A :=
  match l with
  | []  => ([], [])
  | [x] => ([x], [])
  | x :: y :: t =>
      let (l1, l2) := split_list t in
      (x :: l1, y :: l2)
  end.

(* 归并排序——使用 Program Fixpoint 处理递归度量 *)
Require Import Program.

Program Fixpoint mergesort (l : list nat) {measure (length l)} : list nat :=
  match l with
  | []  => []
  | [x] => [x]
  | _   =>
      let (l1, l2) := split_list l in
      merge (mergesort l1) (mergesort l2)
  end.
Next Obligation.
  destruct l as [|a [|b t]]; simpl in *; try omega.
  destruct (split_list t) eqn:Hsplit. simpl.
  pose proof (split_list_length t l1 l2 Hsplit). omega.
Defined.
Next Obligation.
  destruct l as [|a [|b t]]; simpl in *; try omega.
  destruct (split_list t) eqn:Hsplit. simpl.
  pose proof (split_list_length t l1 l2 Hsplit). omega.
Defined.

上面的 split_list_length 需要先证明一个引理——split_list 的两个分片长度均严格小于原列表（当原列表长度 ≥ 2 时）。这是 Program Fixpoint 终止证明所需的。完整代码见下方。

终止性引理

Lemma split_list_length :
  forall (A : Type) (l l1 l2 : list A),
    split_list l = (l1, l2) ->
    length l >= 2 ->
    length l1 < length l /\ length l2 < length l.
Proof.
  induction l as [|a [|b t] IH] using list_ind2.
  - intros. simpl in *. inversion H. subst. simpl in H0. omega.
  - intros. simpl in *. inversion H. subst. simpl in H0. omega.
  - intros l1 l2 Hsplit Hlen.
    simpl in Hsplit.
    destruct (split_list t) as [t1 t2] eqn:Ht.
    inversion Hsplit; subst.
    simpl.
    destruct (le_lt_dec 2 (length t)) as [Hge | Hlt].
    + destruct (IH t1 t2 Ht Hge) as [H1 H2]. omega.
    + destruct t as [|c [|d rest]]; simpl in *; try omega.
      all: inversion Ht; subst; simpl; omega.
Qed.

Print Assumptions split_list_length.
(* 输出：Closed under the global context *)

提取指令

Extract Inlined Constant Nat.leb => "(<=)".

Extraction "mergesort.ml" mergesort merge split_list.

生成的 OCaml 代码（节选）

let rec merge l1 l2 =
  match l1, l2 with
  | [], _ -> l2
  | _, [] -> l1
  | h1 :: t1, h2 :: t2 ->
    if h1 <= h2 then h1 :: merge t1 l2
    else h2 :: merge l1 t2

let rec mergesort l =
  match l with
  | [] -> []
  | [x] -> [x]
  | _ ->
    let (l1, l2) = split_list l in
    merge (mergesort l1) (mergesort l2)

编译与运行

# 在 mergesort.ml 末尾追加测试入口
cat >> mergesort.ml << 'EOF'

let () =
  let result = mergesort [5; 3; 8; 1; 9; 2; 7; 4; 6] in
  List.iter (fun x -> Printf.printf "%d " x) result;
  print_newline ()
EOF

ocamlfind ocamlopt -package str -linkpkg mergesort.ml -o mergesort 2>/dev/null \
  || ocamlopt mergesort.ml -o mergesort

./mergesort
# 输出：1 2 3 4 5 6 7 8 9

性能陷阱

一元 nat 的代价

未做任何映射时，nat 的提取形式是链表结构。Nat.add 1000 1000 在 OCaml 中需要做 1000 次 S 构造。Nat.mul 100 100 的复杂度是 O(n²)。任何需要在提取代码中做实际数值运算的程序，必须通过 ExtrOcamlNatInt 或等价的 Extract Inductive 指令将 nat 映射到机器整数。

失败路径：

(* 未加任何映射指令，直接提取 *)
Extraction "bad_arith.ml" Nat.mul.
(* 生成：let rec mul n m = match n with O -> O | S p -> add m (mul p m) *)
(* mul 1000 1000 需要 10^6 次递归调用 *)

正确路径：

Require Import ExtrOcamlNatInt.
Extract Constant Nat.mul => "( * )".
Extraction "good_arith.ml" Nat.mul.
(* 生成：let mul = ( * ) *)

Haskell 后端的惰性求值陷阱

Haskell 使用惰性求值，而 Coq 的计算语义是严格的（call-by-value）。当把严格的 Coq 程序提取到 Haskell 时，以下情况会产生语义差异：

递归定义中若某分支在 Haskell 端不会被求值（因为惰性），即便 Coq 端已证明终止，Haskell 端也不会触发对应的计算——这通常没有问题。但若提取的函数依赖副作用顺序（通过 IO monad 模拟），严格与惰性的差异会导致执行顺序不同。

解决方案是在 Haskell 提取时显式使用 seq 强制求值，或在 Coq 端将有顺序依赖的操作建模为状态机而非裸函数。

依赖类型与运行时擦除的边界

带依赖类型的 sigma 类型 {x : A | P x} 在提取后变为裸类型 A，证明部分完全消失。这意味着提取出的 OCaml 代码不再携带运行时的合法性保证；若在 OCaml 端直接修改了提取代码，并传入不满足 P x 的值，不会有任何运行时错误，但函数行为未定义（在 Coq 语义下）。

依赖类型只在 Coq 的静态检查层生效。提取的用途是生成经过静态验证的高效代码，而非在运行时保持不变式检查。

一个常见错误与修复

错误：对 Prop 类型做 match 并期望提取出分支

(* 错误写法：H : A \/ B 在 Prop 中，match 会被擦除 *)
Definition bad_choice (A B : Prop) (H : A \/ B) : nat :=
  match H with
  | or_introl _ => 0
  | or_intror _ => 1
  end.

Extraction bad_choice.
(* 提取结果：let bad_choice _ _ _ = 0  -- 总是返回 0，右分支消失 *)

提取器选择第一个分支作为擦除后的占位，右分支的计算内容（返回 1）在提取后不可见。

修复：改用 sumbool

(* 正确写法：sumbool 在 Set 中，分支得以保留 *)
Definition good_choice (A B : Prop) (H : {A} + {B}) : nat :=
  if H then 0 else 1.

Extraction good_choice.
(* 提取结果：let good_choice h = if h then 0 else 1 *)

sumbool 的定义是 Inductive sumbool (A B : Prop) : Set := left : A -> {A}+{B} | right : B -> {A}+{B}，它居住在 Set 中，因此两个构造子都会被提取。

类似地，sumor、sig（在 Type 中）、sigT 都是在提取场景下携带计算分支的常用类型。

Show Proof 与提取前的验证

在证明某个将被提取的函数的性质时，Show Proof 可以用来确认 proof term 的结构，从而预判提取结果：

Lemma add_O_r : forall n : nat, n + 0 = n.
Proof.
  intro n. induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
  Show Proof.
  (* 显示：(fun n : nat =>
       nat_ind (fun n0 : nat => n0 + 0 = n0)
         eq_refl
         (fun (n0 : nat) (IHn : n0 + 0 = n0) =>
           eq_ind_r (fun n1 : nat => S n1 = S n0) eq_refl IHn) n) *)
Qed.

add_O_r 的类型是等式命题（Prop），整个 proof term 在提取时会被完整擦除。若需要将某个类型为 Type 的构造性结果提取出来，Show Proof 是在 Qed 之前检查 proof term 是否包含期望计算结构的有效工具。

练习

练习 1：定义一个 Coq 函数 insert_sorted : nat -> list nat -> list nat，将一个自然数插入有序列表并保持有序，同时证明结果确实有序（使用 Sorted 或自定义谓词）。用 ExtrOcamlNatInt 和 ExtrOcamlBasic 将其提取为 OCaml，在 OCaml 顶层（utop 或 ocaml）中测试 insert_sorted 4 [1;2;3;5;6] 的输出。

练习 2：将如下 Coq 定义提取到 Haskell，并用 ghc 编译：

Fixpoint fib (n : nat) : nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | S (S n' as m) => fib m + fib n'
  end.

观察未加映射时 fib 30 的运行时间，再加入 ExtrHaskellNatInt（或等价指令）后重新编译，比较两次运行时间。解释差异来源。

练习 3：定义一个函数 safe_div : nat -> {m : nat | m > 0} -> nat，对第一个参数除以第二个参数（sigma 类型保证分母非零）。提取到 OCaml，观察 sigma 类型中的证明部分如何被擦除，并说明提取后的 OCaml 函数在类型层面失去了哪些静态保证。

---

参考资料：

• Coq 官方文档 Extraction of programs in Objective Caml and Haskell，Coq 8.19 Reference Manual 第 25 章
• Pierre Letouzey. A New Extraction for Coq. TYPES 2002.
• Xavier Leroy et al. CompCert C Compiler——CompCert 项目是 Coq 提取到 OCaml 的最大规模工程案例
• 本系列第 01 篇（开发环境）、第 03 篇（Gallina 核心语法）、第 09 篇（归纳证明）提供 Extraction 所需前置知识