Hi all, I have released version 7 of metamath-lamp with bug fixes and a few new features.
https://expln.github.io/lamp/v7/index.html Here is a demo https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view I used the text-to-speech function of my video editor to add voice explanations in the demo. It might sound a bit unusual, but believe me this is much better than listening to what I retrieve when recording my own voice. In the demo I used the “my-editor-state.json” set of statements provided by Thierry in one of the posts above (on Jan 11 2023, if anyone wants to find it quickly). Thank you Thierry for providing “my-editor-state.json”. It allowed me to discover some use cases I was not aware of before and helped me a lot in improving mm-lamp. I also saved it in the source code and implemented a few tests based on it - https://github.com/expln/metamath-lamp/blob/4b25515acb8174086cd970d1b10cc4a26821dbba/src/metamath/test/resources/int-test-data/restore-missing-disjoints/editor-initial-state.json Few things I want to mention: - I edited the demo video and cut out some long running phases of unification and bottom-up proving for the demo to be shorter. So in reality mm-lamp might be slower. - While recording the demo I realized that exporting local variables (this is a new feature explained at the end of the demo) might not work well if such variables are not used explicitly in the statement being exported or its hypotheses but are used in its proof. I have not tried to reproduce this bug but I see in the code that this may happen. I am going to fix this in a future version. - I forgot to update some tooltips with hotkeys. Here are the correct hotkeys: 1) to start editing a statement, variables or disjoints - left click it; 2) to save the changes - press Enter; 3) to start a new line in variables or disjoints text fields - press Shift Enter. If anyone sees any mistakes in the current design or finds any issues or bugs, please feel free to let me know. Any feedback is appreciated. For issues and bugs it’s probably better to use the “Issues” section of the repository https://github.com/expln/metamath-lamp/issues David, I walked through the mmj2 tutorial. Please find some my thoughts below: 1) currently mm-lamp doesn’t allow adding comments. I am going to implement this. 2) undo/redo is also not supported in mm-lamp. Most probably I will not be able to implement this feature by storing the editor state in the URL as you mentioned because internal representation of the editor state is actually more than we may see in the local storage. I could store editor states to the local storage after each modification (I mean keeping all previous versions of editor states). But then I am limited by the available amount of the local storage which is usually not too big. I keep thinking on how I can implement this feature. 3) mmj2 can keep few identical statements and mm-lamp cannot. I cannot change this because this lies in the core - it allows me to simplify some parts of the code. Please let me know if this is a vital or very handy part of creating proofs. If it is needed to keep few possible proofs for a single statement then I will try to implement multiple justifications for a single statement. 4) Renumbering of statements, loading existing proofs - I am going to implement this. 5) mm-lamp cannot automatically prove “|- ( ; 9 5 + 1 ) = ; 9 6”. I hope this will be resolved once I start adding heuristics. 6) Search capabilities of mmj2 are profound, I need some time to learn this and figure out what I can steal. Best regards, Igor On Tuesday, February 14, 2023 at 12:14:18 AM UTC+1 Igor Ieskov wrote: > > *>One broad suggestion: Could you give it a short & less generic > name,>since there are other Metamath proof assistants?* > > That’s done! The new name is metamath-lamp “Lite Assistant for Metamath > Proofs”. > I renamed the repository accordingly: > https://github.com/expln/metamath-lamp > I guess I need to create a pull request to make corresponding changes on > https://us.metamath.org/other.html ? I will try after sending this email. > > > > > *> 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 > <https://github.com/expln/metamath-proof-assistant> (MIT license).* > > Good point. I will add such a link. Yes, MIT license, but the new URL is > https://github.com/expln/metamath-lamp > > > *> But I think trying to answer "why can't I automate this in general" is > best delayed for a long time.* > > I thought on this, and finally concluded that this is not even a “nice to > have” but this is “must have” feature. The reasoning is as follows. Users > will ask me “why this doesn’t unify” or “why this cannot be proved > automatically”. Currently the only solution is to reproduce the case > locally and debug. But this is too hard because I debug by small steps and > I don’t see a bigger picture. Thus I conclude that I need some kind of log > of main events to understand faster what’s going on. So I feel like I > cannot delay development of this feature. > > > *> 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 don’t have enough experience to figure out what are the common cases. I > need to spend some time practicing in creating proofs first. And this is > related to the tutorial topic (please see my response on tutorial topic > below). > > > > > > *> 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 > <https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js>* > > Thanks for the reference. I will check and return back to you and Mario > with questions when I will be closer to writing heuristics. > > > *> Even a few small automations could make a big improvement in usability.* > > If anyone sees such small automations please let me know. I have > experience in writing code which manipulates metamath statements, but this > adds almost nothing to my ability to create actual proofs, so such kind of > small improvements are not visible to me at the moment. > > > > *> > b) highlighting syntax subtrees by clicking them> To simplify > replacing them, I guess?* > > Yes, but not only. This should also make easier to copy subexpressions. > Currently unexperienced users like me have to count parentheses which is > too tedious. > > > *> 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).* > > That’s doable. I will add this to my todo list and implement in some time. > > > > > > > *> 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 > <https://www.youtube.com/watch?v=87mnU1ckbI0>> The text is here:> > https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial > <https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial>* > > Yeah, I watched it few times and will watch one more time with pleasure. > Moreover, I have now more understanding of the processes under the hood, so > I am able to catch more details. (When I watched it for the first time few > years ago it was like magic to me :) ) > > > > *> 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.* > > Of course! This is a great opportunity for me to get more experience in > creating proofs and simultaneously help other metamath newcomers to get > acquainted with it. If you can provide those mmp files from > us.metamath.org, and additionally some json file which will work as a > table of content for the tutorial, then I will parse them and represent in > my app. Such an interactive tutorial could be a good starting point for > beginners. So, once you think my app is ready to become a tutorial for > Metamath we may start a separate email thread and discuss details of > implementation of such tutorial. Currently I think the tool requires more > testing, because I implemented some algorithms by intuition and I have not > analyzed everything with mathematical rigor. > > > *> Nevermind, I see you can already rename statements* > > In the previous versions it was not “true” renaming. Justifications were > not updated. But in the v6 renaming of statements updates justifications. > > > *> below I tell what I've come up with, in yamma.* > > Thanks, Glauco, for the ideas. I checked your test cases and I see similar > validations may be implemented in metamath-lamp too. > > > *> 'Working Var unification error: the working var &W2 should be replaced > with the following subformula, containing itself ( &W2 -> ph )'* > > Could you please explain why a working var cannot be replaced by a > subformula containing itself? It is possible in mm-lamp and I don’t see any > reason why it should not be possible. > > > > *> Hope this can give you some ideas.* > > Definitely! Thank you, Glauco! > > > > I implemented few new features and moved my tool to a new URL - > https://expln.github.io/lamp/latest/index.html > > 1) Exit edit mode on ESC, save changes on Enter on all text fields in the > editor. (To start a new line in a multiline text editor press Shift+Enter, > this is not mentioned on tooltips, but I will add it in the next versions ) > 2) Shorter names for statements and “true” renaming of statements when > justifications are also updated with the new statement label. > 3) In substitution dialog, now it is possible to see hints why some > substitutions are invalid. > 4) A new parameter in bottom-up proofs - “Derive from root statements”. It > was present in v5 and it was always “true”. But it significantly decreases > performance and I expect it to be not necessary in many cases. So I added > it to the bottom-up dialog and set its default value to false. Users will > be able to decide if they want to use it or not. I understand that I have > to provide here more details on how bottom-up exactly works in mm-lamp and > in particular what the new parameter does. But unfortunately I don’t have > time right now. I will write this a bit later. > > > The demo video below demonstrates #3 feature and the use case when #4 > feature could be useful. > > > https://drive.google.com/file/d/1nIigII46Z8l1xk9VRWlPT9_N-VcNTh2R/view?usp=sharing > > Current latest version is https://expln.github.io/lamp/v6/index.html > > - > Igor > > > > On Sunday, February 12, 2023 at 9:08:43 PM UTC+1 Igor Ieskov wrote: > >> Sorry, I missed one question which could be easily answered: >> >> *> I don't see how to create hypothesis statements in the tool* >> >> This is implemented. Each statement is prefixed with an upper case >> letter either P (provable) or H (hypothesis). Alt-left-click allows to >> change it. This is demonstrated at 5:49 in this video - >> https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view >> >> - >> Igor >> >> On Sunday, February 12, 2023 at 1:12:24 AM UTC+1 Glauco wrote: >> >>> On 2/11/23 07:39, David A. Wheeler wrote: >>> >>> > 1) I think one of the "key" missing things is ability to help a user >>> > to understand why a statement doesn't unify. >>> >>> I have only an approximate idea of whether this is easy or hard, but I >>> will say that even modest improvements here would be helpful. For >>> example, it may be easier to detect particular cases than every possible >>> "way" a statement can't unify. One of the more time consuming things >>> that happens to me when using mmj2 is that a unification which I >>> expected to happen doesn't, and then I need to look at (sometimes long) >>> expressions to figure out what parts don't match. >>> >>> Hi Igor, >>> >>> below I tell what I've come up with, in yamma. >>> >>> First, I'll write the short story, then I'll elaborate a bit about the >>> theory and the challenges. >>> >>> The short story: >>> >>> yamma has two kinds of diagnostic messages for unification failure. >>> >>> >>> The first kind of message, suggests how to fix the unification error. >>> Two examples: >>> >>> "Unification error: referenced statement is '|- ph' but it was expected >>> to be '|- ( ps -> ph )'" >>> >>> (see >>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329 >>> >>> for the full unit test) >>> >>> or >>> >>> "Unification error: statement is '|- ch' but it was expected to be '|- ( >>> &W1 <-> &W2 )'" >>> >>> (see >>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498 >>> >>> for the full unit test) >>> >>> The first example is a diagnostic highlighted on the hyp label, >>> referencing a formula that doesn't match what's expected. >>> The second example is a diagnostic on the statement itself (the 'main' >>> formula cannot be unified with what's expected by the step label) >>> >>> >>> The second kind of messages, involves substitution of working vars. >>> Example: >>> >>> 'Working Var unification error: the working var &W2 should be replaced >>> with the following subformula, containing itself ( &W2 -> ph )' >>> >>> (see >>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420 >>> >>> for the full unit test) >>> >>> >>> >>> Now, a bit of 'theory' (as far as I understand it) >>> >>> There are two categories of unification: >>> >>> 1. single statement >>> >>> 2. multiple statements >>> >>> With single statement unification, you're trying to find the mgu for >>> both the logical variables (the theory's variables) and the (possible) >>> working variables. You could use a Martelli Montanari algorithm on the >>> whole proof, and it will be clean and "secure", but you'll not get a >>> super-informative error message. >>> That's why, for the single statement unification, I've gone for a >>> 'custom' approach, that allows for some better error message. >>> >>> With multiple statement unification, you're trying to find the mgu for >>> all the working vars in the proof (because logical variables have already >>> been 'substituted'). >>> Here, I've gone with the 'pure' Martelli Montanari algorithm. >>> It can fail either >>> - with a 'clash fail' error (for metamath, it means two constants don't >>> match; something like '->' was expected, but you have '<->' ) >>> or >>> - with an 'occur check fail' (a working var should be replaced with a >>> formula strictly containing itself) >>> >>> Hope this can give you some ideas. >>> >>> >> -- 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/af537ed1-5a8c-4889-bbfa-263eee7c85ean%40googlegroups.com.
