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

namespace nat
{
  namespace induction {
    template<template<class>class Prop, typename Y, template<class>class InductionProp>
    struct apply_induction;

    template<template<class>class Prop, template<class>class InductionProp>
    struct apply_induction<Prop, zero, InductionProp> {
      static typename Prop<zero>::type proof() { return InductionProp<zero>::base_proof(); }
    };

    template<template<class>class Prop, typename Y, template<class>class InductionProp>
    struct apply_induction<Prop, succ<Y>, InductionProp> {
      static typename Prop<succ<Y> >::type proof() { return InductionProp<Y>::step_proof(apply_induction<Prop, Y, InductionProp>::proof()); }
    };
    
    template<template<class>class Prop, template<class>class InductionProp>
    struct forall_by_ind {
      template<typename Y>
      static typename Prop<Y>::type proof() { return apply_induction<Prop, Y, InductionProp>::proof(); }
    };
  }

}

//------------------------------------------------------------------------------------
// 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
//------------------------------------------------------------------------------------

template<typename N>
struct inductive_proof
{
  static eq< add<zero,zero>, add<zero, zero> > base_proof() {
    return eq_refl::proof< add<zero,zero> >();
  }

  static eq< add< zero,succ<N> >, add<succ<N>,zero> > step_proof( 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 );
  }
};



struct theorem {
private:
  template<typename X>
  struct prop {
    typedef eq<add<zero, X>, add<X, zero> > type;
  };
public:
  template<typename X>
  static typename prop<X>::type proof() {
    typedef nat::induction::forall_by_ind<prop, inductive_proof > type;
    return type::template proof<X>();
  }
};

int main()
{
  typedef succ<succ<succ<zero> > > three;
  eq<add<zero, three>, add<three, zero> > p3 = theorem::proof<three>();
}