compile time proof

system_lp.hpp

#pragma once

// Copyright plasma-effect 2015
// Distributed under the Boost Software License, Version 1.0.
// (See http://www.boost.org/LICENSE_1_0.txt)

#include<type_traits>
namespace plasma
{
	namespace proof_system
	{
		namespace detail
		{
			template<class T, class... Ts>struct and_type_i :and_type_i<Ts...> {};
			template<class... Ts>struct and_type_i<std::false_type, Ts...> :std::false_type {};
			template<>struct and_type_i<std::true_type> :std::true_type {};
		}
		template<class... Ts>struct and_type :detail::and_type_i<typename Ts::type...> {};

		template<class T,class U>struct implication{};
		template<class T>struct logical_not{};
		template<class T, class U>using logical_or = implication<logical_not<T>, U>;
		template<class T, class U>using logicaland = logical_not<logical_or<logical_not<T>, logical_not<U>>>;

		template<class Conclusion, class... Claims>struct proof_tree :std::false_type {};
		template<class T, class U>struct proof_tree<T, implication<U, T>, U> :std::true_type {};
		template<class T, class U>struct proof_tree<T, U, implication<U, T>> :std::true_type {};


		template<class Conclusion, class... Assumption>struct proof :and_type<proof_tree<Conclusion, typename Assumption::claim...>, Assumption...>
		{
			typedef Conclusion claim; 
		};

		template<class T, class U>struct proof<implication<T, implication<U, T>>> :std::true_type
		{
			typedef implication<T, implication<U, T>> claim;
		};
		template<class T, class U, class V>struct proof < implication <implication<T, implication<U, V>>,implication<implication<T, U>, implication<T, V>>>>:std::true_type
		{
			typedef implication<implication<T, implication<U, V>>,
				implication<implication<T, U>, implication<T, V>>> claim;
		};
		template<class T,class U>struct proof<implication<implication<logical_not<U>,logical_not<T>>,implication<T,U>>>:std::true_type
		{
			typedef implication<implication<logical_not<U>, logical_not<T>>, implication<T, U>> claim;
		};
		
		template<class T, class U>using tautorogy_typeA = proof<implication<T, implication<U, T>>>;
		template<class T, class U, class V>using tautorogy_typeB = proof<implication<implication<T, implication<U, V>>, implication<implication<T, U>, implication<T, V>>>>;
	}
}