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'.
And after extracting the Haskell code, I wrote a simple driver to test it. I ran into two issues:
Bool
instead of using Haskell's built in boolean type.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.
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.