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