Coqでどう書く? 関数型プログラム

Start and Quit

Coq Ocaml

yoshihiro$ coqtop
Welcome to Coq 8.1 (Feb. 2007)

Coq < 

yoshihiro$ ocaml
        Objective Caml version 3.09.3

# 

Coq < Quit.
yoshihiro$

# #quit;;
yoshihiro$

Compile

Coq Ocaml
yoshihiro$ coqc file1.v file2.v yoshihiro$ ocamlc file1.ml file2.ml
or
yoshihiro$ ocamlopt file1.ml file2.ml

Comments

Coq Ocaml

(* コメント *)
(*
    複数行のコメント
    (*入れ子*)
*)
(**
    coqdocで出力される項目
*)

(* コメント *)
(*
    複数行のコメント
    (*入れ子*)
*)
(**
    ocamldocで出力される項目
**)

Literals

Coq Ocaml

Coq < Check 3.
3
     : nat
# 3;;
- : int = 3

Coq < Require Import String.
Coq < Open Scope string_scope.
Coq < Check "Hello world".
"Hello world"
     : string
# "Hello world";;
- : string = "Hello world"

Coq < Require Import Ascii.
Coq < Open Scope char_scope.
Coq < Check "J".
"J"
     : ascii
# 'J';;
- : char = 'J'

Coq < Check true.
true
     : bool
# true;;
- : bool = true

Coq < Check tt.
tt
     : unit
# ();;
- : unit = ()

Coq < Check (3, true, "hi").
(3%nat, true, "hi")
     : nat * bool * string
# (3,true,"hi");;
- : int * bool * string = 3, true, "hi"

Coq < Require Import List.
Coq < Check 1::2::3::nil.
1 :: 2 :: 3 :: nil
     : list nat
# [1;2;3];;
- : int list = [1; 2; 3]
ない # [|1;2;3|];;
- : int array = [|1; 2; 3|]

Functions

Coq Ocaml
fun x => f (g x)
fun x -> f (g x)

Value Declarations

SML Ocaml
Definition name := expr.
let name = expr
Variables A B : Set.
Definition f (x:A) (y:B) := expr.
or
Definition f := fun (x:A) (y:B) => expr.
let f x y = expr
or
let f = fun x y -> expr
?ltb?
Fixpoint fib n {struct n} :=
   if LTB n 2
   then n
   else fib(n-1) + fib(n-2).
or
Definition fib := fix f (n:nat) :=
   if LTB n 2
   then n
   else f(n-1) + f(n-2).
let rec fib n =
   if n < 2
   then n
   else fib(n-1) + fib(n-2)
or
let rec fib = fun n ->
   if n < 2
   then n
   else fib(n-1) + fib(n-2)

Type Declarations

Coq Ocaml
Definition t := (Z -> bool).
type t = (int -> bool)
Require Import List.
Definition assoc_list a b := list (a * b).
type ('a,'b) assoc_list = ('a * 'b) list
Inductive option (a:Set) : Set :=
  | None : option a
  | Some : a -> option a.
type 'a option =
    None
  | Some of 'a

Matching

Coq Ocaml
Variable A:Set.
Definition get_opt (opt:option A) d :=
   match opt with
        None => d
      | Some x => x
 end.
let get_opt (opt, d) =
   match opt with
        None -> d
      | Some x -> x
Require Import List.
Fixpoint take n xs {struct n} :=
  xs<>nil ->
   match n, xs with
    O, xs => nil
  | S m, (x::xs) => x :: take m xs
  end.

let rec take n xs =
   match n, xs with
        0, xs -> []
      | n, [] -> failwith "take"
      | n, x::xs -> x :: take (n-1) xs

Tuples

Coq Ocaml

Require Import ZArith.
Require Import QArith.
Require Import string.
Open Scope type_scope.
Definition foo := Z * Q *  string 
type foo = int * float * string

Definition bar :=
  (0%Z, (314#100)%Q, "hi"%string) 


let bar = 0, 3.14, "hi"
or
let bar = (0, 3.14, "hi")
Check(snd (fst bar))



match bar with _,x,_ -> x
or
let _,x,_ = bar in x