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 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; >> >> >> *>>> 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/a8ccebbc-1fca-4d52-87fb-cf9928d72260n%40googlegroups.com.
