感谢Pierce 教授的 2012 年夏季视频 4.1，正如Dan Feltey 所建议的那样，我们看到关键是要提取的定理必须提供一个成员Type而不是通常的命题类型，即Prop.
对于特定定理，受影响的构造是归纳 Propex及其符号exists。与 Pierce 教授所做的类似，我们可以陈述我们自己的替代定义，ex_t并将exists_t出现的 替换为Prop的出现Type。
这是通常的重新定义，ex并且与existsCoq 标准库中的定义类似。
Inductive ex (X:Type) (P : X->Prop) : Prop :=
ex_intro : forall (witness:X), P witness -> ex X P.
Notation "'exists' x : X , p" := (ex _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
以下是替代定义。
Inductive ex_t (X:Type) (P : X->Type) : Type :=
ex_t_intro : forall (witness:X), P witness -> ex_t X P.
Notation "'exists_t' x : X , p" := (ex_t _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
现在，有点不幸的是，有必要使用这些新定义重复定理的陈述和证明。
世间有什么？？
为什么有必要对定理进行重复陈述和对定理的重复证明，仅通过使用量词的替代定义而有所不同？
我曾希望在 中使用现有Prop的定理再次证明该定理Type。当 Coq在环境中拒绝inversiona的证明策略时，该策略失败了，而目标是 a that uses 。Coq 报告“错误：反转将需要对排序集进行案例分析，这在归纳定义中是不允许的。” 这种行为发生在 Coq 8.3 中。我不确定它是否仍然出现在 Coq 8.4 中。PropPropexistsTypeexists_t
我认为重复证明的需要实际上是深刻的，尽管我怀疑我个人是否能够很好地理解它的深刻性。它涉及的事实Prop是“隐含的”，Type不是隐含的，而是默认的“分层”的。预测性是（如果我理解正确的话）对罗素悖论的脆弱性，即不是自身成员的集合 S 既不能是 S 的成员，也不能是 S 的非成员。Type通过默认创建包含低级类型的高级类型序列来避免罗素的悖论。因为 Coq 浸透在 Curry-Howard 对应的公式即类型解释中，如果我理解正确，我们甚至可以将 Coq 中的类型分层理解为避免哥德尔不完备性的一种方式，即某些公式表达的现象对诸如它们本身的公式的约束，因此对于它们的真假变得不可知。
回到地球上，这里是使用“exists_t”的定理的重复陈述。
Theorem divalg_t : forall n m : nat, exists_t q : nat,
exists_t r : nat, n = plus (mult q m) r.
由于我省略了 的证明divalg，我也将省略 的证明divalg_t。我只想提一下，我们确实很幸运，包括“exists”和“inversion”在内的证明策略与我们的新定义“ex_t”和“exists_t”一样有效。
最后，提取本身很容易完成。
Extraction Language Haskell.
Extraction "divalg.hs" divalg_t.
生成的 Haskell 文件包含许多定义，其核心是下面相当不错的代码。我对 Haskell 编程语言几乎完全一无所知，这让我有点受不了。请注意，这Ex_t_intro会创建一个类型为Ex_t;的结果。O并且S是Peano算术的零和后继函数；beq_nat测试Peano数是否相等；nat_rec是一个高阶函数，在其参数中递归函数。的定义在nat_rec这里没有显示。无论如何，它是由 Coq 根据 Coq 中定义的归纳类型“nat”生成的。
divalg :: Nat -> Nat -> Ex_t Nat (Ex_t Nat ())
divalg n m =
case m of {
O -> Ex_t_intro O (Ex_t_intro n __);
S m' ->
nat_rec (Ex_t_intro O (Ex_t_intro O __)) (\n' iHn' ->
case iHn' of {
Ex_t_intro q' hq' ->
case hq' of {
Ex_t_intro r' _ ->
let {k = beq_nat r' m'} in
case k of {
True -> Ex_t_intro (S q') (Ex_t_intro O __);
False -> Ex_t_intro q' (Ex_t_intro (S r') __)}}}) n}
2013-04-24 更新：我现在了解更多 Haskell。为了帮助其他人阅读上面提取的代码，我提供了以下手写代码，我声称它们是等效的并且更具可读性。我还展示了我没有删除的提取定义 Nat、O、S 和 nat_rec。
-- Extracted: Natural numbers (non-negative integers)
-- in the manner in which Peano defined them.
data Nat =
O
| S Nat
deriving (Eq, Show)
-- Extracted: General recursion over natural numbers,
-- an interpretation of Nat in the manner of higher-order abstract syntax.
nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
nat_rec f f0 n =
case n of {
O -> f;
S n0 -> f0 n0 (nat_rec f f0 n0)}
-- Given non-negative integers n and m, produce (q, r) with n = q * m + r.
divalg_t :: Nat -> Nat -> (Nat, Nat)
divalg_t n O = (O, n) -- n/0: Define quotient 0, remainder n.
divalg_t n (S m') = divpos n m' -- n/(S m')
where
-- Given non-negative integers n and m',
-- and defining m = m' + 1,
-- produce (q, r) with n = q * m + r
-- so that q = floor (n / m) and r = n % m.
divpos :: Nat -> Nat -> (Nat, Nat)
divpos n m' = nat_rec (O, O) (incrDivMod m') n
-- Given a non-negative integer m' and
-- a pair of non-negative integers (q', r') with r <= m',
-- and defining m = m' + 1,
-- produce (q, r) with q*m + r = q'*m + r' + 1 and r <= m'.
incrDivMod :: Nat -> Nat -> (Nat, Nat) -> (Nat, Nat)
incrDivMod m' _ (q', r')
| r' == m' = (S q', O)
| otherwise = (q', S r')