ねむいよー

ちゅらいね・・・。

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

で、その流れで起きてから可換性の証明も出来ないかなーというソレで。

最初は、定理毎にnamespaceを作ってやっていたのですがC++ではnamespaceにtemplate付けてparametrizeするのはダメらしいのでstructで包み直す感じにしました。

で、まぁ問題なのはforallの中に含まれているconvってヤツ。これはforall a.Pが言えたならaの所を適当にインスタンスにしてPを言っちゃっても良いよねっていう事で導入したものです。

何が良いって、このレベルでプログラム(じゃあ無いような...)を書く時には関数の中身を埋める必要なんざねぇ！！！！！っていうあーーこれは酷い・・・。いや埋めないとダメですよ?証明なので。

あとは、定理を証明している最中に、他の証明を上手く利用する為に利用する側の定理をこれまた型変数でparametrizeしてます。

なんか個人的にはnamespaceで区切った方が以下略。

template<typename T, typename X, typename V>
struct subs {
    typedef T type;
};
template<typename X, typename V>
struct subs<X,X,V> {
    typedef V type;
};
template<template<class> class Uni, typename T1, typename X, typename V>
struct subs<Uni<T1>,X,V> {
    typedef Uni<typename subs<T1,X,V>::type> type;
};
template<template<class,class> class Bin, typename T1, typename T2, typename X, typename V>
struct subs<Bin<T1,T2>,X,V> {
    typedef Bin<typename subs<T1,X,V>::type,
		typename subs<T2,X,V>::type> type;
};


struct zero {};
template<typename> struct succ {};

struct nat
{
    template<typename X, typename Prop>
    class forall
    {
    private:
	forall();

    public:
	template<typename InductiveProof>
	forall( InductiveProof )
	    {
		typename subs<Prop, X, zero>::type p0
		    = InductiveProof::base();

		typename subs< Prop, X, succ<N> >::type (*pf)( typename subs< Prop, X, N >::type )
		    = &InductiveProof::step;
	    }

	template<typename InductiveProof>
	static Prop conv(InductiveProof)
	    {
		typename subs<Prop, X, zero>::type p0
		    = InductiveProof::base();

		typename subs< Prop, X, succ<N> >::type (*pf)( typename subs< Prop, X, N >::type )
		    = &InductiveProof::step;
	    }
    };
private: struct N {};
};


template<typename N, typename M>
class eq
{
    eq() {}
public:
    friend class eq_symm;
    friend class eq_tran;
    friend class eq_refl;
    friend class eq_succ;

    friend class eq_add;
};

struct eq_symm {
    template<typename N, typename M>
    static eq<M,N> proof( eq<N,M> ) { return eq<M,N>(); }
};
struct eq_tran {
    template<typename N, typename K, typename M>
    static eq<N,M> proof( eq<N,K>, eq<K,M> ) { return eq<N,M>(); }
};
struct eq_refl {
    template<typename N>
    static eq<N,N> proof() { return eq<N,N>(); }
};
struct eq_succ {
    template<typename N, typename M>
    static eq< succ<N>,succ<M> > proof( eq<N,M> ) { return eq< succ<N>, succ<M> >(); }
};


template<typename N, typename M>
struct add {};

struct eq_add
{
    template<typename N>
    static eq<add<zero,N>, N> zero_plus()
	{ return eq<add<zero,N>, N>(); }

    template<typename N, typename M>
    static eq< add<succ<N>,M>, succ< add<N,M> > > succ_plus()
	{ return eq< add<succ<N>,M>, succ< add<N,M> > >(); }
};


/*
  0 + X = X + 0
 */
template<typename T>
struct Lemma1
{
    typedef nat::forall< T, eq< add<zero, T>, add<T, zero> > > lemma;
    
    struct inductive_proof
    {
	static eq< add<zero,zero>, add<zero, zero> > base()
	    {
		return eq_refl::proof< add<zero,zero> >();
	    }
	
	template<typename N>
	static eq< add< zero,succ<N> >, add<succ<N>,zero> > step( eq< add<zero,N>, add<N,zero> > indhyp )
	    {
		eq< add<zero,N>, N > p1 = eq_add::zero_plus<N>();
		eq< N, add<N,zero> > p2 = eq_tran::proof( eq_symm::proof(p1), indhyp );
		
		eq< succ<N> , succ< add<N,zero> > >         p3 = eq_succ::proof( p2 );
		eq< add<succ<N>,zero>, succ<add<N,zero> > > p4 = eq_add::succ_plus<N,zero>();
		eq< succ<N> , add<succ<N>,zero> >           p5 = eq_tran::proof( p3, eq_symm::proof(p4) );
		
		eq< add< zero,succ<N> >, succ<N> > p6 = eq_add::zero_plus< succ<N> >();
		return eq_tran::proof( p6, p5 );
	    }
    };
};


/*
  (n + (succ m)) == (succ (n + m))
 */

template<typename N,typename M>
struct Lemma2
{
    typedef nat::forall<N,eq<add<N,succ<M> >,succ<add<N,M> > > > lemma;
    
    struct inductive_proof
    {
	//N = zeroの時
	static eq<add<zero,succ<M> >,succ<add<zero,M> > > base()
	    {
		eq<add<zero,succ<M> >,succ<M> > p1 = eq_add::zero_plus<succ<M > >();

		eq<add<zero,M>,M> p2 = eq_add::zero_plus<M>();

		eq<succ<add<zero,M> >,succ<M> > p3 = eq_succ::proof(p2);

		eq<add<zero,succ<M> >,succ<add<zero,M> > > p4 = eq_tran::proof(p1,eq_symm::proof(p3));

		return p4;
	    }

	//N = succ Xの時
	template<typename X>
	static eq<add<succ<X>,succ<M> >,succ<add<succ<X>,M> > >
	step(eq<add<X,succ<M> >,succ<add<X,M> > > indhyp)//X+(1+M) == 1+(X+M)
	    {
		//1+(X+M) = (1+X)+M
		eq<succ<add<X,M> >,add<succ<X>,M> > p1 = eq_symm::proof(eq_add::succ_plus<X,M>());

		//1+(X+(1+M)) == 1+1+(X+M)
		eq<succ<add<X,succ<M> > >,succ<succ<add<X,M> > > > p2 = eq_succ::proof(indhyp);
		
		//(1+X) + (1+M) == 1+(X+(1+M))
		eq<add<succ<X>,succ<M> >,succ<add<X,succ<M> > > > p3 = eq_add::succ_plus<X,succ<M> >();

		//1+1+(X+M) == 1+((1+X)+M)
		eq<succ<succ<add<X,M> > >,succ<add<succ<X>,M> > > p4 = eq_succ::proof(p1);

		//(1+X) + (1+M) == 1+(1+(X+M))
		eq<add<succ<X>,succ<M> >,succ<succ<add<X,M> > > > p5 = eq_tran::proof(p3,p2);

		//(1+X) + (1+M) == 1+((1+X)+M)
		eq<add<succ<X>,succ<M> >,succ<add<succ<X>,M> > > p6 = eq_tran::proof(p5,p4);

		return p6;
	    }
    };
};

struct Theorem
{
    struct N{};
    struct M{};

    //N + M == M + N
    typedef nat::forall<N,eq<add<N,M>,add<M,N> > > theorem;

    struct inductive_proof
    {
	static eq<add<zero,M>,add<M,zero> > base()
	    {
		eq<add<zero,M>,add<M,zero> > p1 = nat::forall<M,eq<add<zero,M>,add<M,zero> > >::conv(Lemma1<M>::inductive_proof());

		return p1;
	    }

	template<typename X>
	static eq<add<succ<X>,M>,add<M,succ<X> > > step(eq<add<X,M>,add<M,X> > indhyp)
	    {
		//1+(X+M) == 1+(M+X)
		eq<succ<add<X,M> >,succ<add<M,X> > > p1 = eq_succ::proof(indhyp);
		
		//(1+X)+M == 1+(M+X)
		//の為に
		//(1+X)+M = 1+(X+M)を言う
		eq<add<succ<X>,M>,succ<add<X,M> > > p2 = eq_add::succ_plus<X,M>();

		//(1+X)+M == 1+(M+X)
		eq<add<succ<X>,M>,succ<add<M,X> > > p3 = eq_tran::proof(p2,p1);

		//1+(M+X) == M + (1+X)が欲しい
		//Lemma2を使って
		//M+(1+X) == 1+(M+X)を得る
		eq<add<M,succ<X> >,succ<add<M,X> > > p4 =
		    nat::forall<M,eq<add<M,succ<X> >,succ<add<M,X> > > >::conv(typename Lemma2<M,X>::inductive_proof());

		//1+(M+X) == M+(1+X)
		eq<succ<add<M,X> >,add<M,succ<X> > > p5 = eq_symm::proof(p4);
		
		//(1+X)+M == M+(1+X)
		eq<add<succ<X>,M>,add<M,succ<X> > > p6 = eq_tran::proof(p3,p5);
		return p6;
	    }
    };
};

int main()
{
    Theorem::theorem th = Theorem::inductive_proof();
    return 0;
}

超ref : http://codepad.org/L4feGX1J

不味い匂がぷんぷんぷんぷんする(http://twitter.com/kinaba/status/5013758164)けど、ちかたないね。いやちかたあるけど授業です。convは個人的にはまぁコレでいいだろうのなんちゃって(一階述語論理の∀-elimination的な)まぁしかたないですねのソレで日本語でおk

あと、なんだろう、conceptは全然知らない(リアルに知りません)んですが、アレを使えるともうちょっと縛って書けるのかなーとか。

今だとzeroとsuccが無関係だったりするので、そこに関係を作ってどうこう・・・とか?
いや無駄かなぁ・・・。ConceptGCC使ったら他におもろい事出来るのかな?

追記

http://d.hatena.ne.jp/ranha/20091021/1256055346