深入 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 里运行时同样满足该性质。

这里有个前提要单独拎出来说：提取映射本身也在可信基底里，而它把 TCB 显著加长了。提取器是 Coq kernel 之外的一个 OCaml 插件（plugins/extraction/，约万行代码），从未被形式化验证；它的输出还要交给同样未经验证的 OCaml 编译器和运行时。提取之前需要信任的是「kernel + 引入的公理」，提取之后变成「kernel + 公理 + 提取器 + OCaml 编译器 + OCaml runtime」。

不同项目对这条链的处理方式不一样。CompCert 把「编译」这一环也搬进 Coq 里证明，缩短了后半段；CakeML 更进一步，做到了 verified extraction 与 bootstrapping。普通项目达不到这个程度，但至少应当清楚这条链上有哪些未验证的环节。

用任何提取命令之前都要先加载框架，8.11 起这是硬要求：

Require Extraction.
(* 或更稳健的 From Coq Require Extraction. *)

加载之后，切换目标语言靠 Extraction Language，不是靠 Require：

目标语言	切换命令	输出格式
OCaml	Extraction Language OCaml.（默认，可省）	.ml / .mli
Haskell	Extraction Language Haskell.	.hs
Scheme	Extraction Language Scheme.	.scm
JSON	Extraction Language JSON.	.json

JSON 后端输出的是提取器内部的中间 ML 项，主要给调试和自己写后端的人用。

OCaml 后端最成熟，也是 CompCert 采用的提取目标。本文以 OCaml 为主，Haskell 为辅做对比。

Extraction 与 Recursive Extraction

基本用法

Require Extraction.

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

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

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

(* 把整个 Arith.v 提取成 Arith.ml，不含依赖 *)
Extraction Library Arith.

(* Arith.v 及其全部依赖，逐库一个 .ml *)
Recursive Extraction Library Arith.

(* 按源 .v 拆分，只取需要的部分 —— 多文件工程的常用出口 *)
Separate Extraction plus.

Extraction ident 只输出 ident 本身的定义；若依赖项未被显式列出，Coq 会假定它们已在目标语言中存在。Recursive Extraction ident 则递归收集所有依赖，适合自包含的单文件输出。注意 Extraction Library 和 Recursive Extraction Library 的差别正在「含不含依赖」上，名字里带 Recursive 的那个才含。

还有三个工程上迟早会用到的：

• Extraction TestCompile qualid —— 用 Coq 自带的 OCaml 编译器编译一份临时产物，CI 里验证「提取 + 编译」双通过就靠它。
• Extraction Blacklist String List. —— 避免生成的模块名撞上 OCaml 标准库，这是新手第一个会撞的坑。配套有 Print Extraction Blacklist 和 Reset Extraction Blacklist。
• Extraction Implicit qualid [ ... ] —— 手工消掉提取时多余的隐式参数。默认开着的 Extraction SafeImplicits 会把没消掉的隐式参数报成错误而不是警告。

简单示例

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.            (* 每次出现都分配一个新的宇宙变量；层级无上界 *)

提取器按项的类型所在 sort 决定去留：

• 类型在 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 这个参数整个消失了，不是变成一个 _ 形参。这一点容易记错：__ 确实存在，但它出现在类型位置（提取器用它表示被擦掉的逻辑类型），而顶层的逻辑形参会被直接删掉——Extraction Conservative Types 默认是关的，开了它才会保留形参位置。

官方 refman 自己的例子最能说明问题：eucl_dev 在 Coq 里的类型是 forall b:nat, b > 0 -> forall a:nat, diveucl a b，三个参数中间夹一个 Prop，提取出来的签名是 nat -> nat -> diveucl，只剩两个。

搞错这个区分的后果是，会以为提取产物的签名被证明参数污染了，从而去找不存在的问题。

证明相关性与 Prop 的特殊性

擦除能成立的理由不是 proof irrelevance——Coq 的 Prop 并不具备定义性证明无关性（SProp 才有，那也是它整章存在的理由）。真正的依据是 sort 消去限制：Prop 里的居民本来就不允许被消去到 Set/Type，所以它不可能影响任何运行时值，丢掉是安全的。

这条限制的直接后果是，想在 Prop 上做分支拿出计算结果，代码压根过不了类型检查：

Fail Definition choose (P Q : Prop) (H : P \/ Q) (x y : nat) : nat :=
  match H with
  | or_introl _ => x
  | or_intror _ => y
  end.
(* Incorrect elimination of "H" in the inductive type "or":
   the return type has sort "Set" while it should be SProp or Prop.
   Elimination of an inductive object of sort Prop
   is not allowed on a predicate in sort Set
   because proofs can be eliminated only to build proofs. *)

所以这里没有「提取器替你选了哪个分支」的问题——它连提取那一步都到不了。

例外是 singleton elimination：构造子不超过一个、且其参数全在 Prop 里的归纳类型可以被消去到任意 sort。eq、False、and 属于这一类，or、ex 不属于。这也是 rewrite（本质是对 eq 做消去）能在计算内容里正常工作的原因。

