mzpのブックマーク - はてなブックマーク

Coqで多重再帰のデータ構造を証明する - にわとり小屋でのプログラミング

Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_indは次の様な型を持っている。 Coq < Check list_ind. list_ind : forall (A : Set) (P : list A -> Prop), P (Nil A) -> (forall (x : A) (xs : list A), P xs -> P (Cons A x xs)) -> forall l : list A, P l このlist_indは帰納法に関して非常に強力である。リストを引数に持つような任意の述語Pに対し

mzp 2010/09/28

これにひっかかった。常によしひろさんが先にいる感じだ。

Coq

リンク

Coqでニコニコ :-] - にわとり小屋でのプログラミング

Coqで証明をする動画を作って、にこにこ動画に公開した。 http://www.nicovideo.jp/watch/sm1276083

mzp 2007/10/16

リンク

大阪人に関するうわさ - にわとり小屋でのプログラミング

世の中には大阪人に関する間違った認識があふれているように思う。例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。今回はそのような間違った俗説を払拭するべくCoqで証明してみた。 Coq < Section なにわ. まず、次のような文を定めて、６つの噂を仮定する。ただし ~（にょろ）は否定を表す記号である。 Coq < Variable 大阪人である : Prop. Coq < Variable たこ焼きを食べたことがある : Prop. Coq < Variable 常に縦縞の服を着る : Prop. Coq < Variable 嫁さんの尻に敷かれてる : Prop. Coq < Variable 阪神の試合には欠かさず行く : Prop. 大阪人である is assumed たこ焼きを食べたことがある is assumed 常に縦縞の

mzp 2007/07/24

リンク

Coqのインストール - にわとり小屋でのプログラミング

最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。対象となる OS はWindows Vistaだ! Coqはだいたい次の３ステップで、使うことが出来る。恐れずに挑戦してみよう。 1。CoqのサイトからCoqのもとをダウンロード → 2。それを自分のパソコンにセットアップ → 3。起動 1。Coqのもとをダウンロードまずは Coqのサイトを見てみよう。(インターネットにつながっている必要がある。注意しよう) そこは黄色い雰囲気のサイトで、何やら英語でいろいろ書いてあるだろう。よくみると[Coq 8.1]という項目の近くに鶏の絵があって、その近くに Download とかいてある部分が見つかる。そこをマウスでクリックしてみよう。 [The current version : Coq 8.1]という項目の中をよくよくさが