谢谢Pierce教授2012年夏季视频4.1 http://www.cs.uoregon.edu/Research/summerschool/summer12/curriculum.html as 丹·费尔蒂 https://stackoverflow.com/users/1447178/dan-feltey建议，我们看到关键是要提取的定理必须提供一个成员Type而不是通常的命题，即Prop.
对于特定定理，受影响的构造是归纳 Propex及其符号exists。与皮尔斯教授所做的类似，我们可以陈述我们自己的替代定义ex_t and exists_t替换出现的Prop与出现Type.
这是通常的重新定义ex and exists与 Coq 标准库中的定义类似。
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 拒绝证明策略时，该策略失败inversion for a Prop当那个环境中Prop uses exists目标是Type使用exists_t。 Coq 报告“错误：反转需要对排序集进行案例分析，这是不允许的
对于归纳定义例如。”这种行为发生在 Coq 8.3 中。我不确定它是否是这样
在 Coq 8.4 中仍然出现。
我认为重复证明的必要性实际上是深刻的，尽管我怀疑我个人是否能够理解其深刻性。它涉及以下事实：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。我只会提到，我们确实很幸运，包括“存在”和“反演”在内的证明策略与我们的新定义“ex_t”和“exists_t”的工作原理相同。
最后，提取本身很容易完成。
Extraction Language Haskell.
Extraction "divalg.hs" divalg_t.
生成的 Haskell 文件包含许多定义，其核心是下面相当不错的代码。我对 Haskell 编程语言几乎完全无知，这只是稍微妨碍了我。注意Ex_t_intro创建一个类型为的结果Ex_t; O and S是皮亚诺算术中的零和后继函数；beq_nat测试皮亚诺数是否相等；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')
