Add some automation heuristics

[david-a-wheeler]

I know you already plan to add some automation. I thought I'd add this issue as a way to track that. I think automation is the only major area where mmj2 has a significant advantage for typical proof creation.

You can find mmj2's automation heuristics here: https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js In short, when automation is enabled there are certain statements it always tries, and when it detects certain patterns it uses a simple algorithm to simplify it (e.g., for numbers). This automation is within its larger set of macros.

Mario can explain them in more detail.

Obviously it'd be awesome to have a full tactics language (including support for backtracking on failure). But simple automations could go a long way. Anyway, I know you're interested in that, so I thought I'd try to capture that idea here.

[expln]

Yes, the automation heuristics is the most interesting part for me. The only reason why I still have not started working on it is that once I start, everything else will stay undone for a long period of time :)

I thought of making heuristics flexible. One of my ideas was to use Metamath itself as a language for heuristics in the following way. You define an *.mm file with many different theorems and append it to the main database as usually but then mark it as "all theorems in this file are heuristics". Then mm-lamp treats such theorems in a special way - it tries to apply them before any other "usual" theorem. Once a proof is found, these "heuristic" theorems get in-lined (usually producing few new statements) so that none of the "heuristic" theorems appears in the final proof. On the other hand, if these "heuristic" theorems are so useful, why not to add them directly to the main database. I cannot assess effectiveness of this approach myself due to lack of experience of creating proofs. And this is not easy enough to "just do it and see how it works". So what do you think, is there any chance it will work?

[david-a-wheeler]

I'm skeptical of that approach if I understand you correctly. In particular, some of the automation in mmj2 fundamentally depends on loops/recursion which aren't easily described within metamath itself (as it's an operation on the symbols).

I think a more fruitful approach would be a "tactics-like" language like Coq, HOL-Lite, Isabelle, etc. Basically, a simple language where you can define some things you can try that will produce something correct (though not always useful), and then determine if it should accept it or bail out. In the long term I'd love to see the ability to invoke, within metamath-lamp, a command to execute a complicated tactic on a selected set of statements.

I suggest talking with Mario once you get closer. He has quite a bit of experience with this sort of thing.

However, I think there are some minor tweaks that can be made to the UI that will take relatively little time & create big benefits, e.g., supporting long-press so it's useful on smartphones, making it so adding a new statement doesn't require selecting and unselecting qed, etc. I suggest working on those first, because I think metamath-lamp with a few tweaks, documentation, and some tutorial videos will be more than enought to be useful now. Metamath-lamp's ability to do multi-step backwards proofs is actually enough to do some mmj2 automations in some cases, we just need to help people understand how to use it.

[david-a-wheeler]

@digama0 (Mario Carneiro) - "how to automate proves" is a huge topic. Thoughts?

[digama0]

I agree that having a programming language in which you can write proof automation is a game-changer. It doesn't really matter what the language is, but it should be roughly Turing-complete. mmj2 used an embedded javascript scripting language, mm0 has a scheme interpreter for its metaprogramming language. Lean uses Lean, isabelle uses ML, the HOLs use ML or OCaml. Coq uses Ltac or ML.

Writing in the implementation language is also a possibility, although it is generally less flexible because you need to keep updating the proof assistant with any automation changes and it can get quite heavy. But it saves you the trouble of figuring out how to run or interface with a scripting language.

Besides this, mmj2 doesn't actually have that much in the way of bespoke automation, except for the numeric normalizer. The majority of the automation work is a very simple heuristic: apply anything that can be applied, and don't backtrack. Blacklist a bunch of theorems which are not a good idea to apply eagerly in this way. This is especially good for "closure" style theorems (aka typing constraints), since these tend to be very syntax-directed.

[david-a-wheeler]

In the very short term I think there are a few tweaks to the metamath-lamp UI that should happen first, to fix a few oddities. It might also be good to give a little time to stew and think about it.

It might be that a useful "next step" would be to try hand-implement a little of mmj2's automation. As Mario notes, it's not sophisticated, but it's real and would give a sense of the kind of operations that it might be useful for an automation tool to do. That might be useful to get an idea of what might be common in such languages, and would simultaneously provide some useful function in the interim.