3 ms·
Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of
by tel 7y ago
Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of proofs relate to their theorems.
This isn't really a problem per se, but instead an invitation to look into, say, Agda to see that side of things, too.
- deleted 7y ago[deleted]
- zozbot234 7y agoAgda just uses proof terms directly - you could do that in Coq and Lean as well. It's a bit of a bummer though that neither Coq nor Lean have a currently-maintained declarative mode ala Mizar/Isar. The former C-zar included in older Coq versions (aka Mathematical Proof Mode) was especially nifty, albeit not totally free from bugs. (One other approach is to generate a "declarative", human-readable version of the proof directly from the proof term. Very old versions of Coq (6.x series) and IIRC even Agda (1.x) could essentially do this. Declarative proof mode integrates better with complex tactics however - proof terms can sometimes get a bit weird.)
- tel 7y agoI agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them. In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.