Coq

Coqで鳩の巣原理の証明

「Software Foundations」のLogic_Jで定式化された鳩の巣原理の証明。 pigeonhole_principle.v (* (* Logic_J.v の独自(<=)を使う場合はこの中身が必要 *) Lemma lt_irrefl : forall n, ~ n < n. Proof. induction n. intro. inversion H. intro. destruct IHn. apply […]

なぜCoqが重要か

%なぜCoqが重要か %@yoshihiro503 %平成26年4月29日 なぜCoqが重要か 結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhDが必要? 高校生でも練 […]

Coq で圏論:背景と普遍性について

まとめ そもそもどんな風に Coq で圏論やってるのかという話 存在性と唯一性で構成される普遍性を「函数とその性質」という形に変換して記述した 証明を割愛するという暴挙 参照しているソースコード それをライブラリ化したもの 背景 暇つぶしに、 Coq 上で Setoid ベースの構成的な圏論をやっている。 どういうことかというと、 普通の圏論における局所小(locally small)な圏を基準に、 普通の圏論における「集合」を Set […]

スタックコンパイラの証明

スタックコンパイラの証明 @suharahiromichi 2014_04_30 Require Import ssreflect ssrbool ssrnat seq eqtype ssrfun. 算術式をスタック指向のプログラミング言語にコンパイルするコンパイラ(スタックコンパイラ)が正しく動作することの証明をする。証明は SSReflect を使っておこなう。 ソースコードは以下にあります。 https://github.com/ […]

MacintoshでCoqide

名古屋のProof Cafeで永らくCoqを利用してきた。 http://proofcafe.org/wiki/ 持っていく機材が毎回違うと、毎回Coqを入れ直しをしていた。 導入済みの道具類によって、導入方法が違うと面倒である。 最近ではbrew cask install coqide”で導入している。 道具の導入の仕方が良くないと、うまく過去のプログラムを読み込まず、最初からファイルを読み込みながらやっていた。 資料類 […]

リフレクションのしくみをつくる

リフレクションのしくみをつくる 2015/08/11 2015/08/16 2015/09/12 「スモール SSReflect の製作」から改題 @suharahiromichi はじめに 命題(Prop型)をbool型の式に変換すること(とその逆)をリフレクションと呼びます。 例: x = y と x == y 命題をbool型の計算に変換することで、命題の証明が簡単になる場合があります。そのリフレクションを「狭い範囲」で行い、証明 […]

じぇねらるたんシールの注文方法

概要 ADPRINTというサービスを使って誰でもじぇねらるたんの形のシールを作ってもらうことができる。値段は1枚あたり約12円1。 ProofGeneral とは じぇねらるたんは ProofGeneralというツールの公式キャラクターであるが、このツールはCoqなどの対話的証明支援器で証明を対話的に開発するための Emacs プラグインである。 手順 ADPRINTではじぇねらるたんのデータを入校する前に、シールの大きさやタイプを指定 […]

試して面白いプログラミング言語6選

今日は、プログラマなら誰でも試して面白いと思えると私が考えているプログラミング言語6つを紹介したいと思います。 元記事 (英語) Haskell Haskellは静的型システムを持つ純粋関数型言語です。 Haskellはプログラミング言語の分野の有名な研究者たちによって設計されています。 Haskellによるプログラミングを通して、Haskellプログラマは、プログラミング言語の理論について多く学ぶことができます。 Haskellには優 […]