我可以提取Coq证明作为Haskell函数吗？ [英] Can I extract a Coq proof as a Haskell function?

问题描述

• 自从我学到一点Coq之后，我就想学习写所谓的除法算法的Coq证明，这实际上是一个逻辑命题： forall nm ：nat，存在q：nat，存在r：nat，n = q * m + r


• 我最近利用从软件基础。


• Coq是用于开发建设性证明，我的证明实际上是一种从值<$ c $构造合适的值 q 和 r 的方法c> m 和 n 。


• Coq具有吸引人的功能，可以提取 Coq的算法算法语言（Gallina）转换为通用函数式编程语言，包括Haskell。


• 我分别设法将divmod操作编写为Gallina Fixpoint 并将其提取。我想仔细注意一下，该任务不是我在这里考虑的。


• Adam Chlipala用依赖类型的认证编程，许多Curry-Howard函式的支持者都支持从证明中提取程序的想法。实际上，很少有Coq和相关工具的用户这样做。

• Ever since I learned a little bit of Coq I wanted to learn to write a Coq proof of the so-called division algorithm that is actually a logical proposition: forall n m : nat, exists q : nat, exists r : nat, n = q * m + r
• I recently accomplished that task using what I learned from Software Foundations.
• Coq being a system for developing constructive proofs, my proof is in effect a method to construct suitable values q and r from values m and n.
• Coq has an intriguing facility for "extracting" an algorithm in Coq's algorithm language (Gallina) to general-purpose functional programming languages including Haskell.
• Separately I have managed to write the divmod operation as a Gallina Fixpoint and extract that. I want to note carefully that that task is not what I'm considering here.
• Adam Chlipala has written in Certified Programming with Dependent Types that "Many fans of the Curry-Howard correspondence support the idea of extracting programs from proofs. In reality, few users of Coq and related tools do any such thing."

是否有可能提取我对Haskell的证明中隐含的算法？

Is it even possible to extract the algorithm implicit in my proof to Haskell? If it is possible, how would it be done?

推荐答案

感谢教授。 Pierce在2012年夏季发布的视频4.1 作为 Dan Feltey 建议，我们看到关键是定理提取必须提供 Type 的成员，而不是通常的命题 Prop 。

Thanks to Prof. Pierce's summer 2012 video 4.1 as Dan Feltey suggested, we see that the key is that the theorem to be extracted must provide a member of Type rather than the usual kind of propositions, which is Prop.

对于特定定理，受影响的构造是归纳式Prop ex 及其符号存在。与Pierce教授所做的类似，我们可以陈述自己的替代定义 ex_t 和 exists_t 来替换道具出现类型。

For the particular theorem the affected construct is the inductive Prop ex and its notation exists. Similarly to what Prof. Pierce has done, we can state our own alternate definitions ex_t and exists_t that replace occurrences of Prop with occurrences of Type.

重新定义 ex 和 的定义与在Coq标准库中定义的类似。

Here is the usual redefinition of ex and exists similarly as they are defined in Coq's standard library.

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.

现在，不幸的是，有必要同时重复陈述和证明

Now, somewhat unfortunately, it is necessary to repeat both the statement and the proof of the theorem using these new definitions.

世界到底是什么？

为什么有必要对定理进行反复陈述和对定理进行反复证明，仅通过使用量词的替代定义而有所区别？

What in the world??

Why is it necessary to make a reiterated statement of the theorem and a reiterated proof of the theorem, that differ only by using an alternative definition of the quantifier??

我希望使用 Prop 中的现有定理来再次证明定理在 Type 。当Coq拒绝环境中 Prop 的证明策略反转时，该策略失败，道具使用存在，目标是使用的类型存在_t 。 Coq报告错误：反转需要对排序集进行案例分析，而归纳定义ex不允许
。此行为发生在Coq 8.3中。我不确定在Coq 8.4中是否仍会出现
。

I had hoped to use the existing theorem in Prop to prove the theorem over again in Type. That strategy fails when Coq rejects the proof tactic inversion for a Prop in the environment when that Prop uses exists and the goal is a Type that uses exists_t. Coq reports "Error: Inversion would require case analysis on sort Set which is not allowed for inductive definition ex." This behavior occurred in Coq 8.3. I am not certain that it still occurs in Coq 8.4.

我认为重复证明的必要性实际上是深远的，尽管我怀疑我个人相当设法感觉到它的深刻性。它涉及到以下事实： Prop 是强制性的，而 Type 不是强制性的，而是默认的分层的。谓词性是（如果我理解正确的话）对罗素悖论的脆弱性，即不是自身成员的集合的集合S既不能成为S的成员，也不能成为S的非成员。 Type 通过默认创建包含较低类型的较高类型的序列来避免罗素悖论。因为Coq充斥在Curry-Howard对应关系的公式即类型解释中，如果我正确理解这一点，我们甚至可以理解Coq中的类型分层是避免Gödel不完整（一种某些公式所表达的现象）的方式对诸如它们自己的公式的约束，从而使他们对它们的真实性或虚假性变得不可知。

I think the need to repeat the proof is actually profound although I doubt that I personally am quite managing to perceive its profundity. It involves the facts that Prop is "impredicative" and Type is not impredicative, but rather, tacitly "stratified". Predicativity is (if I understand correctly) vulnerability to Russell's paradox that the set S of sets that are not members of themselves can neither be a member of S, nor a non-member of S. Type avoids Russell's paradox by tacitly creating a sequence of higher types that contain lower types. Because Coq is drenched in the formulae-as-types interpretation of the Curry-Howard correspondence, and if I am getting this right, we can even understand stratification of types in Coq as a way to avoid Gödel incompleteness, the phenomenon that certain formulae express constraints on formulae such as themselves and thereby become unknowable as to their truth or falsehood.

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的作用相同。

As I have omitted the proof of divalg, I will also omit the proof of divalg_t. I will only mention that we do have the good fortune that proof tactics including "exists" and "inversion" work just the same with our new definitions "ex_t" and "exists_t".

最后，提取本身很容易完成。

Finally, the extraction itself is accomplished easily.

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生成的。

The resulting Haskell file contains a number of definitions, the heart of which is the reasonably nice code, below. And I was only slightly hampered by my near-total ignorance of the Haskell programming language. Note that Ex_t_intro creates a result whose type is Ex_t; O and S are the zero and the successor function from Peano arithmetic; beq_nat tests Peano numbers for equality; nat_rec is a higher-order function that recurs over the function among its arguments. The definition of nat_rec is not shown here. At any rate it is generated by Coq according to the inductive type "nat" that was defined in Coq.

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。

Update 2013-04-24: I know a bit more Haskell now. To assist others in reading the extracted code above, I'm presenting the following hand-rewritten code that I claim is equivalent and more readable. I'm also presenting the extracted definitions Nat, O, S, and nat_rec that I did not eliminate.

-- 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')

这篇关于我可以提取Coq证明作为Haskell函数吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！