要在提取产物里保留分支，得把判定放进 Set——标准做法是 sumbool：

Require Import ExtrOcamlBasic.   (* 把 sumbool 映成 OCaml bool *)

Definition choose' (P Q : Prop) (H : {P} + {Q}) (x y : nat) : nat :=
  if H then x else y.

Extraction choose'.
(* 加载了 ExtrOcamlBasic 时：let choose' h x y = if h then x else y
   不加载时 sumbool 提取成 type sumbool = Left | Right，代码是
   match h with | Left -> x | Right -> y *)

{P} + {Q} 是 sumbool P Q 的记号，它住在 Set 里，两个构造子都携带运行时可区分的信息，因此分支保留。

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 内部的核心指令（8.20 原文）：*)
Extract Inductive nat => int [ "0" "Stdlib.Int.succ" ]
  "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

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

这个文件还顺带映射了一批运算，不只是类型：Extract Constant plus => "(+)"、Extract Constant mult => "( * )"、Extract Constant pred => "fun n -> Stdlib.max 0 (n-1)"、Extract Inlined Constant Nat.eqb => "(=)" 等等。所以用了它之后不需要再手写一遍这些运算的映射。

它的文件头还有一段免责声明值得留意：「trying to obtain efficient certified programs by extracting nat into int is definitively not a good idea」——int 有界而 nat 无界，溢出的责任完全在使用者。标准库给的建议是，真要在提取产物里做数值运算，用 Coq 自己的高效表示（positive、Z、N、BigN、BigZ），或者走模块化/公理化的表示。

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

文件	作用
ExtrOcamlBasic	bool、option、list、pair 映射到 OCaml 内置
ExtrOcamlNatInt	nat → int
ExtrOcamlZInt	Z → int
ExtrOcamlString	string → OCaml char list（不是原生 string）
ExtrOcamlNativeString	string → OCaml 原生 string，性能与 FFI 场景选它
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

这里的默认值和直觉相反：Extraction AutoInline 默认是关的。即使关着，recursor（nat_rect 这类 _rect / _rec scheme）、projection、andb / orb（为保持惰性）、良基递归组合子这几类仍然无条件内联。想要启发式地内联小函数得显式 Set Extraction AutoInline.，而想精确控制某几个常量则用下面的 Extraction Inline。

(* 强制内联：提取时将 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.

(* 归并两个有序列表。
   注意这里为什么不能写成朴素的双参数递归：
     h1 :: merge t1 l2   —— l1 减小、l2 不变
     h2 :: merge l1 t2   —— l1 不变、l2 减小
   两个递归调用没有共同的结构递减参数，而 Coq 的 guard checker
   只接受单一递减参数，会报 Cannot guess decreasing argument of fix.
   标准库 Sorting/Mergesort.v 的解法是嵌套 fix：外层对 l1 递减，
   内层 merge_aux 对 l2 递减。 *)
Fixpoint merge (l1 l2 : list nat) : list nat :=
  let fix merge_aux l2 :=
    match l1, l2 with
    | [], _  => l2
    | _, []  => l1
    | h1 :: t1, h2 :: t2 =>
        if Nat.leb h1 h2
        then h1 :: merge t1 l2
        else h2 :: merge_aux t2
    end
  in merge_aux l2.

(* 按长度分割列表 *)
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.

Coq 是严格顺序处理的，所以终止性引理必须写在 Program Fixpoint 之前——Next Obligation 里引用一个还没定义的引理会直接报 The reference split_list_length was not found in the current environment.。

终止性引理

split_list 的两个分片长度均严格小于原列表（当原列表长度 ≥ 2 时），这是 Program Fixpoint 终止证明所需的。证明要对列表做两步归纳，而标准库没有现成的双步归纳原理，得自己给一个：

Require Import Lia.

(* 标准库里没有 list_ind2，先自己定义 *)
Lemma list_ind2 : forall (A : Type) (P : list A -> Prop),
  P [] ->
  (forall a, P [a]) ->
  (forall a b l, P l -> P (a :: b :: l)) ->
  forall l, P l.
Proof.
  intros A P H0 H1 H2.
  fix IH 1.
  intros [|a [|b l]]; auto.
Qed.

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.
  intros A l. induction l as [| a | a b t IH] using list_ind2.
  - intros. simpl in *. inversion H. subst. simpl in H0. lia.
  - intros. simpl in *. inversion H. subst. simpl in H0. lia.
  - 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]. lia.
    + destruct t as [|c [|d rest]]; simpl in *; try lia.
      all: inversion Ht; subst; simpl; lia.
Qed.

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

归并排序本体

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 lia.
  destruct (split_list t) eqn:Hsplit. simpl.
  pose proof (split_list_length _ t l1 l2 Hsplit). lia.
Defined.
Next Obligation.
  destruct l as [|a [|b t]]; simpl in *; try lia.
  destruct (split_list t) eqn:Hsplit. simpl.
  pose proof (split_list_length _ t l1 l2 Hsplit). lia.
