Thanks David! *>>> 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. 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. 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): a) exit edit mode by pressing ESC key b) highlighting syntax subtrees by clicking them c) graphical visualization of justifications d) proof explorer for the loaded *.mm file 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). Currently my plan is to work on the 1st and 4th items. Best regards, Igor On Saturday, February 11, 2023 at 12:45:31 AM UTC+1 David A. Wheeler wrote: > > > On Feb 10, 2023, at 4:56 PM, Igor Ieskov <[email protected]> wrote: > > > > Hi all, > > > > I implemented bottom-up proofs in v5. In order to start proving > bottom-up it is necessary to select one statement and click "unify" button. > It is not very fast, but for not big statements it works well. > > > > Demo video - > https://drive.google.com/file/d/1cjJnvlNGACAmlEnlvxzInqmIqE5dl-0Z/view?usp=sharing > > > In the demo video I am trying to repeat (as close as possible) proof > steps from this mmj2 tutorial > https://www.youtube.com/watch?v=vE3v175cMKM&t=217s > > > > https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html > > WOW! That is *so* cool. That looks like enough functionality that it could > be seriously used, > though I'm sure there are many things that could be added. > > The fact that there's no "install" step required for this prover is > especially neat. > That does reduce a barrier to getting started. > The unification may not be fast, but the demo suggests it's okay. > I suspect there are easy tricks that could make it faster in JavaScript, > and a WebAssembly routine could eventually be added if that becomes a true > bottleneck. > > What are the "key" things you think it's missing, especially in comparison > to mmj2? > > --- David A. Wheeler > > > > > > Best regards, > > Igor > > > > On Monday, January 23, 2023 at 9:51:41 AM UTC+1 Igor Ieskov wrote: > > Hi all, > > > > I made few changes in v4: > > - short names for work variables (&Cn, &Sn, ...); > > - variables are highlighted with different colors depending on their > types (only in the editor tab); > > - automatic detection of missing disjoint variable groups when applying > a substitution (so now substitutions are easier to do for users in the > cases like the one with spcgv described earlier in this thread); > > > > Work variable names and colors are configurable on the settings tab. > > > > https://igorocky.github.io/mm-proof-assistant/demo/v4/index.html > > > > Best regards, > > Igor > > > > On Friday, January 13, 2023 at 10:59:53 AM UTC+1 Igor Ieskov wrote: > > >>> However It looks like for the former, in the example we use, an > additional burden is placed on the user to manually add new DV for UI > substitutions. > > > > That's nice to know that my implementation of disjoint checks in the > proof assistant is not wrong. Yes, my intent was to not allow (at least to > decrease possibility of) creating valid proofs which will fail in > metamath.exe because of disjoints or similar kind of issues (my experience > in creating MM proofs is very small, so I cannot imagine what kind of > issues may arise). So as the very first version I implemented it in the > strictest way I could. Now, having your feedback, I will think on how to > make it more user friendly. My current ideas what I want to try: > > > > a) in the substitution dialog, allow users to temporarily disable > disjoints (all at once or only some of them) to see how this affects > results; > > b) add missing disjoints automatically if this helps to make > substitution valid (once a user permits this); > > c) try to handle automatically simple use cases as in the example with > class1->x; > > d) something similar to temporarily disabling disjoints but in cases > when "justification cannot be found automatically" to make it easier to > understand how disjoints affect unification; > > > > > > > > > > Best regards, > > Igor > > > > On Friday, January 13, 2023 at 12:08:31 AM UTC+1 Thierry Arnoux wrote: > > Ok, one more quick remark (now that I know how to use substitutions!): > > > > Currently, the tool blocks if two steps are the same. One has to > manually remove the step, and update any justification using that step. > > > > MMJ2 automatically merged them, IIRC. It would be very nice to have the > same mechanism (automatically updating corresponding justifications too, of > course!) > > > > > > > > On 12/01/2023 22:58, Thierry Arnoux wrote: > >> Hi Igor, > >> > >> Thanks for all answers, and especially the change for the single click! > >> > >> I understand very well not everything is simple, and you have to move > on step by step. > >> > >> Concerning the substitution function: thanks to your explanations, I > could make it work in cases which previously blocked! > >> > >> > >> > >> I think here I would make a difference between the UI substitution > function, which is here to help the user, and the substitutions checked > when applying theorems. > >> > >> The later requires to follow distinct variables requirement, and it's > very nice that your proof assistants follows with that along the way (that > is a weak point of MMJ2 in my opinion, as it seems to only worry about > disjoint variables after the whole proof is complete, and sometimes miss > some). > >> > >> However It looks like for the former, in the example we use, an > additional burden is placed on the user to manually add new DV for UI > substitutions. Actually, I think ideally the UI would instead help the user > and automatically turn the DV restriction from "setvar1,wff4,class2" into > "x,wff4,class2". Indeed the first one disappears (since setvar1 gets > replaced), and the second one is the same DV where "setvar1" has been > substituted by "x". > >> > >> Of course it's not just simple substitutions, if a more complex > substitution is done, the UI would have to all all variables to the new DV > restrictions... so it's probably easier said than done - but that would be > another great feature. > >> > >> Keep it up! > >> > >> _ > >> Thierry > >> > >> > >> > >> On 11/01/2023 21:42, Igor Ieskov wrote: > >>> Hi Thierry, > >>> > >>> And next follows the most difficult part of my response (at least for > me) :) > >>> >>> Your examples works, but in many cases I do not manage to replace > metavariables. For example in "spcgv", when I want to replace "setvar1" by > e.g. "x", or in "brab2a" when I want to replace "class1" by anything. > >>> > >>> If I am getting you correctly, you started with an empty page, read > all the set.mm, added “spcgv” by searching it by label. As a result > you’ve got the state as follows: > >>> > >>> Variables: > >>> > >>> var1 setvar setvar1 > >>> > >>> var2 class class2 > >>> > >>> var3 wff wff3 > >>> > >>> var4 wff wff4 > >>> > >>> var5 class class5 > >>> > >>> Disjoints: > >>> > >>> setvar1,wff4,class2 > >>> > >>> stmt1-spcgv.11: |- ( setvar1 = class2 -> ( wff3 <-> wff4 ) ) > >>> > >>> stmt1:|- ( class2 e. class5 -> ( A. setvar1 wff3 -> wff4 ) ) > >>> > >>> > >>> Then you tried to replace setvar1 with x and you’ve got “No > substitution can be extracted from the provided expressions.” > >>> > >>> > >>> In that case it behaves exactly as I programmed it, though I am not > sure if this is correct as for a proof assistant. And I need your and > others experienced metamath developers help to verify this. This case > doesn’t work because of disjoints. The Metamath book explains how to check > disjoints when we are verifying a proof, but I have not found any > explanation of how to check disjoints in a proof assistant (or maybe I have > not read till that place in the book or skipped it unintentionally :) ) So > I came up with the following rules myself. When you provide “Replace what” > = [some sequence of active symbols] and “Replace with” = [another sequence > of active symbols], the program searches for all possible substitutions by > means of which we can get from [some sequence of active symbols] to > [another sequence of active symbols]. In your example there is only one > possible substitution setvar1 -> [x]. Then the program adds all other > active variables to this substitution replacing them by themselves. So as a > result we have such substitution: > >>> > >>> setvar1 -> [x] > >>> > >>> x -> [x] > >>> > >>> ph -> [ph] > >>> > >>> class2 -> [class2] > >>> > >>> … and so on for all other variables defined in set.mm and all the > work variables. > >>> > >>> I introduced this by analogy of applying substitutions during proof > verification, when we have to apply a substitution simultaneously for all > the variables in the assertion used in the proof step. > >>> > >>> Next the program checks disjoints for this substitution. setvar1 > results in [x] (an expression consisting of only one symbol) and class2 > results in [class2] (also an expression consisting of only one symbol). > Then similarly to the checks in proofs: > >>> > >>> • “the two expressions must have no variables in common”: [x] and > [class2] have no common variables - this is passed. > >>> > >>> • “each possible pair of variables, one from each expression, must > exist in an active $d statement …”, i.e. x and class2 must be in a disjoin > group - this fails. So the entire substitution is considered invalid and > the programs shows “No substitution can be extracted from the provided > expressions.” > >>> > >>> This is possible to fix by adding a disjoint “x,wff4,class2”, so > you’ll end up with two disjoints: > >>> > >>> Disjoints: > >>> > >>> setvar1,wff4,class2 > >>> > >>> x,wff4,class2 > >>> > >>> Then the replacement should work. > >>> > >>> Please let me know if this is what is expected from a proof assistant. > If this is correct behavior, then I will consider adding some messages to > the ui explaining why no substitution can be found or even adding missing > disjoints automatically. > >>> > >>> > >>> Best regards, > >>> > >>> Igor > >>> > >>> > >>> > >>> On Wednesday, January 11, 2023 at 2:44:54 PM UTC+1 Thierry Arnoux > wrote: > >>> Hi Igor, > >>> > >>> Ok, let me give you here some quick and random feedback: > >>> > >>> Your examples works, but in many cases I do not manage to replace > metavariables. For example in "spcgv", when I want to replace "setvar1" by > e.g. "x", or in "brab2a" when I want to replace "class1" by anything. > >>> Every time I get a message "No substitution can be extracted from the > provided expressions." How can I deal with that? > >>> > >>> It's possible to edit a step's formula using ALT-left click, why not a > simple click? (that's why I naturally tried first, then I saw the > tooltip...) > >>> > >>> If when creating a new step I change my mind, it seems there is no way > out of actually creating the step and then deleting it. I end up writing > some dummy, and then deleting the step. It would be nice if e.g. just ESC > would get you out of the step edition mode. > >>> > >>> When "Justification cannot be determined automatically", it would be > nice to find out what fails: was an unification found, but distinct > variables conditions were missing, or was a unification found, but no > matching for (such and such) hypothesis, etc... > >>> > >>> Of course more automation would be nice... > >>> > >>> > >>> > >>> > >>> > >>> On 06/01/2023 19:17, Igor Ieskov wrote: > >>>> I fixed few bugs and moved my proof assistant to a new URL - > https://igorocky.github.io/mm-proof-assistant/demo/latest/index.html > >>>> > >>>> This URL will always redirect to the latest version of the proof > assistant ( to > https://igorocky.github.io/mm-proof-assistant/demo/vN/index.html ) > >>>> > >>>> Best regards, > >>>> > >>>> Igor > >>>> > >>>> > >>>> On Friday, January 6, 2023 at 1:14:14 AM UTC+1 Igor Ieskov wrote: > >>>> Thanks Glauco! > >>>> > >>>> Best regards, > >>>> > >>>> Igor > >>>> > >>>> > >>>> On Friday, January 6, 2023 at 1:07:57 AM UTC+1 Igor Ieskov wrote: > >>>> Thanks Antony and David for your feedback! > >>>> > >>>> > >>>> "Who's it targeted at?" > >>>> > >>>> At the moment I don’t have any particular long term plans for this > project. I started it just out of curiosity, Metamath seemed very simple > and I wanted to try to automate proofs. When I realized that I cannot > achieve desired level of automation, I started watching what existing > solutions can do. I liked how mmj2 works because it is also seemed simple > but very practical. So I decided to check if I can do something similar. > When I was able to repeat the proof from the mmj2 tutorial I wrote this > post. Now I am planning to work on two more major features - proving in > bottom-up direction and proof explorer, some small UI improvements and > writing more tests (the code is tough, I already found few bugs). When I > complete these goals, probably, I will use this assistant to learn to > create Metamath proofs myself. Editing code in a dedicated code editor is > much more comfortable but it is difficult to implement, so I didn’t even > choose between what kind of UI to implement. Simple HTML UI was the only > option for me. > >>>> > >>>> > >>>> "it might be good to provide a README.md (and a repository with a > sensible name)" > >>>> > >>>> I moved the code to a new repository and provided a README file with > instructions. Please let me know if there are any issues with running the > project locally. > >>>> > >>>> The new repo - https://github.com/expln/metamath-proof-assistant > >>>> > >>>> This project depends on @expln/utils npm module. This is my project > too ( https://github.com/expln/rescript-utils ) But this is not a usual > library. This is just a set of useful functions which I collected in one > place to reuse across my other projects. And version N+1 may be absolutely > not compatible with version N :) > >>>> > >>>> > >>>> "I'd like to see some reusable packages make their way into the npm > repository so that this isn't such a huge mountain to climb." > >>>> > >>>> That’s a good idea. As for now I think it makes sense for me to > implement remaining features and when the code (underlying data structures) > become more stable, I will be able to create some API and publish it as an > npm package. I also feel like I need to warn regarding the algorithm I use > for unification. I read in the mmj2 documentation that mmj2 first creates > syntax trees of expressions and then compares them to find possible > substitutions (please correct me if I am wrong). As I understand this > approach guaranties quick response for any expressions. But what I > implemented is comparing two arrays of integers with some performance > improvements (counting parentheses is one of them). And there is no > guarantee that this algorithm will work fast for any expressions. So it may > turn out that using my future library is not such a good decision :) > >>>> > >>>> > >>>> "I notice that you don't have a license included - please add one!" > >>>> > >>>> I added MIT license. Thanks for pointing out to this! > >>>> > >>>> > >>>> > >>>> Best regards, > >>>> > >>>> Igor > >>>> > >>>> > >>>> > >>>> On Thursday, January 5, 2023 at 5:14:42 PM UTC+1 David A. Wheeler > wrote: > >>>> > >>>> > On Jan 3, 2023, at 4:51 PM, Igor Ieskov <[email protected]> > wrote: > >>>> > > >>>> > Hi all, > >>>> > > >>>> > I am developing a web-based proof assistant and would like to share > current results. The proof assistant is written in ReScript programming > language and React UI library. It runs completely in the browser. It uses > the same approach for building proofs as mmj2 (but at the moment it doesn’t > have all the features mmj2 has). I recorded a video (without verbal > explanations) similar to one of the mmj2 tutorial videos in order to > demonstrate its features. Any feedback is appreciated. > >>>> > > >>>> > > >>>> > > >>>> > The demo video (if it is not opening, try to download; and sorry > for low quality of the video): > >>>> > > >>>> > > https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view?usp=share_link > > >>>> > > >>>> > > >>>> > The proof assistant: > >>>> > > >>>> > https://igorocky.github.io/mm-proof-assistant/demo/v1/index.html > >>>> > > >>>> > > >>>> > The source code is stored in two repositories. And there is mess > with it. I started writing it inside of another project, put some logic > into a second repo. Because of that it is not easy to run it locally. But I > am going to improve this soon. > >>>> > > >>>> > > >>>> > The source code: > >>>> > > >>>> > > https://github.com/Igorocky/learn-js-react-app/tree/master/src/metamath > >>>> > > >>>> > > https://github.com/Igorocky/js-common-functions/tree/master/src/main > >>>> > >>>> That's awesome! > >>>> > >>>> I notice that you don't have a license included - please add one! > >>>> If you're going to release as open source software, then you need an > OSS license. > >>>> MIT is especially common: > >>>> https://github.com/IQAndreas/markdown-licenses/blob/master/mit.md > >>>> The Apache-2.0 and GPL-2.0+ licenses are also widely used. > >>>> > >>>> A way to "get started" with proofs without any installation steps at > all has its appeal! > >>>> > >>>> Sadly, the mmj2 tool has become harder to install and maintain. > >>>> One problem: it's in Java, but it calls out to JavaScript code, and > the > >>>> mechanism it uses for calling JavaScript has been dropped from > more-recent versions of Java. > >>>> Specifically, mmj2 uses Nashorn. My understanding is that Nashorn's > intended replacement is GraalVM. > >>>> I don't think this is *unsurmountable*. > >>>> Mario looked into this briefly & expected that it wouldn't be hard to > switch to GraalVM > >>>> <https://github.com/digama0/mmj2/issues/7#issuecomment-428404641>, > >>>> but no one has (as of yet) picked up this work. > >>>> > >>>> --- 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/9aac3fc2-ea01-4bce-afab-7f08aa99be8en%40googlegroups.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/e4e7deb6-06e7-41a3-88a4-a2adcdf1293en%40googlegroups.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/2961bd35-1f93-8cce-feb2-760ace5ae4db%40gmx.net > . > > > > -- > > 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/a8ccebbc-1fca-4d52-87fb-cf9928d72260n%40googlegroups.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/dc697913-b921-4186-9ff8-8074c9099c7an%40googlegroups.com.
