README

FOL Idris

I'm definitely not the first person to do this, but I had an idea a while back for correct by construction FOL terms and formulas in a dependently typed language, and finally got around to playing with it, and it is very cool. The idea is I have a type Term representing a term in some first order language, and a type Formula representing a formula in that language. Then, through some careful applications of dependent types, it is only possible to construct well-formed formulas. For example, suppose the signature N contains a binary function symbol Plus, a nullary function symbol (i.e. constant symbol) Zero, and a unary function symbol S. Then you can construct the term Plus(Zero, S(Zero)), but Plus(S(Zero(Zero), Zero)) doesn't type check.

Where things start to get really cool is that you can do the same thing with a proof object. So Proof is a type representing a proof, but only correct proofs can even be constructed. Typically you'd have representations of terms, formulas, and proofs, but then would have to write code to verify them; verify that the proof is correct and that the terms and formulas are well formed. You can also very easily play with different logics by just tweaking the constructors of Proof. For example, by removing the constructor Contra from Proof, and adding some other constructors that become necessary, you'd have an intuitionist logic. As it stands, the rules and connectives are extremely minimal, with derived rules existing as proofs in the Logic module.

I don't really have a goal with this project, and have just been working on it for fun. There's tons more work that can be done. As it stands, this is far less capable/usable than my last proof assistant, but I think it's pretty cool. It's pretty similar to lisa, but with a more trusted kernel and far less usability.

I recently wrote a blog post explaining in an overly self-indulgent level of detail how all this works.

TODOs

TODO elimBinder

elimBinder should probably actually take an index to eliminate rather than just always eliminating the outermost index.

TODO Improve experience working with equality

EqE is extremely difficult to use right now, primarily because Idris can't tell that elimBinder t (inc s) = s. That and several other lemmas regarding inc, sub, and elimBinder would likely be extremely helpful.

TODO Consider reworking Hyp

If Hyp : In phi c -> Proof c phi, then maybe much more data surrounding c could be erased, making things more ergonomic, as well as making Weaken a theorem, and allowing for easily proving that if c and c' are permutations of each other, then there exists a Proof c phi if and only if Proof c' phi, which currently would be an absolute nightmare to prove. This could make using Hyp quite a bit more awkward.

TODO Parser?

This is a long term goal. Making a parser would be quite a challenge, since it also kind of has to come with a proof of correctness in order to work at all with how strict the types are.

TODO Pretty-Printer

This is much more doable, and would also help quite a bit. It would also be very nice if I could hook it into the repl, so that Idris uses the pretty-printer in holes. Right now, holes are quite difficult to read, since they don't show any abbreviations or anything.

TODO Unifier

Some sort of unification implementation would make working with equality a lot easier.