> 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/F4F5A4FC-995E-44B4-BC20-BF4161493A4F%40dwheeler.com.
