*>>> 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; *>>> MMJ2 automatically merged them, IIRC. It would be very nice to have the same mechanism (automatically updating corresponding justifications too, of course!)* I have not realized that identical statements could appear as a result of substitution. Now I will add this case to my plans of what to do. Thanks for the idea :) 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: > > 1. > > “the two expressions must have no variables in common”: [x] and > [class2] have no common variables - this is passed. > 2. > > “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/v*N*/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 >> >> <https://groups.google.com/d/msgid/metamath/9aac3fc2-ea01-4bce-afab-7f08aa99be8en%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/e4e7deb6-06e7-41a3-88a4-a2adcdf1293en%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/e4e7deb6-06e7-41a3-88a4-a2adcdf1293en%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/2961bd35-1f93-8cce-feb2-760ace5ae4db%40gmx.net > > <https://groups.google.com/d/msgid/metamath/2961bd35-1f93-8cce-feb2-760ace5ae4db%40gmx.net?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/60a405cf-5163-4f56-94d1-eb81d54bad84n%40googlegroups.com.
