あぐだちゃんがトリックを仕掛けて来たようです

data Bool : Set0 where true : Bool ; false : Bool data _∨_ (A : Set0) (B : Set0) : Set0 where intro1 : A -> A ∨ B intro2 : B -> A ∨ B data Id {A : Set0} : A -> A -> Set0 where refl : (a : A) -> Id a a -- Boolはなぁ・・・trueか、falseだけな…

2009-10-31

これは買いたいなー

http://journal.mycom.co.jp/news/2009/10/30/087/index.htmlと思ったけど、PSPはついてないんですね。まぁPSP買っても良いかなーみたいなソレはどうしよう。12/3って確実に悲しい生活に陥ってるので何をやるにしても年末だよなぁみたいな。

2009-10-30

C++0xにはdefault template parameterがあるらしいです

ので取りあえずソレを使ってみてかわいそうな事をしてみたのですが int main() { Or<A,B> o = or_intro1<A,B>(A()); C c = or_elim(o,impl_intro(f),impl_intro(g)); //↓だとオッケー //C c = or_elim(or_intro1<A,B>(A()),impl_intro(f),impl_intro(g)); } error: no match</a,b></a,b></a,b>…

2009-10-27

計算機言語で定理証明#1

さる10月24日土曜日に大久保で次のようなイベントがありました。http://atnd.org/events/1507ありましたもといやりましたもとい出来ました。何度かこのブログでも人が少ない困ったみたいな事を書いたのですが、当日は最終的に9人の参加になりました。すごい…

2009-10-23

Haskell Not 98

{-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} data Zero data Succ a data Plus a b data Id :: * -> * -> * where Refl :: a -> Id a a Symm :: (Id a b) -> Id b a Tran :: (Id a b) -> (Id b c) -> (Id a c)…

2009-10-22

C++で証明のついったタイムラインまとめ

凄く見辛いですけど、タイムラインを纏めてみました。http://ranha.tumblr.com/day/2009/10/22/使ったのは、http://esuji.daa.jp/log/matome_st.php です。

2009-10-21

宣伝2

http://atnd.org/events/1507twitterで#proofpartyを付けて事前活動をもそもそやった結果9人に！！ありがとうございます。定員を一応10人としていて後1人大丈夫です、ので画面の前のキミ。そうキmry 来てください。今週土曜日に下のエントリでC++使ってした…

2009-10-21

お腹すいた...

ちゅらいね。この流れは...? //はてなのC++カラーリング指定子がcppになってるのどうにかしてくだち /* 取りあえずNat */ struct zero{}; template<typename>struct succ{}; template<typename N1,typename N2>struct add{}; template<typename N2> struct add<zero,N2> { typedef N2 val; }; template<typename N1,typename N2> struct add<succ<N1>,N2> </succ<n1></typename></zero,n2></typename></typename></typename>…

2009-10-20

ねむいよー

ちゅらいね・・・。kinabaさんが楽しいものを昨日twitterに流していた(http://twitter.com/kinaba/status/4986574175)ので、ももーい生放送が終わった辺りからねむいねむい言って別の補題(n + (succ m) == succ (n + m))を１つ証明してみました。で、その流…

2009-10-18

お腹空いた...

#include <iostream> using namespace std; struct True{}; struct False{}; struct Zero{}; template<typename T> struct Succ{}; template<typename A,typename B> struct Add { }; template<typename B> struct Add<Zero,B> { typedef B val; }; template<typename A,typename B> struct Add<Succ<A>,B> { typedef typen…</succ<a></typename></zero,b></typename></typename></typename></iostream>

2009-10-18

色々足りてないから酷い

data Nat : Set0 where zero : Nat succ : Nat -> Nat leibnizEq : Nat -> Nat -> Set1 leibnizEq x1 y1 = (P1 : Nat -> Set0) -> P1 x1 -> P1 y1 g : (P2 : Nat -> Set0) -> Nat -> Nat -> Set0 g P3 x2 z2 = (P3 z2 -> P3 x2) h : (P4 : Nat -> Set0) -> (…

2009-10-16

計算機言語を使った定理証明の会

http://atnd.org/events/150710月24日東京は大久保です。人が7人ぐらい居ないとちょっと広いなーという部屋を借りてしまっているので、俺はやるぞ！！って人はなんとしても来てください。全く宣伝になってないなー。「当日までにやってくるべきお題」がま…

2009-10-15

はこはるるん

今日はカナダ政治の試験らしいけど・・・。なんか明らかに基礎的な所がかけてるので辛いっていうか、まぁなんかこれらはゲームだよなぁみたいな感じです。そう、ゲームだと良いんですけど、そういう要素は無くて全部覚えてこいっていうそれなので心を消して…

2009-10-14

■

data Bool : Set0 where true : Bool false : Bool data BoolHold : Bool -> Set0 where boolHold : (b1 : Bool) -> BoolHold b1 not : Bool -> Bool not b2 with b2 ... | true = false ... | false = true g : (b : Bool) -> BoolHold (not b) g b with b …