gistfile1.cpp

#include <stdio.h>

//http://stackoverflow.com/questions/281725/template-specialization-based-on-inherit-class
template<typename D, typename B>
class IsDerivedFrom
{
  class No { };
  class Yes { No no[3]; }; 

  static Yes Test( B* ); // not defined
  static No Test( ... ); // not defined 

  static void Constraints(D* p) { B* pb = p; pb = p; } 

public:
  enum { Is = sizeof(Test(static_cast<D*>(0))) == sizeof(Yes) }; 

  IsDerivedFrom() { void(*p)(D*) = Constraints; }
};

struct Prop {};

struct True : public Prop { const char *what() { return "True"; } };
struct False : public Prop { const char *what() { return "False"; } };

template<class> struct Always : public True {};
template<class> struct Never : public False {};

template<template<typename>class> struct ForAll : public False {};
template<> struct ForAll<Always> : public False {};

template<class T> struct Assert { static_assert(IsDerivedFrom<T, True>::Is, "oh no");};

template<bool b> struct TrueFalseChooser {};
template<> struct TrueFalseChooser<true>  : public True {};
template<> struct TrueFalseChooser<false> : public False {};
template<class T1, class T2> struct And : public TrueFalseChooser<IsDerivedFrom<T1, True>::Is && IsDerivedFrom<T2, True>::Is> {};
template<class T1, class T2> struct Or :  public TrueFalseChooser<IsDerivedFrom<T1, True>::Is || IsDerivedFrom<T2, True>::Is> {};

struct Type {};

namespace Nat {
    
    struct Nat : public Type {
        const bool Is_Nat = true;
    private:
        constexpr Nat(){}
    };
    
    struct O : public Nat {
        O() = default;
    };
    template <class P>
    struct S : public Nat {    
        S() = default;
    };
    
    template <char> struct var : public Nat {};
    
    template<int N>
    struct nat {
		using value = S<typename nat<N - 1>::value>;
    };
    template<> struct nat<0> { using value = O; };
    
    template<class T1, class T2>
    struct eq : public False {
        static_assert(T1::Is_Nat, "T1 isn't Nat");
        static_assert(T2::Is_Nat, "T2 isn't Nat");
        static_assert(sizeof(T1)!=sizeof(T1), "oh no");
    };
    template<char c> struct eq<var<c>, var<c>> : public True { };
    template<> struct eq<O, O> : public True { };
    template<class T1, class T2> struct eq<S<T1>, S<T2>> : public eq<T1, T2> { };
    
    template<class T1, class T2>
    struct add {
        static_assert(sizeof(T1) != sizeof(T1), "oops");
    };
    template<class T1> struct add<O, T1> { using value = T1; };
    template<class T1> struct add<T1, O> { using value = T1; };
    template<class T1, class T2> struct add<S<T1>, T2> { using value = S<typename add<T1, T2>::value>; };
    
    // Axiom S n + m = S (n + m)
    template<class N> struct add_Sn_m { static_assert(sizeof(N) != sizeof(N), "cannot rewrite"); };
    template<class N, class M> struct add_Sn_m<add<S<N>,M>> { using expr = S<add<N, M>>; };
    
    // Axiom n + S m = S (n + m)
    template<class N> struct add_n_Sm { static_assert(sizeof(N) != sizeof(N), "cannot rewrite"); };
    template<class N, class M> struct add_n_Sm<add<N,S<M>>> { using expr = S<add<N, M>>; };
    
    // Goal a + b = b + a.
    // Proof.
    // Induction a. (might be wrong)
    //   0 + b = b + 0. (who cares? too trivial)
    //   [a : Nat] a + b = b + a -> S a + b = b + S a
    
    // Induction b. (might be wrong)
    //   [a b : Nat] a + b = b + a -> a + S b = S b + a /\
    //               a + S b = S b + a -> S a + S b = S b + S a
    
    // $ a + S b
    struct eq_1 { using expr = add<var<'a'>, S<var<'b'>>>; };
    // $ S b + a
    struct eq_2 { using expr = add<S<var<'b'>>, var<'a'>>; };
    
    // premise: a + b = b + a
    template<class T1, class T2> struct local_eq_1 : public eq<T1, T2> {};
    template<class T1, class T2> struct local_eq_1<S<T1>,S<T2>> : public local_eq_1<T1, T2> {};
    template<> struct local_eq_1<add<var<'a'>,var<'b'>>, add<var<'b'>,var<'a'>>> : public True {};
    
    // rewrite using add_n_Sm
    struct eq_3 { using expr = add_n_Sm<eq_1::expr>::expr; };
    
    // rewrite using add_Sn_m
    struct eq_4 { using expr = add_Sn_m<eq_2::expr>::expr; };
    
    // now prove a + b = b + a -> a + S b = S b + a
    struct prop_1 : public local_eq_1<eq_3::expr, eq_4::expr> {};
    
    // next, prove a + S b = S b + a -> S a + S b = S b + S a
    
    // premise: a + S b = S b + a
    template<class T1, class T2> struct local_eq_2 : public eq<T1, T2> {};
    template<class T1, class T2> struct local_eq_2<S<T1>,S<T2>> : public local_eq_2<T1, T2> {};
    template<> struct local_eq_2<add<var<'a'>,S<var<'b'>>>, add<S<var<'b'>>,var<'a'>>> : public True {};
    
    // $ S a + S b
    struct eq_5 { using expr = add<S<var<'a'>>, S<var<'b'>>>; };
    // $ S b + S a
    struct eq_6 { using expr = add<S<var<'b'>>, S<var<'a'>>>; };
    
    // rewrite using add_Sn_m
    struct eq_7 { using expr = add_Sn_m<eq_5::expr>::expr; };
    
    // rewrite using add_n_Sm
    struct eq_8 { using expr = add_n_Sm<eq_6::expr>::expr; };
    
    // complete the proof of a + S b = S b + a -> S a + S b = S b + S a
    struct prop_2 : public local_eq_2<eq_7::expr, eq_8::expr> {};
    
    // Qed.
    struct add_reflexivity : public And<prop_1, prop_2> {};
}


int main() {
    using P = Nat::eq<Nat::add<Nat::nat<2>::value, Nat::nat<3>::value>::value, Nat::nat<5>::value>;
    Assert<P> asserter{};
    
    using P2 = Nat::add_reflexivity;
    Assert<P2> asserter2{};
}