(Replying to myself) Nevermind, I see you can already rename statements in <https://github.com/expln/metamath-proof-assistant> / <https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html>! You clearly demo'ed it too.
When renaming, I *do* wish that either RETURN or ESCAPE would save the name. I'd prefer shorter default statement names, because I hope to eventually see them & their justification names on screen, but clearly the functionality is there already. I don't see how to create hypothesis statements in the tool, that's probably more important if it's not already there (I didn't see how to do that). I recommend not using "h" as a prefix to indicate that (mmj2 does that, but I don't think that should be repeated). I think a button that sets/unsets a statement's "hypothesis" flag would be great, and then just have a special onscreen marker for hypotheses. --- David A. Wheeler > On Feb 11, 2023, at 10:39 AM, David A. Wheeler <[email protected]> wrote: > >> >> On Feb 11, 2023, at 5:00 AM, Igor Ieskov <[email protected]> wrote: >> >> Thanks David! > > You're very welcome! This version really has come a long way: > https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html > > One broad suggestion: Could you give it a short & less generic name, > since there are other Metamath proof assistants? > Naming is hard, but a short unique name will make it easier to discuss & find. > And I think this is *very* worthy of discussion & being found. > > You might want to include, on the screen or an "about" option, a link to the > GitHub repo for the code (so people can review/contribute). I understand that > is currently: > https://github.com/expln/metamath-proof-assistant (MIT license). > > >>>>> What are the "key" things you think it's missing, especially in >>>>> comparison to mmj2? >> >> 1) I think one of the "key" missing things is ability to help a user to >> understand why a statement doesn't unify. As also Thierry noted earlier, >> currently the app shows only this message "Justification cannot be >> determined automatically". Or another message is possible too >> "Justification for this statement is incorrect". But the app doesn't explain >> what is the reason. That's my next goal. I don't see any trivial or simple >> solution, so it may take some time to implement. > > Whoa, that's a very high bar. > > I suggest working on other things first & getting back to that later (if > ever). In particular, if you add tactics & some automation, the reason for > that answer will change, so I suggest working on some predefined > tactics/heuristics first. > > If your intent is to just determine why "this statement doesn't unify with > this other specific statement", you could try to find the longest match & > identify where it finally fails. That seems doable. You could even walk > across the database & report the longest incomplete match, but I don't know > if it'd be helpful; it'd probably report some very general but unrelated > theorems. But I think trying to answer "why can't I automate this in general" > is best delayed for a long time. I can be wrong, of course :-). > > >> 2) Another, although maybe not a "key" thing, is to have predefined >> "tactics" to prove some common cases, for example, prove by induction or >> prove by case analysis. This not necessarily has to result in complete ready >> proofs, but it may create another new statements which help a user to move >> in the desired direction (similar to what I saw in Coq proof assistant). >> >> 3) As you mentioned mmj2 uses some useful heuristics. I also would like to >> add heuristics to improve automatic proof search. > > You could easily combine 2 & 3. Just create a first tactic called "auto" or > similar that tries to apply a few simple rules to automatically prove a few > simple/common cases. I would devise them so that eventually tactics could be > called internally (e.g., by other tactics & maybe even a scripting language). > Then make it so a user can select a tactic to a selected set of statements, > and you're off. > > mmj2 has a few simple heuristics that it applies automatically its default > configuration. > You could make them either fully automatic or the basis for an "auto" tactic. > Code here > (I think Mario wrote more or all of this): >> https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js > Don't feel you have to use it exactly, and it might be better split into > different > tactics (mmj2 doesn't really support multiple different tactics, a big > weakness of it). > > Even a few small automations could make a big improvement in usability. > > >> 4) Finally, not key at all, but what should improve user experience and may >> be achieved relatively easy (implementation still may require a lot of time >> but at least everything is clear for me in terms of how to implement): > > User experience improvements can make a big difference. I think that's more > key than you realize, and I bet a few easy ones would make all the difference. > >> a) exit edit mode by pressing ESC key > > Yes! Existing with the ESC key would be a big help. > > >> b) highlighting syntax subtrees by clicking them > > To simplify replacing them, I guess? > >> c) graphical visualization of justifications > > Graphical visualization of justifications is probably not very helpful, they > tend to be a mess once they become non-trivial. > > I would instead prefer an optional simple column, to the left of the > statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS > (similar to how mmj2 works now). I'd also make the default statement names > shorter (so that justification text takes less space), e.g., shorten "stmt" > to "s" or some such. In the future, as a bonus, it'd be nice to be able to > rename step names - they don't matter for the final proof, but it might make > proving things easier. > >> d) proof explorer for the loaded *.mm file > > A nice-to-have, but I think you can delay that. The metamath website already > provides a proof explorer that people can use. > You could provide a link that opens a new tab to us.metamath.org and get a > lot of the way there. > >> e) sharing proofs via URLs (as you suggested and I find this very useful for >> collaboration). I want to implement this after some time, because when I >> implement it, I will have to support backward compatibility between >> different versions, so I want to wait when internal representation of the >> editor state becomes stable (no frequent changes in the code). > > Cool, glad you liked the idea. The rationale for delay makes sense, though I > can't wait to use it :-). Once you implement 4(e), undo/redo becomes trivial > (you can let the browser do it!). I suspect there's no need to compress it, > and you'll get decent results from > encodeURIComponent(JSON.stringify(your_representation_here)). Of course, > there's the question of what your_representation_here is :-). Just don't > stick the whole MM database in there :-). > >> Currently my plan is to work on the 1st and 4th items. > > As I said, I'd delay #1 (that is likely to be *hard* unless you really back > off on your plans). > I'd love to see small increments on #4, and a little automation (#2/3). > > Regarding user improvements, most people will want to load the current set.mm > & iset.mm, > so making that easier would be helpful. If there was an easy way to download > it straight > from the web, that might make getting started easier. I could easily configure > us.metamath.org's CORS settings so the script could always download .mm files > from us.metamath.org > no matter where it started from. > > You might want to walk through the mmj2 tutorial to see what ideas are > worth stealing. I recorded it on Youtube here: > https://www.youtube.com/watch?v=87mnU1ckbI0 > The text is here: > https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial > > Once you're further along, I'd be happy to work with you to create a tutorial > if you'd like. I'd probably want to build on the same examples from the mmj2 > tutorial. > > It's your project, so take my comments with a bucket of salt. > I really do think this is neat though! > > --- David A. Wheeler > > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/C2593B77-C1F2-45F5-8523-E347EEF5C569%40dwheeler.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E3F7119A-6226-4A65-BA22-56C10B402CFE%40dwheeler.com.
