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

  template<typename F, typename X, typename Prop, typename Y>
  struct nat_forall_apply;
  
  template<typename F, typename X, typename Prop>
  struct nat_forall_apply<F, Prop, X, zero> {
    static typename subs<Prop, X, zero>::type proof(F f) {
      return f.p0;
    }
  };
  
  template<typename F, typename X, typename Prop, typename Y>
  struct nat_forall_apply<F, Prop, X, succ<Y> > {
    static typename subs<Prop, X, succ<Y> >::type proof(F f) {
      return f.p1(nat_forall_apply<F, X, Prop, Y>::proof(f));
    }
  };

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


    public:
      typedef typename subs<Prop, X, zero>::type base_prop;
      typedef typename subs< Prop, X, succ<N> >::type (*rec_prop)( typename subs< Prop, X, N >::type );

      base_prop p0;
      rec_prop p1;
      
      template<typename InductiveProof>
      forall( InductiveProof ) : p0(InductiveProof::base()), p1(&InductiveProof::step) {
      }

      template<typename Y>
      typename subs<Prop, X, Y>::type apply() { return nat_forall_apply<forall, X, Prop, Y>::proof(*this); }
    };
};

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

  typedef succ<succ<succ<zero> > > three;
  eq<add<zero, three>, add<three, zero> > p3 = p.apply<three>();
}