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/e4e7deb6-06e7-41a3-88a4-a2adcdf1293en%40googlegroups.com.
