提取Coq到Haskell [英] Extracting Coq to Haskell

问题描述

我正在试验Coq对Haskell的提取机制。我在Coq中为素数写了一个幼稚的谓词，这里是：

I'm experimenting with Coq's extraction mechanism to Haskell. I wrote a naive predicate for prime numbers in Coq, here it is:

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m,n with
  | 0,_ => false
  | 1,_ => false
  | _,0 => false
  | _,1 => false
  | S m',S n' => (orb ((mult m n) =? p) (helper' p m' n))
  end.

(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
  end.

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

Compute (isPrime 220).

(*****************)
(* isPrimeHelper *)
(*****************)
Extraction Language Haskell.

(*****************)
(* isPrimeHelper *)
(*****************)
Extraction "/home/oren/GIT/CoqIt/Primes.hs" isPrime helper helper'.

提取Haskell代码后，我编写了一个简单的驱动程序对其进行测试。我遇到了两个问题：

And after extracting the Haskell code, I wrote a simple driver to test it. I ran into two issues:

1. Coq导出了自己的 Bool 而不是使用Haskell的


2. Coq还使用了自己的 nat ，所以我不能问 isPrime 6 ，我必须使用 S（S（...））。

1. Coq exported its own Bool instead of using Haskell's built in boolean type.
2. Coq also used its own nat, so I can't ask isPrime 6 and I have to use S (S (...)).

module Main( main ) where    
import Primes    
main = do
    if ((isPrime (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S ( O ))))))))
        ==
        Primes.True)
    then
        print "Prime"
    else
        print "Non Prime"

推荐答案

关于您的第一点-尝试添加

Regarding your first point - try to add

Require Import ExtrHaskellBasic.

您的Coq来源。它指定提取应针对某些基本类型使用Haskell的前奏定义。可以在此处找到文档。 字符串也有一个类似的模块。

to your Coq source. It specifies that the extraction should use Haskell's prelude definitions for some basic types. Documentation can be found here. There is also a similar module for strings.

这篇关于提取Coq到Haskell的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！