forall n m : nat, exists q : nat, exists r : nat, n = q * m + rm和n中构造适当的值q和r的方法。Fixpoint编写并提取了出来。我要小心地指出，这个任务不是我在这里考虑的。是否可能将我证明中的隐含算法提取到Haskell？如果可能，该如何操作？
Type的成员而不是通常类型的命题，即Prop。ex及其符号exists。与Pierce教授所做的类似，我们可以声明自己的替代定义ex_t和exists_t，将Prop的出现替换为Type的出现。ex和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对环境中使用exists的Prop和目标为使用exists_t的Type时拒绝证明策略inversion时，这个策略失败了。Coq报告“错误：反演需要对排序Set进行情况分析，而对于归纳定义ex，这是不允许的。”这种行为在Coq 8.3中发生过。我不确定它是否仍然存在于Coq 8.4中。
我认为需要重复证明实际上是深奥的，尽管我个人怀疑自己是否能够感知其深奥性。它涉及事实，即Prop是“非谓词化的”，而Type不是非谓词化的，而是含蓄地“分层”的。如果我理解正确，谓词性是面对罗素悖论（S是那些不是它们本身成员的集合，既不能是S的成员，也不能是S的非成员）的脆弱性。Type通过含蓄地创建包含较低类型的一系列更高类型来避免Russell's paradox。由于Coq浸润在Curry-Howard对应的公式即类型解释中，如果我理解正确，我们甚至可以将Coq中的类型分层理解为避免Gödel不完全性的一种方式，即某些公式会表达对自身或其他公式等约束条件，从而无法知道它们的真假。
回到地球上，这里是使用"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和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年4月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')
sigT 可用。你可以在这个地址找到所有这个对的变体（因为在构造逻辑中，“存在一个 X 使得 P”只是一个 X 和证明 P 的见证，可能依赖于 X）。 - Vinzdivalg和divalg_t？我认为这会非常有用。 - OrenIshShalom2012年7月25日的《软件基础》副本，在后期章节“Extraction2”中简明地回答了这个问题。答案是可以做到的，就像这样：
Extraction Language Haskell
Extraction "divalg.hs" divalg
Type，而不是Prop。否则，在提取的过程中它将被删除。Type而不是Prop），这些命题是divalg依赖的。对于一个彻底、有趣且可行的证明提取示例，可以查看上面提到的Extraction2章节。该示例提取到OCaml，但将其适应于Haskell只需使用如上所述的Extraction Language Haskell。
0 <= r < m... - Alexey0 <= r存在于r是类型nat的成员。2 但是，是的，糟糕的是，缺少条件r < m。因此，更有效的 Haskell 函数是divalg n m = Ex_t_intro O (Ex_t_intro n __)。3 然而，我从另一个证明中提取了 Coq 提取 Haskell 代码，而不是将 q 设置为零并将 r 设置为 n 的证明。因此，给定两个Nat参数，我的答案中的 Haskell（我声称）满足r < m的条件，其中r是结果中的第二个Nat，而m是参数中的第二个Nat。 - minopret