On Mon, Feb 13, 2023, 5:14 PM Igor Ieskov <[email protected]> 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/4c913c14-d74b-4457-a6af-f6fd5dcc5e13n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4c913c14-d74b-4457-a6af-f6fd5dcc5e13n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAMZ%3Dzj4hLx0%3DqeSfSUqzP8aQH%3Di0Li6FDrt7T%2B2zMzyAZ8w-mw%40mail.gmail.com.
