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