眠気と戦う日々

眠気と戦いながらプログラミングについていろいろと書くブログ

コンピュテーション式の変形後を覗き見る #FsAdvent

はじめに この記事はF# Advent Calendar 2014の10日目の記事です。 前日はbleisさんの「クラスのコンストラクタ呼び出し時にプロパティも同時に初期化する」でした。 本日はTipsからちょっと外れてネタをご紹介します。 タイトルにもある通り、コンピュテー…

リスト反転関数が単射であることを証明する

coq

久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。 問題のTheorem Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2. ソフトウェアの基礎ではCoqコードではありません…

内部でFixpointの関数を呼ぶ関数を定義した時にsimplだと証明できない

Coq

はい、表題のとおりです。 Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。 問題のコード Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Definition oddb (n:nat) : bool := negb (…

TAPL読書会@名古屋# 1に参加しました

ちょっとした前置き TaPL? TAPL? どっちなんでしょう。 ということで8月2日に開催されたTAPL読書会@名古屋#1に参加しました。 短歌会館というところの和室を借りて行いました。非常に雰囲気の良い所でしたので、お勧めです。 ただし無線LANとかはないので…

とある会社の新卒三年内離職率をアレした話

6/11を最終出社日として、新卒で入社した会社を6/30で退職する運びとなりました。で、7/1から愛知の某社に転がり込む感じです。 本エントリをもって関係各位への連絡と変えさせていただきます。 え、画像? なんか伝統らしいですね? (マズければ取り下げま…

24時間耐久ハッカソンを企画/主催しました

人生初のハッカソン企画/主催してしまいました。 細かい流れなどはpocketberserkerさんのtogetterがあるので、そちらを御覧ください。 http://togetter.com/li/567360 #24hack is 何 24時間ぶっ通しでハッカソンやりましょう! という企画です。 難しいこと…