Hi Thierry, Sorry, I have not replied regarding the attached json file with an editor state. I saw there are few statements marked as " should work here ". But currently it is not easy to debug such issues, and I am also modifying the unification algorithm at the moment. So I decided to postpone this issue until I finish current changes. Maybe this issues will be resolved in the new code, otherwise it will be easier for me to investigate it because I am adding additional debug utilities.
Best regards, Igor On Wednesday, January 11, 2023 at 9:42:11 PM UTC+1 Igor Ieskov wrote: > Hi Thierry, > > *>>> 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...)* > > I reserved a simple click for future - I am planning to implement a > feature when a simple click on any symbol will highlight the smallest > syntax subtree the symbol is included into. I hope this feature will > simplify exploring long statements and also it should make it easier to > copy subexpressions. > > *>>> 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.* > > That’s right, currently a user is forced to type at least one dummy symbol > in that situation. I was trying to implement the editor in the most simple > way for me for not to spent a lot of time on ui development when some core > features are not ready. Unfortunately, this simple use case is not so > simple to fix. But I will definitely fix it in the future. > > *>>> 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…* > > Yeah, I also though about that. Unfortunately I don’t see any simple fix > for this at the moment. Moreover the unification algorithm is still under > development and I am actively modifying it now when developing bottom-up > proofs. But for sure I will try to improve this in the future. BTW, what is > current behavior of mmj2 in a similar situation? > > Thanks Thierry for your feedback! > > 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/2630b29b-067a-42d1-bc6c-6c520d71564cn%40googlegroups.com.
