怀疑C++不能用于自动化定理证明

[NanaGlutamate]

由于C++并不会检查requires是否在任何条件下都满足，而只会检查对于某个特定的实例化是否满足，C++可能并不能用来做自动定理证明。
例如，甚至可以证明任何自然数都是0：

template <Nat::isNat N>
struct EveryNumberIsZero : Prop {
    constexpr Eq<N, Nat::Zero>
        operator() () {
        using namespace Nat;
        using namespace Prover;

        return rfl<Nat::Zero>();
    }
};

int main() {
    auto proof = EveryNumberIsZero<Zero>()();
    return 0;
}

表面上看，EveryNumberIsZero确实能对任何一个自然数实例化一个Eq<N, Nat::Zero>

[fogsong233]

有pattern matching的语言会要求每个分支都要检查的，这里面这个isNat实现只是约束了输入，但是没办法给到代码里面这个类型就是自然数，必须满足所有的分支，所以只能自己约束匹配到所有可能的模式。
其实也可以去除concept，直接要求完全匹配类型，事实上这样就没有问题了，有了concept就会造成这样的情况。

[fogsong233]

但是因为没有类型空间，所以我是引入了prop这个基类，然后concept方便判断命题，不然每个prop都要模式匹配，而如果有类型空间，那么concept就是不必的