Progress: infix syntax, definitions

[Raph Levien]

A lot of progress, including infix syntax (using a precedence parser) and definitions. The prototype is starting to look like my current vision.

Definitions are basically just "def lhs: rhs;", and the rules for using them are quite friendly; anywhere the lhs appears in the proof, an attempt to unify it with the rhs will succeed, as the unifier will expand the definition.

 A good example of this is the proof of df-bi as a theorem. The body of the proof proves bijust (all these propositional proofs are adapted straight from Metamath), and the instances of <-> in the conclusion just expand when they match against that. pm2.53 is another example of a proof by definition expansion.

The two .gh files (test and ski) have a bunch of good examples of short proofs. Personally I find this style of proofs fairly readable even in raw source form, certainly more so than Metamath or original Ghilbert. I find that the result lines very helpful, as otherwise it's pretty easy to get lost in RPN.

The tool is still pretty rough to use, especially in error reporting. It doesn't give you a whole lot of information other than "something went wrong". Writing good error messages is an art form, and will take some work to make this really polished, but I believe the conceptual core is solid.

Of course, the prototype is still missing any concept of modules or imports/exports. I plan to dig into that deeply later, after I have some more confidence in this stuff. That said, the capabilities of the current prototype are in the same ballpark as those of Metamath.

Feedback welcome.

Raph