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; > > > *>>> 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/bb432d88-7d0a-461f-af58-443cf71eeeafn%40googlegroups.com.
