Language: C C++ D Haskell Lua OCaml PHP Perl Plain Text Python Ruby Scheme Tcl //------------------------------------------------------------------------------------ // [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(); } Private [?] Run code