*>One broad suggestion: Could you give it a short & less generic
name,>since there are other Metamath proof assistants?*
That’s done! The new name is metamath-lamp “Lite Assistant for Metamath
Proofs”.
I renamed the repository accordingly:
https://github.com/expln/metamath-lamp
I guess I need to create a pull request to make corresponding changes on
https://us.metamath.org/other.html ? I will try after sending this email.
*> You might want to include, on the screen or an "about" option, a link to
the> GitHub repo for the code (so people can review/contribute). I
understand that is currently:>
https://github.com/expln/metamath-proof-assistant (MIT license).*
Good point. I will add such a link. Yes, MIT license, but the new URL is
https://github.com/expln/metamath-lamp
*> But I think trying to answer "why can't I automate this in general" is
best delayed for a long time.*
I thought on this, and finally concluded that this is not even a “nice to
have” but this is “must have” feature. The reasoning is as follows. Users
will ask me “why this doesn’t unify” or “why this cannot be proved
automatically”. Currently the only solution is to reproduce the case
locally and debug. But this is too hard because I debug by small steps and
I don’t see a bigger picture. Thus I conclude that I need some kind of log
of main events to understand faster what’s going on. So I feel like I
cannot delay development of this feature.
*> You could easily combine 2 & 3. Just create a first tactic called "auto"
or similar that tries to apply a few simple rules to automatically prove a
few simple/common cases.*
I don’t have enough experience to figure out what are the common cases. I
need to spend some time practicing in creating proofs first. And this is
related to the tutorial topic (please see my response on tutorial topic
below).
*> mmj2 has a few simple heuristics that it applies automatically its
default configuration.> You could make them either fully automatic or the
basis for an "auto" tactic. Code here>(I think Mario wrote more or all of
this):>>
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js*
Thanks for the reference. I will check and return back to you and Mario
with questions when I will be closer to writing heuristics.
*> Even a few small automations could make a big improvement in usability.*
If anyone sees such small automations please let me know. I have experience
in writing code which manipulates metamath statements, but this adds almost
nothing to my ability to create actual proofs, so such kind of small
improvements are not visible to me at the moment.
*> > b) highlighting syntax subtrees by clicking them> To simplify
replacing them, I guess?*
Yes, but not only. This should also make easier to copy subexpressions.
Currently unexperienced users like me have to count parentheses which is
too tedious.
*> I would instead prefer an optional simple column, to the left of the
statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS
(similar to how mmj2 works now).*
That’s doable. I will add this to my todo list and implement in some time.
*> You might want to walk through the mmj2 tutorial to see what ideas are>
worth stealing. I recorded it on Youtube here:>
https://www.youtube.com/watch?v=87mnU1ckbI0> The text is here:>
https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial*
Yeah, I watched it few times and will watch one more time with pleasure.
Moreover, I have now more understanding of the processes under the hood, so
I am able to catch more details. (When I watched it for the first time few
years ago it was like magic to me :) )
*> Once you're further along, I'd be happy to work with you to create a
tutorial> if you'd like. I'd probably want to build on the same examples
from the mmj2 tutorial.*
Of course! This is a great opportunity for me to get more experience in
creating proofs and simultaneously help other metamath newcomers to get
acquainted with it. If you can provide those mmp files from
us.metamath.org, and additionally some json file which will work as a table
of content for the tutorial, then I will parse them and represent in my
app. Such an interactive tutorial could be a good starting point for
beginners. So, once you think my app is ready to become a tutorial for
Metamath we may start a separate email thread and discuss details of
implementation of such tutorial. Currently I think the tool requires more
testing, because I implemented some algorithms by intuition and I have not
analyzed everything with mathematical rigor.
*> Nevermind, I see you can already rename statements*
In the previous versions it was not “true” renaming. Justifications were
not updated. But in the v6 renaming of statements updates justifications.
*> below I tell what I've come up with, in yamma.*
Thanks, Glauco, for the ideas. I checked your test cases and I see similar
validations may be implemented in metamath-lamp too.
*> 'Working Var unification error: the working var &W2 should be replaced
with the following subformula, containing itself ( &W2 -> ph )'*
Could you please explain why a working var cannot be replaced by a
subformula containing itself? It is possible in mm-lamp and I don’t see any
reason why it should not be possible.
*> Hope this can give you some ideas.*
Definitely! Thank you, Glauco!
I implemented few new features and moved my tool to a new URL -
https://expln.github.io/lamp/latest/index.html
1) Exit edit mode on ESC, save changes on Enter on all text fields in the
editor. (To start a new line in a multiline text editor press Shift+Enter,
this is not mentioned on tooltips, but I will add it in the next versions )
2) Shorter names for statements and “true” renaming of statements when
justifications are also updated with the new statement label.
3) In substitution dialog, now it is possible to see hints why some
substitutions are invalid.
4) A new parameter in bottom-up proofs - “Derive from root statements”. It
was present in v5 and it was always “true”. But it significantly decreases
performance and I expect it to be not necessary in many cases. So I added
it to the bottom-up dialog and set its default value to false. Users will
be able to decide if they want to use it or not. I understand that I have
to provide here more details on how bottom-up exactly works in mm-lamp and
in particular what the new parameter does. But unfortunately I don’t have
time right now. I will write this a bit later.
The demo video below demonstrates #3 feature and the use case when #4
feature could be useful.
https://drive.google.com/file/d/1nIigII46Z8l1xk9VRWlPT9_N-VcNTh2R/view?usp=sharing
Current latest version is https://expln.github.io/lamp/v6/index.html
-
Igor
On Sunday, February 12, 2023 at 9:08:43 PM UTC+1 Igor Ieskov wrote:
> Sorry, I missed one question which could be easily answered:
>
> *> I don't see how to create hypothesis statements in the tool*
>
> This is implemented. Each statement is prefixed with an upper case letter
> either P (provable) or H (hypothesis). Alt-left-click allows to change it.
> This is demonstrated at 5:49 in this video -
> https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view
>
> -
> Igor
>
> On Sunday, February 12, 2023 at 1:12:24 AM UTC+1 Glauco wrote:
>
>> On 2/11/23 07:39, David A. Wheeler wrote:
>>
>> > 1) I think one of the "key" missing things is ability to help a user
>> > to understand why a statement doesn't unify.
>>
>> I have only an approximate idea of whether this is easy or hard, but I
>> will say that even modest improvements here would be helpful. For
>> example, it may be easier to detect particular cases than every possible
>> "way" a statement can't unify. One of the more time consuming things
>> that happens to me when using mmj2 is that a unification which I
>> expected to happen doesn't, and then I need to look at (sometimes long)
>> expressions to figure out what parts don't match.
>>
>> Hi Igor,
>>
>> below I tell what I've come up with, in yamma.
>>
>> First, I'll write the short story, then I'll elaborate a bit about the
>> theory and the challenges.
>>
>> The short story:
>>
>> yamma has two kinds of diagnostic messages for unification failure.
>>
>>
>> The first kind of message, suggests how to fix the unification error. Two
>> examples:
>>
>> "Unification error: referenced statement is '|- ph' but it was expected
>> to be '|- ( ps -> ph )'"
>>
>> (see
>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329
>>
>> for the full unit test)
>>
>> or
>>
>> "Unification error: statement is '|- ch' but it was expected to be '|- (
>> &W1 <-> &W2 )'"
>>
>> (see
>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498
>>
>> for the full unit test)
>>
>> The first example is a diagnostic highlighted on the hyp label,
>> referencing a formula that doesn't match what's expected.
>> The second example is a diagnostic on the statement itself (the 'main'
>> formula cannot be unified with what's expected by the step label)
>>
>>
>> The second kind of messages, involves substitution of working vars.
>> Example:
>>
>> 'Working Var unification error: the working var &W2 should be replaced
>> with the following subformula, containing itself ( &W2 -> ph )'
>>
>> (see
>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420
>>
>> for the full unit test)
>>
>>
>>
>> Now, a bit of 'theory' (as far as I understand it)
>>
>> There are two categories of unification:
>>
>> 1. single statement
>>
>> 2. multiple statements
>>
>> With single statement unification, you're trying to find the mgu for both
>> the logical variables (the theory's variables) and the (possible) working
>> variables. You could use a Martelli Montanari algorithm on the whole proof,
>> and it will be clean and "secure", but you'll not get a super-informative
>> error message.
>> That's why, for the single statement unification, I've gone for a
>> 'custom' approach, that allows for some better error message.
>>
>> With multiple statement unification, you're trying to find the mgu for
>> all the working vars in the proof (because logical variables have already
>> been 'substituted').
>> Here, I've gone with the 'pure' Martelli Montanari algorithm.
>> It can fail either
>> - with a 'clash fail' error (for metamath, it means two constants don't
>> match; something like '->' was expected, but you have '<->' )
>> or
>> - with an 'occur check fail' (a working var should be replaced with a
>> formula strictly containing itself)
>>
>> Hope this can give you some ideas.
>>
>>
>
--
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/4c913c14-d74b-4457-a6af-f6fd5dcc5e13n%40googlegroups.com.
