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 <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 <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.
