No type error constructing incorrect Eq proof

[higherorderco]

No type error constructing incorrect Eq proof

[VictorTaelin]

Sorry for the delay. That shouldn't be a type error because Eq<Nat>(Nat{zero})(Nat{succ(Nat{zero})}) is just the type that asserts 0 == 1. Or, in other words, it is just, literally, the "zero is one!" assertion written in the language of types. It doesn't prove anything by itself. To prove that assertion, what you need is a separate term of that type. That is, when you run formality -b sntc your_file.formality.hs, this is what you see:

[TERM]

Eq<Nat>(n0)(n1)

[TYPE]

Type

[EVAL]

Eq<Nat>(Nat{zero})(Nat{succ(Nat{zero})})

This is what you want instead:

[TERM]

X

[TYPE]

Eq<Nat>(Nat{zero})(Nat{succ(Nat{zero})})

[EVAL]

X

The first just says "Eq<Nat>(n0)(n1) describes the theorem 1 == 0", the second says "X proves the theorem 1 == 0". If you find a term X which has the type Eq<Nat>(Nat{zero})(Nat{succ(Nat{zero})}), then, and only then, you have proven that one is the same as zero, which should obviously be impossible in Formality.

Note: you can actually do this right now since Formality doesn't include certain consistency checks yet (universe polymorphism, guarded recursion). I'm working in simplifying Formality's implementation (it is down to 500 LOC, from almost 3k LOC!), here. Once that is done I'll include those checks and reason about its consistency (which should follow from Coq's consistency).

[emturner]

I'm so sorry for the delay getting back to you.

Thanks so much for taking time to explain it all! That makes a lot more sense now, within the context of what I was trying to do.

Cool! That's exciting - I'll definitely take a good look :)