トップ
新規
単語検索
ヘルプ
ネタ記録庫/Coq
をテンプレートにして作成
開始行:
[[ネタ記録庫/Coq]]
#br
Agdaはこちら -> ネタ記録庫/Agda
#contents
* 日本語のCoq入門資料 (by [[Asai Laboratory:http://pllab....
[[Coqゼミ:http://pllab.is.ocha.ac.jp/lab.html]]
- 第 1 回 Coq のインストール,関数,大域的変数, Specific...
- 第 2 回 命題論理
- 第 3 回 関数の拡張,述語論理
- 第 4 回 implication (ならば,→) 以外の論理演算, 等式の...
- 第 5 回 帰納的なデータ型 (再帰を含まないもの/含むもの) ,
再帰関数の定義, 帰納法
- 第 6 回 リスト,帰納的な命題の定義
- 第 7 回 演習
- 第 8 回 演習(続き)
* 超演繹のための定理証明支援器 [#c4f59bc5]
http://rho.loria.fr/lemuridae.html
* Coqでニコニコ :-] [#uc59f799]
http://www.nicovideo.jp/watch/sm1276083 from [[にわとり小...
(youtube : http://jp.youtube.com/watch?v=f9XOdpmeJ0o )
- Javascriptでニコニコも :-] http://www.nicovideo.jp/watc...
* 本山とりとり亭でのCoq談義に捧ぐ。(07/10/15) [#o7920891]
http://f.hatena.ne.jp/images/fotolife/G/Gemma/20071015/20...
- [[名古屋(2) - ヒビルテ:http://www.tom.sfc.keio.ac.jp/~s...
- [[飲み会 - zyxwvの日記:http://d.hatena.ne.jp/zyxwv/2007...
- [[飲み会 - すえひろがりっっっ!:http://kamakiri.ddo.jp/n...
* Coqに関する発表をしました(2007/9/20 よしひろ) [#dfaea...
[[論理と証明 - 安全なWebアプリケーションのために:http://w...
*Proofs and Types [#z5683f1d]
Jean-Yves Girard, Yves Lafont and Paul Taylor
- http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
定理証明器ネタのページがそろそろ必要か。
*reddit.comから [#d5676edd]
こんなのがありました。
http://as305.dyndns.org/wiki/index.php?Coq%2Ftactics
* 定理証明器 Coq でHello, world! (よしひろ)[#pc6c3278]
Coqで "Hello, world!" を標準出力させるのはちょっと難しい。~
なぜなら純粋だから。~
今回は29行ほどのOCamlの力を借りて実装した。~
具体的には次の三つのファイルを作った。~
-coqstring.v
-helloworld.v
-main.ml (29行のOCamlコード)
ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリス...
(*Coqのスタンダードライブラリより*)
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Inductive string : Set :=
| EmptyString : string
| String : ascii -> string -> string.
まずcoqstring.v~
Coqの文字列に関する便利のものたちを定義した。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Definition aH := Ascii false false false true false fal...
Definition ae := Ascii true false true false false tr...
Definition al := Ascii false false true true false tr...
Definition ao := Ascii true true true true false tru...
Definition aCMM := Ascii false false true true false t...
Definition aSPC := Ascii false false false false false ...
Definition aw := Ascii true true true false true tr...
Definition ar := Ascii false true false false true tr...
Definition ad := Ascii false false true false false tr...
Definition aEXCLAM := Ascii true false false false fal...
Definition aLF := Ascii false true false true false f...
次にhelloworld.v~
このソースがこのプログラムの本質部分。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Require Import coqstring.
Definition msg :=
String aH
(String ae
(String al
(String al
(String ao
(String aCMM
(String aSPC
(String aw
(String ao
(String ar
(String al
(String ad
(String aEXCLAM
(String aLF EmptyString))))))))))))).
Extraction "coqhelloworld.ml" nat_of_ascii msg.
以上のコードをコンパイルした結果、自動生成されるOCamlのコ...
(* これは上にあるCoqのコードから自動的に生成されたOCaml...
type bool =
| True
| False
type nat =
| O
| S of nat
(** val plus : nat -> nat -> nat **)
let rec plus n m =
match n with
| O -> m
| S p -> S (plus p m)
(** val mult : nat -> nat -> nat **)
let rec mult n m =
match n with
| O -> O
| S p -> plus m (mult p m)
type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bo...
(** val nat_of_ascii : ascii -> nat **)
let nat_of_ascii = function
| Ascii (a1, a2, a3, a4, a5, a6, a7, a8) ->
plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(match a8 with
| True -> S O
| False -> O))
(match a7 with
| True -> S O
| False -> O)))
(match a6 with
| True -> S O
| False -> O)))
(match a5 with
| True -> S O
| False -> O)))
(match a4 with
| True -> S O
| False -> O)))
(match a3 with
| True -> S O
| False -> O)))
(match a2 with
| True -> S O
| False -> O))) (match a1 with
| True -> S O
| False -> O)
type string =
| EmptyString
| String of ascii * string
(** val aH : ascii **)
let aH =
Ascii (False, False, False, True, False, False, True, F...
(** val ae : ascii **)
let ae =
Ascii (True, False, True, False, False, True, True, Fal...
(** val al : ascii **)
let al =
Ascii (False, False, True, True, False, True, True, Fal...
(** val ao : ascii **)
let ao =
Ascii (True, True, True, True, False, True, True, False)
(** val aCMM : ascii **)
let aCMM =
Ascii (False, False, True, True, False, True, False, Fa...
(** val aSPC : ascii **)
let aSPC =
Ascii (False, False, False, False, False, True, False, ...
(** val aw : ascii **)
let aw =
Ascii (True, True, True, False, True, True, True, False)
(** val ar : ascii **)
let ar =
Ascii (False, True, False, False, True, True, True, Fal...
(** val ad : ascii **)
let ad =
Ascii (False, False, True, False, False, True, True, Fa...
(** val aEXCLAM : ascii **)
let aEXCLAM =
Ascii (True, False, False, False, False, True, False, F...
(** val aLF : ascii **)
let aLF =
Ascii (False, True, False, True, False, False, False, F...
(** val msg : string **)
let msg =
String (aH, (String (ae, (String (al, (String (al, (Str...
(aCMM, (String (aSPC, (String (aw, (String (ao, (Stri...
(String (ad, (String (aEXCLAM, (String (aLF,
EmptyString)))))))))))))))))))))))))))
最後に以上をまとめて結果を出すOCamlのコードmain.ml。~
この部分だけは証明することができない。
(* OCamlのコード *)
module Coq = Coqhelloworld
let rec int_of_nat = function
| Coq.O -> 0
| Coq.S p -> 1 + (int_of_nat p)
let length coqstr =
let rec length_aux n = function
| Coq.EmptyString -> n
| Coq.String (_, tl) -> length_aux (1+n) tl
in
length_aux 0 coqstr
let char_of_ascii a =
char_of_int (int_of_nat (Coq.nat_of_ascii a))
let string_of_coqstring coqstr =
let n = length coqstr in
let s = String.create n in
let rec aux i = function
| Coq.EmptyString -> ()
| Coq.String (hd, tl) ->
s.[i] <- char_of_ascii hd;
aux (i+1) tl
in
aux 0 coqstr;
s;;
print_string (string_of_coqstring Coq.msg);;
実行結果
Hello, world!
やった!できた!
* Proof are Programs [#fca44cec]
- http://www.radiumsoftware.com/0605.html#060523
- Philip Wadler. [[Proofs are Programs: 19th Century Logi...
- 数理論理学とコンピュータ・プログラムの間には深い関連性...
終了行:
[[ネタ記録庫/Coq]]
#br
Agdaはこちら -> ネタ記録庫/Agda
#contents
* 日本語のCoq入門資料 (by [[Asai Laboratory:http://pllab....
[[Coqゼミ:http://pllab.is.ocha.ac.jp/lab.html]]
- 第 1 回 Coq のインストール,関数,大域的変数, Specific...
- 第 2 回 命題論理
- 第 3 回 関数の拡張,述語論理
- 第 4 回 implication (ならば,→) 以外の論理演算, 等式の...
- 第 5 回 帰納的なデータ型 (再帰を含まないもの/含むもの) ,
再帰関数の定義, 帰納法
- 第 6 回 リスト,帰納的な命題の定義
- 第 7 回 演習
- 第 8 回 演習(続き)
* 超演繹のための定理証明支援器 [#c4f59bc5]
http://rho.loria.fr/lemuridae.html
* Coqでニコニコ :-] [#uc59f799]
http://www.nicovideo.jp/watch/sm1276083 from [[にわとり小...
(youtube : http://jp.youtube.com/watch?v=f9XOdpmeJ0o )
- Javascriptでニコニコも :-] http://www.nicovideo.jp/watc...
* 本山とりとり亭でのCoq談義に捧ぐ。(07/10/15) [#o7920891]
http://f.hatena.ne.jp/images/fotolife/G/Gemma/20071015/20...
- [[名古屋(2) - ヒビルテ:http://www.tom.sfc.keio.ac.jp/~s...
- [[飲み会 - zyxwvの日記:http://d.hatena.ne.jp/zyxwv/2007...
- [[飲み会 - すえひろがりっっっ!:http://kamakiri.ddo.jp/n...
* Coqに関する発表をしました(2007/9/20 よしひろ) [#dfaea...
[[論理と証明 - 安全なWebアプリケーションのために:http://w...
*Proofs and Types [#z5683f1d]
Jean-Yves Girard, Yves Lafont and Paul Taylor
- http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
定理証明器ネタのページがそろそろ必要か。
*reddit.comから [#d5676edd]
こんなのがありました。
http://as305.dyndns.org/wiki/index.php?Coq%2Ftactics
* 定理証明器 Coq でHello, world! (よしひろ)[#pc6c3278]
Coqで "Hello, world!" を標準出力させるのはちょっと難しい。~
なぜなら純粋だから。~
今回は29行ほどのOCamlの力を借りて実装した。~
具体的には次の三つのファイルを作った。~
-coqstring.v
-helloworld.v
-main.ml (29行のOCamlコード)
ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリス...
(*Coqのスタンダードライブラリより*)
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Inductive string : Set :=
| EmptyString : string
| String : ascii -> string -> string.
まずcoqstring.v~
Coqの文字列に関する便利のものたちを定義した。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Definition aH := Ascii false false false true false fal...
Definition ae := Ascii true false true false false tr...
Definition al := Ascii false false true true false tr...
Definition ao := Ascii true true true true false tru...
Definition aCMM := Ascii false false true true false t...
Definition aSPC := Ascii false false false false false ...
Definition aw := Ascii true true true false true tr...
Definition ar := Ascii false true false false true tr...
Definition ad := Ascii false false true false false tr...
Definition aEXCLAM := Ascii true false false false fal...
Definition aLF := Ascii false true false true false f...
次にhelloworld.v~
このソースがこのプログラムの本質部分。
(* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Require Import coqstring.
Definition msg :=
String aH
(String ae
(String al
(String al
(String ao
(String aCMM
(String aSPC
(String aw
(String ao
(String ar
(String al
(String ad
(String aEXCLAM
(String aLF EmptyString))))))))))))).
Extraction "coqhelloworld.ml" nat_of_ascii msg.
以上のコードをコンパイルした結果、自動生成されるOCamlのコ...
(* これは上にあるCoqのコードから自動的に生成されたOCaml...
type bool =
| True
| False
type nat =
| O
| S of nat
(** val plus : nat -> nat -> nat **)
let rec plus n m =
match n with
| O -> m
| S p -> S (plus p m)
(** val mult : nat -> nat -> nat **)
let rec mult n m =
match n with
| O -> O
| S p -> plus m (mult p m)
type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bo...
(** val nat_of_ascii : ascii -> nat **)
let nat_of_ascii = function
| Ascii (a1, a2, a3, a4, a5, a6, a7, a8) ->
plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(plus
(mult (S (S O))
(match a8 with
| True -> S O
| False -> O))
(match a7 with
| True -> S O
| False -> O)))
(match a6 with
| True -> S O
| False -> O)))
(match a5 with
| True -> S O
| False -> O)))
(match a4 with
| True -> S O
| False -> O)))
(match a3 with
| True -> S O
| False -> O)))
(match a2 with
| True -> S O
| False -> O))) (match a1 with
| True -> S O
| False -> O)
type string =
| EmptyString
| String of ascii * string
(** val aH : ascii **)
let aH =
Ascii (False, False, False, True, False, False, True, F...
(** val ae : ascii **)
let ae =
Ascii (True, False, True, False, False, True, True, Fal...
(** val al : ascii **)
let al =
Ascii (False, False, True, True, False, True, True, Fal...
(** val ao : ascii **)
let ao =
Ascii (True, True, True, True, False, True, True, False)
(** val aCMM : ascii **)
let aCMM =
Ascii (False, False, True, True, False, True, False, Fa...
(** val aSPC : ascii **)
let aSPC =
Ascii (False, False, False, False, False, True, False, ...
(** val aw : ascii **)
let aw =
Ascii (True, True, True, False, True, True, True, False)
(** val ar : ascii **)
let ar =
Ascii (False, True, False, False, True, True, True, Fal...
(** val ad : ascii **)
let ad =
Ascii (False, False, True, False, False, True, True, Fa...
(** val aEXCLAM : ascii **)
let aEXCLAM =
Ascii (True, False, False, False, False, True, False, F...
(** val aLF : ascii **)
let aLF =
Ascii (False, True, False, True, False, False, False, F...
(** val msg : string **)
let msg =
String (aH, (String (ae, (String (al, (String (al, (Str...
(aCMM, (String (aSPC, (String (aw, (String (ao, (Stri...
(String (ad, (String (aEXCLAM, (String (aLF,
EmptyString)))))))))))))))))))))))))))
最後に以上をまとめて結果を出すOCamlのコードmain.ml。~
この部分だけは証明することができない。
(* OCamlのコード *)
module Coq = Coqhelloworld
let rec int_of_nat = function
| Coq.O -> 0
| Coq.S p -> 1 + (int_of_nat p)
let length coqstr =
let rec length_aux n = function
| Coq.EmptyString -> n
| Coq.String (_, tl) -> length_aux (1+n) tl
in
length_aux 0 coqstr
let char_of_ascii a =
char_of_int (int_of_nat (Coq.nat_of_ascii a))
let string_of_coqstring coqstr =
let n = length coqstr in
let s = String.create n in
let rec aux i = function
| Coq.EmptyString -> ()
| Coq.String (hd, tl) ->
s.[i] <- char_of_ascii hd;
aux (i+1) tl
in
aux 0 coqstr;
s;;
print_string (string_of_coqstring Coq.msg);;
実行結果
Hello, world!
やった!できた!
* Proof are Programs [#fca44cec]
- http://www.radiumsoftware.com/0605.html#060523
- Philip Wadler. [[Proofs are Programs: 19th Century Logi...
- 数理論理学とコンピュータ・プログラムの間には深い関連性...
ページ名: