お腹すいた...

ちゅらいね。

この流れは...?

//はてなの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>
{
    typedef succ<typename add<N1,N2>::val> val;
};

/*
  まず、NatId相当を作る
*/
 
template<typename N1,typename N2>
struct NatId
{
};

struct Refl
{
    template<typename N>
    static NatId<N,N> proof(){return NatId<N,N>();}
};

struct Symm
{
    template<typename N1,typename N2>
    static NatId<N2,N1> proof(NatId<N1,N2>){return NatId<N2,N1>();}
};

struct Tran
{
    template<typename N1,typename N2,typename N3>
    static NatId<N1,N3> proof(NatId<N1,N2>,NatId<N2,N3>){return NatId<N1,N3>();}
};

struct succId
{
    template<typename N1,typename N2>
    static NatId<succ<N1>,succ<N2> > proof(NatId<N1,N2>){return NatId<succ<N1>,succ<N2> >();}
};

//(0 + x) == (x + 0)
/*
template<typename N>
struct Lemma1
{
    static
    NatId<add<zero,zero>::val,add<zero,zero>::val > case0()
	{
	    //return Refl<add<zero,zero>::val>::proof();
	    return Refl::proof<zero>();
	}

    static
    NatId<typename add<zero,succ<N> >::val,typename add<succ<N>,zero>::val>
    caseN(NatId<typename add<zero,N>::val,typename add<N,zero>::val> hypo)
	{
	    NatId<typename add<zero,N>::val,N> p1 = Refl::proof<N>();
	    NatId<N,typename add<N,zero>::val> p2 = Tran::proof(Symm::proof(p1),hypo);
	    NatId<succ<N>,succ<typename add<N,zero>::val> > p3 = succId::proof(p2);
	    NatId<typename add<succ<N>,zero>::val,succ<typename add<N,zero>::val> > p4 = Refl::proof<typename add<succ<N>,zero>::val>();
	    NatId<succ<N>,typename add<succ<N>,zero>::val> p5 = Tran::proof(p3,Symm::proof(p4));
	    NatId<typename add<zero,succ<N> >::val,succ<N> > p6 = Refl::proof<succ<N> >();
	    NatId<typename add<zero,succ<N> >::val,typename add<succ<N>,zero>::val> goal = Tran::proof(p6,p5);
	}
};
*/

template<typename N>
struct Lemma1{};

template<>
struct Lemma1<zero>
{
    static
    NatId<add<zero,zero>::val,add<zero,zero>::val > proof()
	{
	    return Refl::proof<add<zero,zero>::val>();
	}
};

template<typename N>
struct Lemma1<succ<N> >
{
    static
    NatId<typename add<zero,succ<N> >::val,typename add<succ<N>,zero>::val>
    proof(NatId<typename add<zero,N>::val,typename add<N,zero>::val> hypo)
	{
	    NatId<typename add<zero,N>::val,N> p1 = Refl::proof<N>();
	    NatId<N,typename add<N,zero>::val> p2 = Tran::proof(Symm::proof(p1),hypo);
	    NatId<succ<N>,succ<typename add<N,zero>::val> > p3 = succId::proof(p2);
	    NatId<typename add<succ<N>,zero>::val,succ<typename add<N,zero>::val> > p4 = Refl::proof<typename add<succ<N>,zero>::val>();
	    NatId<succ<N>,typename add<succ<N>,zero>::val> p5 = Tran::proof(p3,Symm::proof(p4));
	    NatId<typename add<zero,succ<N> >::val,succ<N> > p6 = Refl::proof<succ<N> >();
	    NatId<typename add<zero,succ<N> >::val,typename add<succ<N>,zero>::val> goal = Tran::proof(p6,p5);
	}

    static
    NatId<typename add<zero,succ<N> >::val,typename add<succ<N>,zero>::val>
    proof()
	{
	    NatId<typename add<zero,N>::val,typename add<N,zero>::val> hypo = Lemma1<N>::proof();
	    return proof(hypo);
	}
};

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

template<typename M>
struct Lemma2<zero,M>
{
    static
    NatId<typename add<zero,succ<M> >::val,succ<typename add<zero,M>::val> >
    proof()
	{
	    NatId<typename add<zero,succ<M> >::val,succ<M> > p1 = Refl::proof<succ<M> >();
	    NatId<typename add<zero,M>::val,M> p2 = Refl::proof<M>();
	    NatId<succ<typename add<zero,M>::val>,succ<M> > p3 = succId::proof(p2);
	    NatId<typename add<zero,succ<M> >::val,succ<typename add<zero,M>::val> > goal = Tran::proof(p1,Symm::proof(p3));
	    return goal;
	}
};
    
template<typename N,typename M>
struct Lemma2<succ<N>,M>
{
    static
    NatId<typename add<succ<N>,succ<M> >::val,succ<typename add<succ<N>,M>::val> >
    proof(NatId<typename add<N,succ<M> >::val,succ<typename add<N,M>::val> > hypo)
	{
	    NatId<succ<typename add<N,M>::val>,typename add<succ<N>,M>::val> p1 = Symm::proof(Refl::proof<succ<typename add<N,M>::val> >());
	    NatId<succ<typename add<N,succ<M> >::val>,succ<succ<typename add<N,M>::val> > > p2 = succId::proof(hypo);
	    NatId<typename add<succ<N>,succ<M> >::val,succ<typename add<N,succ<M> >::val> > p3 = Refl::proof<typename add<succ<N>,succ<M> >::val>();
	    NatId<succ<succ<typename add<N,M>::val> >,succ<typename add<succ<N>,M>::val> > p4 = succId::proof(p1);
	    NatId<typename add<succ<N>,succ<M> >::val,succ<succ<typename add<N,M>::val> > > p5 = Tran::proof(p3,p2);
	    NatId<typename add<succ<N>,succ<M> >::val,succ<typename add<succ<N>,M>::val> > goal = Tran::proof(p5,p4);
	    return goal;
	}

