読者です 読者をやめる 読者になる 読者になる

CoqでFizzBuzzを書いてみる

Coq

これ、やろうとすると結構難しい。ということで勉強がてら、Web上の他の人のものを参考にして理解しながら進めることにしました。つまりほぼ私が書いたものではないです。いちおう自分でいろいろ調べつつ、理解できていないところは理解しながら進めてみまし…

refineの例

Coq

Coqを勉強していたら、refineタクティクというものに出会った。一緒にSpecif moduleのsigの記述もあったので最初は混乱していたものの、何となく把握してきた。使い方は次のような感じ。 Definition pred (n : nat) : n>0 -> nat. refine (match n with | 0 …

任意の自然数a,b,cについてa*a+b*b=c*cのときにa,b,cすべてが奇数ではないことを証明してみた

Coq

Coqネタ。挑戦してみていろいろ勉強になった。試行錯誤はやっぱり勉強になる。勉強中はバックトラックでもタダでは起きない(キリッ 時間かかり過ぎですが。今回はタイトル通り、「任意の自然数a, b, cについて a*a+b*b=c*c のとき、a, b, cすべてが奇数ではな…

Coq to OCamlで便利な標準ライブラリ(型変換)

先日Coqの関数をOCamlのコードとして出力してみました。サンプルとしては (* ret_num.v *) Definition ret_num (n : nat) : nat := n. Extraction "ret_num.ml" ret_num. を coqc ret_num.vして (* ret_num.ml *) type nat = | O | S of nat (** val ret_num…

Coqの練習(2)

Coq

前回に引き続き、練習してます。今回はちょうど見つけたCoq-99 : Part 1の問題をやってみました。一応、答えを見ずに全部できましたが、所々詰まったりしました。ある意味、人間バックトラックです。 Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B)…

Coqの練習(1)

Coq

突然ですが、皆さんは定理証明支援器ってご存知ですか。 定理証明支援器というのは、命題論理の定理を半自動で証明することを可能にしてくれるツールです。去年の末、「テスト?ちがうちがう。これからの時代は証明だよ!」という話になったので、どうせOCam…