[Coq] Coq-99 : Part 1
Personal memorandum for studying functional languages, theorem proving, and formal verification. But other topics might be included. Written in Japanese (Shift-JIS Encoding). 前にS-99: Ninety-Nine Scala Problemsというのを紹介しましたが、Coqでも入門者が勉強用に解く為の問題集というのを考えてみました。 まずは命題論理の証明の課題。勿論、tautoとかで一発だと思いますが、練習問題なので入門者は自力で解こう。 Admitted.を消して証明を書く事が期待されています。 Section Prop_Logic. Lemma Coq_01 : forall A B C:Prop, (A->B-
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - kik/TaraiTermination: Proof of general Tarai function termination problem by Coq