Defined.

提取指令

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

(* Program Fixpoint 会经良基递归组合子脱糖，不内联这两个的话，
   产物里会带一层 Fix_sub / proj1_sig / Acc 脚手架和 mergesort_func 之类的辅助名 *)
Extraction Inline Wf.Fix_sub Wf.Fix_F_sub.

Extraction "mergesort.ml" mergesort merge split_list.

生成的 OCaml 代码

这里要提醒一句：别照抄任何「手写风格」的提取产物。提取器的输出有几个固定特征，跟人写的不一样：

• 它不生成 match l1, l2 with 这种元组匹配，而是输出嵌套的 match；
• Program Fixpoint 的产物即使加了上面的 Extraction Inline，命名和结构仍与源码有距离；
• let (l1, l2) = ... 这种写法依赖 ExtrOcamlBasic 把 prod 映到 OCaml 元组。

所以正确的做法是自己跑一遍 coqc 看真实输出，而不是照着预期写一份。

coqc mergesort.v          # 会在当前目录生成 mergesort.ml 和 mergesort.mli
head -40 mergesort.ml     # 看真实产物长什么样

编译与运行

Extraction "mergesort.ml" 会同时生成 mergesort.mli。有接口文件在场时，直接往 .ml 末尾追加 let () = ... 入口是编译不过的——入口不在接口里暴露，签名不匹配。把测试入口放进单独的文件：

cat > main.ml << 'EOF'
let () =
  let result = Mergesort.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 mergesort.mli mergesort.ml main.ml -o mergesort

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

（别加 2>/dev/null——初学者最需要看到的恰恰是被它吞掉的那些编译错误。）

性能陷阱

一元 nat 的代价

未做任何映射时，nat 的提取形式是链表结构。Nat.add 1000 1000 在 OCaml 中需要做 1000 次 S 构造。Nat.mul 100 100 的复杂度是 O(n²)。

但要注意 Extract Inductive 只换表示，不换算法。refman 对此有明确告警：把 nat 提取成 OCaml int 之后，Nat.mul 仍然是平方级。映射换掉的是类型，那个乘法函数的实现没动。要真正拿到常数级乘法，必须同时用 Extract Constant 把 Nat.add、Nat.mul 等映到原生运算——ExtrOcamlNatInt 之所以有用，正是因为它两件事都做了。

数值表示的选型大致是这样一条阶梯：nat（教学用，别上生产）→ N / Z（Coq 内部的二进制表示，本身就高效）→ ExtrOcamlZBigInt（映到 Zarith，提取后无溢出）→ Int63（有界但快，8.20 有 ExtrOCamlInt63）。ExtrOcamlZInt 把 positive、N、Z 三个类型都映到 int，快但会溢出，责任在使用者。

失败路径：

(* 未加任何映射指令，直接提取 *)
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 中，这一段过不了类型检查 *)
Fail Definition bad_choice (A B : Prop) (H : A \/ B) : nat :=
  match H with
  | or_introl _ => 0
  | or_intror _ => 1
  end.
(* Incorrect elimination of "H" in the inductive type "or":
   the return type has sort "Set" while it should be SProp or Prop.
   Elimination of an inductive object of sort Prop
   is not allowed on a predicate in sort Set
   because proofs can be eliminated only to build proofs. *)

关键在于这段代码根本走不到提取那一步——kernel 在类型检查阶段就拒绝了。or 有两个构造子，不满足 singleton elimination 的条件，所以不能被消去到 Set。

这个区分很容易记反成「提取器自动选了第一个分支」。没有这回事：Prop 上的非 singleton 消去是编译期错误，不是运行期行为。同一条报错在第 13 篇的诊断清单里也该有一席。

修复：改用 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 和 sigT 也是在提取场景下携带计算分支的常用类型。

sig 要单独说：它恰恰不在这个列表里。sig 是 singleton（唯一的构造子 exist，第二个参数在 Prop），提取时整个归纳结构被折叠掉，只剩内层类型的别名——一个「分支」都不留。refman 讲 Extraction KeepSingleton 这个 flag 时点的典型例子就是 sig。前面 {n : nat | n > 0} 提取成 nat 用的正是这条规则；想关掉它做对照实验就 Set Extraction KeepSingleton.（默认是关的，也就是默认会折叠）。

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 8.20.0 Reference Manual，Extraction of programs in OCaml and Haskell：https://rocq-prover.org/doc/V8.20.0/refman/addendum/extraction.html
• Pierre Letouzey. A New Extraction for Coq. TYPES 2002.
• Xavier Leroy et al. CompCert C Compiler：Coq 提取到 OCaml 的最大规模工程案例
• 本系列《深入 Coq 01：开发环境与项目结构》、《深入 Coq 03：Gallina 核心语法速查》、《深入 Coq 09：归纳证明》提供 Extraction 所需前置知识
• 本篇技术的实战落地见《深入 Coq 15：验证一个小型解释器》