# Proofs Using C++ Compilation

About a month ago, I realized I could use the Curry-Howard Correspondence to formulate a simple proof assistant using C++’s type system. Of course, the C++ type system is pretty rudimentary, so proving things using it is an uphill battle, but I was able to formulate propositional logic. One major shortcoming is that C++ can’t reason about inductive types, so we have to add axioms to properly reason about logical connectives.

Here is `logic.h`:

``````#include <functional>

// Ignore return types so we can form axioms
#pragma GCC diagnostic ignored "-Wreturn-type"

// False is a proposition with no proof,
// so it has no constructors
class False { False () = delete; };

// Modus ponens is just function application
template<typename P, typename Q>
using Implies = std::function<Q(P)>;

// explosion: False -> P
template<typename P>
P explosion (False f) {}

template<typename P>
using Not = Implies<P, False>;

// left: P /\ Q -> P
// right: P /\ Q -> Q
// conj: P -> Q -> P /\ Q
template<typename P_, typename Q_>
class And {
P_ p;
Q_ q;
And<P_, Q_> (P_ p, Q_ q) : p(p), q(q) {}
public:
template<typename P, typename Q>
friend P left (And<P, Q> a);
template<typename P, typename Q>
friend Q right (And<P, Q> a);
template<typename P, typename Q>
friend Implies<Q, And<P, Q>> conj (P p);
};

template<typename P, typename Q>
P left (And<P, Q> a) { return a.p; }
template<typename P, typename Q>
Q right (And<P, Q> a) { return a.q; }
template<typename P, typename Q>
Implies<Q, And<P, Q>> conj (P p) {
return [p] (Q q) {
return And<P, Q>(p, q);
};
}

// inl: P -> P \/ Q
// inr: Q -> P \/ Q
// confluence: P \/ Q -> (P -> R) -> (Q -> R) -> R
template<typename P_, typename Q_>
class Or {
Or<P_, Q_> () {};
public:
template<typename P, typename Q>
friend Or<P, Q> inl (P p);
template<typename P, typename Q>
friend Or<P, Q> inr (Q q);
};
template<typename P, typename Q>
Or<P, Q> inl (P p) {}
template<typename P, typename Q>
Or<P, Q> inr (Q q) {}

template<typename P, typename Q, typename R>
Implies<Implies<P, R>,
Implies<Implies<Q, R>,
R>> confluence (Or<P, Q> pq) {}

#pragma GCC diagnostic error "-Wreturn-type"
``````

And here is a demonstration of two proofs:

``````#include "logic.h"

class A { A () = delete; };
class B { B () = delete; };
class C { C () = delete; };

template<typename P, typename Q>
auto constrapositive =
[] (Implies<P, Q> pq) {
return [pq] (Not<Q> nq) {
return [pq, nq] (P p) {
return nq(pq(p));
};
};
};

Implies<Implies<A, B>, Implies<Not<B>, Not<A>>>
contrapositive_check = constrapositive<A, B>;

template<typename P, typename Q, typename R>
auto or_assoc =
[] (Or<P, Or<Q, R>> pqr) {
return confluence<P, Or<Q, R>, Or<Or<P, Q>, R>>
(pqr)
([] (P p) { return inl<Or<P, Q>, R>(inl<P, Q>(p)); })
([] (Or<Q, R> qr) {
return confluence<Q, R, Or<Or<P, Q>, R>>
(qr)
([] (Q q) { return inl<Or<P, Q>, R>(inr<P, Q>(q)); })
([] (R r) { return inr<Or<P, Q>, R>(r); });
});
};

// This is actually only one direction of Or associativity
Implies<Or<A, Or<B, C>>, Or<Or<A, B>, C>>
or_assoc_check = or_assoc<A, B, C>;

int main () {}
``````

The proofs are checked at compile time by way of type checking.

Some things to notice: First, template definitions are not fully type-checked, so we have to use instantiations like `or_assoc_check` to force type-checking using “concrete placeholders.” Second, C++’s type inference is not strong enough to deduce all intermediate types, so we often have to specify them ourselves (e.g. writing `inr<P, Q>(p)` instead of `inr(p)`).

I’m not sure if first order logic can be formulated with C++ in this way. Note that the templating system is Turing-complete, so it is possible to write a full proof assistant in it, but I’m only curious about reusing `g++`’s type checking system to also check proofs.

15 December 2022