//------------------------------------------------------------------------------------
// [Metafunction] Substitution as usual
//------------------------------------------------------------------------------------

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;
	};





//------------------------------------------------------------------------------------
// Natural Numbers
//   The type "nat::forall<X, Prop>" is a proposition.
//   To create an instance (= proof) of the propotision,
//   you must supply
//     - an instance of type Prop[X/zero], and
//     - an instance of type Prop[X/N] -> Prop[X/succ<N>]
//------------------------------------------------------------------------------------

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;
			}
		};
	private: struct N {};
};




//------------------------------------------------------------------------------------
// Equality Predicate
//   can construct an instance of eq<N, M> if and only if N=M
//------------------------------------------------------------------------------------

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; // todo: how to make this extensible???
	};

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> >(); }
};




//------------------------------------------------------------------------------------
// Axiom of addition
//------------------------------------------------------------------------------------

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> > >(); }
};




//------------------------------------------------------------------------------------
// Main Proof
//------------------------------------------------------------------------------------

struct X {};
typedef nat::forall< X, eq< add<zero,X>, add<X, zero> > > theorem;

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 );
	}
};

int main()
{
	theorem p = inductive_proof();
}