我可以将Coq证明提取为Haskell函数吗？

Question

• 自从我学会了一点Coq后,我想学习写一个所谓的除法算法的Coq证明,这实际上是一个逻辑命题: forall n m : nat, exists q : nat, exists r : nat, n = q * m + r
• 我最近使用从Software Foundations中学到的东西完成了这项任务.
• Coq是一个用于开发建设性证明的系统,我的证明实际上是一种构造合适的值的方法,q并且是r从值m和n.
• Coq有一个有趣的工具,用于将Coq的算法语言(Gallina)中的算法"提取"到包括Haskell在内的通用函数编程语言.
• 另外,我已经设法将divmod操作编写为Gallina Fixpoint并将其提取出来.我想仔细注意那个任务不是我在这里考虑的.
• 亚当Chlipala写在与相关类型认证的编程说,"柯里-霍华德同构的很多球迷支持从样张中提取节目的想法.在现实中,勒柯克的少数用户和相关的工具做任何这样的事情."

甚至可以将我的证明中隐含的算法提取到Haskell中吗？如果有可能,怎么办呢？

Answer 1

感谢Pierce教授的2012年夏季视频4.1,正如Dan Feltey所建议的那样,我们看到关键是被提取的定理必须提供一个成员Type而不是通常的命题,即Prop.

对于特定定理,受影响的构造是归纳Prop ex及其符号exists.与皮尔斯教授所做的类似,我们可以陈述我们自己的替代定义,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.当勒柯克拒绝证明战术,战略失败inversion的Prop环境中时Prop使用exists,并且目标是一个Type使用exists_t.Coq报告"错误:反转将需要对排序集进行案例分析,这对于归纳定义ex不允许." 此行为发生在Coq 8.3中.我不确定它是否仍然出现在Coq 8.4中.

我认为重复证据的必要性实际上是深刻的,尽管我怀疑我个人是否能够完全理解它的深刻性.它涉及的事实Prop是"不可预测的",Type并不是不可预测的,而是默认的"分层".预测性(如果我理解正确的话)易受拉塞尔悖论的影响,即不属于自身成员的集合S既不是S的成员,也不是S的非成员.Type通过默默地创建包含较低类型的更高类型的序列来避免Russell的悖论.因为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并且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')