ProofCafe

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 […]

MacintoshでCoqide

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