时间戳

首页 > 解决方案 > 将 Coq 提取到 Haskell

haskell - 将 Coq 提取到 Haskell

问题描述

我正在试验 Coq 对 Haskell 的提取机制。我在 Coq 中为素数写了一个简单的谓词，它是：

(***********)
(* 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 代码后，我编写了一个简单的驱动程序来测试它。我遇到了两个问题：

  1. Coq 导出它自己的Bool而不是使用 Haskell 的内置布尔类型。
  2. Coq 也使用了它自己的nat，所以我不能问isPrime 6，我必须使用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"

标签： haskellcoq

解决方案

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

Require Import ExtrHaskellBasic.

到你的 Coq 源。它指定提取应该使用 Haskell 的一些基本类型的前奏定义。文档可以在这里找到。字符串也有一个类似的模块。

推荐阅读