    static
    NatId<typename add<succ<N>,succ<M> >::val,succ<typename add<succ<N>,M>::val> >
    proof()
	{
	    NatId<typename add<N,succ<M> >::val,succ<typename add<N,M>::val> > hypo = Lemma2<N,M>::proof();
	    return proof(hypo);
	}
};

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

//0+M = M+0
template<typename M>
struct Theorem<zero,M>
{
    static
    NatId<typename add<zero,M>::val,typename add<M,zero>::val>
    proof()
	{
	    return Lemma1<M>::proof();
	}
};

template<typename N,typename M>
struct Theorem<succ<N>,M>
{
    static
    NatId<typename add<succ<N>,M>::val,typename add<M,succ<N> >::val>
    proof(NatId<typename add<N,M>::val,typename add<M,N>::val> hypo)
	{
	    NatId<succ<typename add<N,M>::val>,succ<typename add<M,N>::val> > p1 = succId::proof(hypo);
	    NatId<typename add<succ<N>,M>::val,succ<typename add<N,M>::val > > p2 = Refl::proof<typename add<succ<N>,M>::val>();
	    NatId<typename add<succ<N>,M>::val,succ<typename add<M,N>::val > > p3 = Tran::proof(p2,p1);
	    NatId<typename add<M,succ<N> >::val,succ<typename add<M,N>::val> > p4 = Lemma2<M,N>::proof();
	    NatId<succ<typename add<M,N>::val>,typename add<M,succ<N> >::val> p5 = Symm::proof(p4);
	    NatId<typename add<succ<N>,M>::val,typename add<M,succ<N> >::val> goal = Tran::proof(p3,p5);
	    return goal;
	}

    static
    NatId<typename add<succ<N>,M>::val,typename add<M,succ<N> >::val>
    proof()
	{
	    NatId<typename add<N,M>::val,typename add<M,N>::val> hypo = Theorem<N,M>::proof();
	    return proof(hypo);
	}
};

int main()
{
    typedef succ<zero> one;
    typedef succ<one> two;
    typedef succ<two> three;
    typedef succ<three> four;
    typedef succ<four> five;
    typedef succ<five> six;
    typedef succ<six> seven;
    typedef succ<seven> eight;
    typedef succ<eight> nine;
    typedef succ<nine> ten;
    typedef add<ten,ten>::val twenty;
    typedef add<twenty,twenty>::val fourty;

    NatId<add<zero,zero>::val,add<zero,zero>::val > l1 = Lemma1<zero>::proof();
    //NatId<add<zero,one>::val,add<one,zero>::val > l2 = Lemma1<one>::proof(l1);//一々渡してやるのが面倒臭い!!

    NatId<add<zero,one>::val,add<one,zero>::val > l3 = Lemma1<one>::proof();//のでボトムアップな感じに

    NatId<add<zero,succ<two> >::val,succ<add<zero,two>::val> > l4 = Lemma2<zero,two>::proof();
    NatId<add<one, succ<two> >::val,succ<add<one, two>::val> > l5 = Lemma2<one,two>::proof();

    NatId<add<zero,three>::val,add<three,zero>::val > l6 = Theorem<zero,three>::proof();
    NatId<add<one, three>::val,add<three,one >::val > l7 = Theorem<one ,three>::proof();

    //10 + 9 = 9 + 10
    NatId<add<ten,nine>::val,add<nine,ten>::val> th1 = Theorem<nine,ten>::proof();
    NatId<add<twenty,nine>::val,add<nine,twenty>::val> th2 = Theorem<nine,twenty>::proof();
    NatId<add<fourty,twenty>::val,add<twenty,fourty>::val> th3 = Theorem<fourty,twenty>::proof();
}

流れ

http://twitter.com/kikx/status/5014473813
http://twitter.com/kinaba/status/5014726804
http://twitter.com/kikx/status/5014803334

C++を使う人がそういうんだから、という事で遠慮なくそうしてみました。

LemmaとかTheoremの中で押し込むんじゃなくて、そいつらはproofという関数を持っていて、証明した結果を返すという形にしています。
で、元のkinabaさんのコード(codepadのコード参照)にあった明示的なforallは、template変数で代わりにしちゃってます。

kinabaさんのコードにはprivateなダミーっぽいstructとか、グローバルに置かれているstructがあってそれがパターンの代わりを果たして居たのですがそれらは全て除去。
してしまった結果、インスタンス化が無いのでどう考えても間違っている証明過程でも、「証明自体は」コンパイル自体は通ってしまうようになります。
上のように値を与えて具体化すれば弾いてはくれますが・・・。

これだと本当に証明しているというよりは、C++で「ソレっぽくやってみた」であってうーんというかなんというか・・・。

なんていうか、コアは2,3日前に書いたヤツと変わらない気がします。

ただまぁ取りあえずあちこちにtypenameが付くのと"::val"が付くのは勘弁して欲しいっていう感じですよねぇ・・・。

取りあえずkinabaさんの解説も上がるらしいので、C++な視点からのソレを超期待！！
http://twitter.com/ranha/status/4993087027
http://twitter.com/kinaba/status/4993650737

その他

心の底から、succはzeroかsuccしか取れないとかいうような制約を書きたいです・・・。

それから、Mac版バイナリconceptgccは何か知らないけどdylibで死ぬとかでこっちがお前を許さないって感じ。

改良案

addの定義をvalを持たせる系じゃなくてeq_addに変える。
これだとパターンを表すクラス(class,struct)を使っても耐える感じなので、というソレ。

お腹空いた。