Mephistolus development

[Olivier Binda]

Let's make this the Thread about Mephistolus (it'll help prevent me spamming the metamath group).
I'll report the Mephistolus progress in here and maybee also, post stuff about it's internals and design decisions
( and ask a lot  of help for metamath experts when I'm at a loss, I'll be in you gentle care :))

Milestone 5 has been reached, with the first Mephistolus-proof exported and proof checked in Metamath for an exercise I give to my students (now only 400+ more to go :) ) :

 

|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) )

Here is the high level human proof : 

/** proving that ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) */
val assertion = "( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) )".toSingle("∨1c e. CC", "∨3c e. NN0")
val result = "( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )".toStatement()
val step = "|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) )".toStatement()
val i = "∨2s".toStatement()
val j = dummy(MType.S, assertion.origin, *assertion.context.toTypedArray())
val proof = assertion
    .s(AxSum)                                                                                 /*.s(A_times_Sum)*/ // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( 1 - ∨1c ) x. ( ∨1c ^ ∨2s ) )
    .c(rotX)                                                                                  // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) x. ( 1 - ∨1c ) )
    .c(Ax_BsubC)                                                                              // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ( ∨1c ^ ∨2s ) x. 1 ) - ( ( ∨1c ^ ∨2s ) x. ∨1c ) )
    .eq(P.c.a.th(Ax1), P.c.c.th(Aexp_Bp1))                                                    // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) - ( ∨1c ^ ( ∨2s + 1 ) ) )
    .s(Sum_AsubB)                                                                             // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ( ∨2s + 1 ) ) )
    .c(Sum_CDI) { arrayOf(j, statement1, "( ∨1c ^ ( ( $j - 1 ) + 1 ) )".toStatement()) }      // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( ( 0 + 1 ) .. ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 ) ) )
    .eq(P.c.b.a.mut(Engine::reduceAddition))                                                  // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 )
    .eq(P.c.c.c.th(rotSubP))                                                                  // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ∨5s - ( 1 - 1 ) ) )
    .eq(P.c.c.mut(Engine::reduce))                                                            // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ∨5s ) )
    .eq(P.a.th(ApSumA) { arrayOf("( ∨1c ^ 0 )".toStatement()) }, P.c.th(SumA_pA) { arrayOf("( ∨1c ^ ( ∨3c + 1 ) )".toStatement()) })      // ( ( ( ∨1c ^ 0 ) + sum_ ∨2s e. ( ( 0 + 1 ) ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ( ( ∨3c + 1 ) - 1 ) ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) )
    .eq(P.a.a.mut(Engine::reduce), P.a.c.b.mut(Engine::reduce), P.c.a.b.c.th(rotPSub))        // ( ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ( ∨3c + ( 1 - 1 ) ) ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) )
    .eq(P.c.a.b.c.mut(Engine::reduce))                                                        //  ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) )
    .s(rotPSub)                                                                               // ( 1 + ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - ( sum_ ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ) )
    .c(rotSubSub)                                                                             // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) )
    .eq(P.c.a.c.th(Sum_CDV) { arrayOf(i, "( ∨1c ^ $i )".toStatement()) })                     // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) )
    .eq(P.c.mut(Engine::reduce))                                                              // ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )
/** done */

Here are the goals for Milestone 6 (let's make Mephistolus a concrete goal driven development, instead of a feature driven development) : 

context("Exo 2.7") {
    it("a") {
        val s = "sum_ ∨2s e. ( 1 ... ( ∨1c - 1 ) ) ( ( 5 x. ( 3 ^ -u ∨2s ) ) - ( 4 x. ( 2 ^ ( ( 2 x. ∨2s ) - 1 ) ) ) )".toSingle("∨1c e. NN")
    }
    it("b") {
        val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( 1 / 4 ) ^ ( 2 x. ∨2s ) ) )".toSingle("∨1c e. NN0")
    }
    it("c") {
        val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ( ( ( ( ∨1c ^ 2 ) x. ∨2s ) + ( ∨1c x. ( ∨2s ^ 2 ) ) ) - ( 3 x. ( ∨2s ^ 3 ) ) ) / ( ∨1c ^ 4 ) )".toSingle("∨1c e. NN0")
    }
    it("d") {
        val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( ( ( ∨2s x. ( ∨2s - 1 ) ) x. ( 3 ^ ∨2s ) ) - ( 5 ^ ( ∨2s - 1 ) ) ) / ( 3 ^ ∨2s ) )".toSingle("∨1c e. NN0")
    }
    it("e") {
        val s = "sum_ ∨2s e. ( 0 ... ( ( 2 x. ∨1c ) - 1 ) ) ( 5 / ( 6 ^ ( ∨2s - 1 ) ) )".toSingle("∨1c e. NN0")
    }
}
context("Exo 2.10") {
    it("1 (induction)") {
        val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s ) ) = ( ( ! ` ( ∨2s + 1 ) ) - 1 )".toSingle("∨1c e. NN")
    }
    it("2 (telescopic sums)") {
        val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s ) )".toSingle("∨1c e. NN")
    }
}

Milestone 6 will be reached with 2 other real world proofs involving only  sums (say Exo2.7a and Exo 2.7b) and for 1 real world proof by induction (say Exo 2.10.1)

Best regards,
Olivier

[Mario Carneiro]

Have you thought about providing a limited release, or a recording of you using the program? It's not really clear to me what the overall program is, and you post snippets that lack the context to make sense of them (I don't think you are expecting people to run them, but I don't even know what language they are written in). Is this the end user experience or is there some GUI front end? The code snippets on their own only provide a myopic view into the development process.

I know you want to ultimately sell this program, and I don't want to make you do anything to compromise that, but you might get more and better feedback if you provide a more comprehensive overview of what the program is.

Mario

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3c43167b-f7ad-4eff-b90e-a75460fd5862%40googlegroups.com.

[Olivier Binda]

Short answer : At the moment (19/11/2019)

Mephistolus is a library, written in the (new but promising) Kotlin langage.
It is mostly a tooling layer over  metamath that holds  :

a Metamath parser : for turning strings into Metamath trees
an experimental Math API : for mutating Metamath trees and proving the mutations, a bit like we, humans, do maths
simple math services : for automatically providing the numerous hypotheses needed by theorems, like A =/= 0, A e. B, A <_ B, ...

a collection of Mephistolus theorems (like metamath deduction theorems but that make handling any number of antecedents easier)
a Mephistolus proof checker
a Mephistolus to MetaMath proof exporter

a Metamath Proof checker (to test the exported metamath proofs)

The only user that this library will probably ever have is me.
But, I intend to use this library to build a free (but closed) app that allows anyone to read/write/use ( metamath) proof checked maths

I have 2 targets for the app : 
- mathematicians 

- the general public (say everyone between 16 and 99 years old)

First, I am focusing on mathematicians and my priority is to build the library so that it enpowers the metamath-experts among mathematicians 
to have a better/faster workflow. Basicaly, I would like Mephistolus to allow expert meta-mathematiciens to prove what they want,
without hassle, faster and with all the help a computer (and code by me) can muster (it is a goal for Mephistolus to be fun, powerful and hassle free).

As of now, I do not know if you have a use yet for the help that Mephistolus can provide : 
It only handles a few operators (+, -, /, *, ^, !, -u, -., /\\, \//, A., E., [_ / ]_, [ / ], F/, F/_, e., <, <_, C_, sum_

It can apply any metamath theorem but it can only provide sugar/fun math api for Mephistolus-theorem

 So, I am slowly improving it, in the hope that one day, it will provide enough to make people want to use Mephistolus more than, say mmj2 which is powerful and efficient, now.

The snipets I post are to give people some idea what to expect. This is neither the user experience, nor a gui.
You are right, I should document how you build a proof in Mephistolus. 
I'll think how (maybee slides ?) to explain what could be done with Mephistolus

Thanks for the pointers,
Olivier

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

[fl]

 

I have 2 targets for the app : 
- mathematicians 

Real mathematicians don't use proof checkers, I'm afraid. It's too time-consuming.

Villani has poroblems with statistics by the way. Who can help him?

https://www.huffingtonpost.fr/entry/municipales-2020-villani-saisit-la-commission-des-sondages-apres-des-chiffres-publies-par-griveaux_fr_5dd3a4c2e4b0d6f02fa495a9

(And there are true believers who believe in evidence-based reality. Sighs...)

-- 

FL 

[vvs]

Real mathematicians don't use proof checkers, I'm afraid. It's too time-consuming.

They will, as somebody said: "mathematics is a game", and mathematicians like to play. Proof assistants just need a good UI to make it fun. Right now it's boring as you already said.

[Olivier Binda]

I agree with both of your views :) 

As for Mario's take. I am not sure that I'll be able to create a proper mock up of what could be done with Mephistolus. And It'll probably be a waste of time.
So, I am just going to just coding an experimental UI for the App/Proof assistant (I'll have to do it anyway at one point).

Once it is done, it'll be easier to explain to people what can be done and what cannot (I will be able to record the Mephistolus workflow).
and hopefully, I'll get good feedback to improve things afterwards. :)

So, I'm going to code an UI through a single WebView, in Html/css/Javascript/MathJax/MathMl/Kotlin.

And only implement the most basic math workflow (click and choose, user makes detailed decisions about expression mutations)
Don't expect something fancy and polished. Let's just make something that works as expected first. :)

This is going to be fun. :)

Diving now in the code, see you when I have really something to display... 
Best regards,
Olivier

[Olivier Binda]

This is a first video showcasing 2 things :
- math rendering with MathJax
- click to select a part of a metamath statement and apply some operation on it (reduction only in this video)
It illustrates a bit what I am trying to accomplish : Math could mostly be as simple as pointing to a bit of a statement and choosing a possible outcome

The first reduction takes a lot of time because the math engine does a cold start and has to initialize everything (the parser, the theorems...)
It becomes faster afterwards

It took some time to get the WebView and the javascript parts going (I get to learn javascript the hard way, by discovering and squishing bugs :/) and coding an UI for the dom is a bit painful (it is weird, lots of things are possible but you have to discover how and there is a lot of complexity involved).

Next, I think that I'll
1) display on the side the metamath statements that are proven with each operation, in a collapsable list.
2) click on a proven metamath statement and export it's metamath proof to a file

3) input a metamath statement (with antecedents) with error reporting when it is not well formed

Any feedback is welcome. :)

Best regards,
Olivier

[Thierry Arnoux]


Hi Olivier,

Very interesting!

Mathjax is also what I’m using for the rendering of the “structured” pages, like:

http://metamath.tirix.org/esum.html

http://metamath.tirix.org/areacirc.html

I’m maintaining the rules for translating any set.mm statement into MathJax here:

https://github.com/metamath/set.mm/blob/develop/set-mathml.mmts

Feel free to reuse it!

It looks like for simplifying a formula, one would start at the lowest level, and then continuously work ones way up:

If I’m looking for a proof assistant, I would probably like to have this automated, and the whole formula simplified in one step.

But I suppose for educational purposes, you want to expose each of these steps.

BR,

_

Thierry

[Olivier Binda]

Hey Thierry

Thanks for those rules. I am planning to export human proofs to TeX (and let mathJax do the translation to mathML), so I might not be able to use your rules as is but, following their lead, they might speed up writing TeX rules. I'll open source the rules for translating metamath to TeX, once/when/if I write them.
That way human proofs may be exported to the web or to pdf, for printing

You are right about the symplifying the formula part and about the showcasing part too.
By selecting the root of a formula and applying reduce, it can be simplified in one go.
When formulas are too complicated for Mephistolus to handle, it will require some human gently guiding it's software hands (like with students)

(much) later, I hope to be able to handle commutativity, associativity, moving things around in a user/mouse/touch friendly way.

Best regards,
Olivier

[Olivier Binda]

Mephisolus reached Milestone 6

Here is a video, proving that it did : https://www.youtube.com/watch?v=HuLFpQxwkmU&feature=youtu.be

It shows me a bit stressed (this was my fith attempt, there is always something going wrong... :) and struggling at the end with html ^^;
 
Sadly, the exported metamath proof had an issue (I store metamath theorem with some renaming/shuhhling of variables and It messed up the exported proof). 
I'll fix it at soon as possible and hopefully post a valid exported proof. 

I'm quite happy with the result : it ended up a bit better that I envisionned and, I already have quite a few ideas about how to further enhance the user workflow and make it much better.

Hoping to get some feedback now :)

And preparing to start development of Mephistolus Milestone 7...

Best regards, 
Olivier

[Giovanni Mascellani]

Hi,

Il 21/01/20 22:24, Olivier Binda ha scritto:

> Here is a video, proving that it did
> : https://www.youtube.com/watch?v=HuLFpQxwkmU&feature=youtu.be
> It shows me a bit stressed (this was my fith attempt, there is always
> something going wrong... :) and struggling at the end with html ^^;

Nice video, it seems to be a useful tool for this type of computations.
Being able to visually select and manipulate an expression can be
convenient to locally edit a formula while at the same time having a
global view on the whole of it.

Does the vieo have a comment? To me the video is completely mute (I can
hear the audio from other YouTube videos, so it doesn't seem to be a
problem in my gear).

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[OlivierBinda]

Hello.


The video has no sound (that way, I won't have to record it again if I
mess up the comments).
When/If the app becomes useful, I'll publish the app and video/tutorial
with sounds to explain features/workflow.

At this point, the video is mostly there so that we can discuss what
would be a nicer UI/way of doing things,
what we can accomplish and what we cannot, possibilities, features,
wishes, etc...

Obviously, making the action menu resizable and dragable was a big
mistake : next time, it'll be anchored at the right side of the window
and will resize automatically automatically

Also, past mutations will be foldable/hidden, so that they don't take
too much screen estate and so that we can concentrate on the last result


The "select and mutate" process is the signature move of Mephistolus at
this point.
It is also available in 2 of mutation categories :
same "power" equality =, equivalence <->
different "power" : implication ->, inequalities <=, <, binary relations...

For example :

|- ( x in A -> x <_ 2 )

with the mutation

|- 2 <_ 3

provides |- ( x in A -> x <_ 3 ) by proving the statement |- ( x in A ->
( x <_ 2 ) -> x <_ 3 ) )

Different "power"


Olivier

[OlivierBinda]

Il 22/01/20 11:00, OlivierBinda ha scritto:

Obviously, making the action menu resizable and dragable was a big
mistake : next time, it'll be anchored at the right side of the window
and will resize automatically automatically

Yes, it's quite clear that the action menu is still rather awkward to
use. And, to be honest, I don't think it is easy to find the right way
to lay it down. It seems to be quite a UX challenge.

Yes, I'll try my best (and take advices)

Also, in the next release, I am planning to filter/order display in a better way the actions in this menu (because it is a mess at the moment). It is very hard to do so(it requires human smarts), but I'll probably be able to do a decent job (with computer smarts).

Another thing I noticed is that the variable name that you write are
different from those that appear in the pretty printed formula. For
example, you write "v1c" and "X" appears in the formula. This is quite
counterintuitive, I believe.

Yes, you are right about that
Internally, Mephistolus uses names like v2s, v8c, v3w
for setvar, classvar and wffvar

But as It is aimed at the general public, my goal is to allow people to use the variable names they like
x, k,n or it might be stuff like 平 or  ひ , etc...

At the moment, I am able to display custom variable names.
But I haven't implemented yet, the translation process to convert a user variable name like x, to the right variable set/class/wff type

I still have to figure out how to do it. I'll probably try first to infer if it should be a wff var or not,
go with class var by default and fallback to setvar if it is necessary.

Hopefully, that will work out nicely (or I'll have to think further about it :) )

ps : sorry for the double mail, I'll probably get it soon ^^

[Olivier Binda]

Here are my main goals for Mephistolus Milestone 7 : 


1) build a pure kotlin metamath antlr parser and build a Mephistolus App with the Kotlin/Js target, so that we can use it in a browser
(that way, it would be  easier for you to test it)

2) improve the UI and the user workflow, 
a) save and load a proof (this requires choosing a serialization format for representing the proof state)
b) filter/order/fix the action menu to make it fun/great to use
c) fold previous steps to concentrate on the last step
d) experiment with a custom user variable name -> mephistolus var name, to completely hide internal mephistolus names
e) research  : Method (or tactic ?) groups : 

the user should be able to say : I want to prove an induction, or I want to prove an <-> through 2 x ->
and then Mephistolus should display places where the user would prove sub-aim and let Mephistolus write the annoying and repetitive glue
to get the final statement

3) research enhancements to the back-end
a) when doing an index change, you should just give the translation : use explicit mephistolus theorem instead of implicit ones, to remove the need for the user to input too many substitutions
for example, instead of using this
"sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = sum_ ∨5s e. ( ( ∨2c + ∨6c ) ... ( ∨3c + ∨6c ) ) ∨7c", 

"∨2c e. ZZ", "∨3c e. ZZ", "∨6c e. ZZ", "( ∨1s e. ( ∨2c ... ∨3c ) -> ∨4c e. CC )", "( ∨1s = ( ∨5s - ∨6c ) -> ∨4c = ∨7c )"

I should probably use something like  : 
 "sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = sum_ ∨1s e. ( ( ∨2c + ∨5c ) ... ( ∨3c + ∨5c ) ) [ ∨1s - ∨5c / ∨1s  ] ∨4c",

That way, Mephistolus only has to ask for v5c and then, let it reduce the [ ∨1s - ∨5c / ∨1s  ] ∨4c part, it is good at that

b) research unification, from infered parts and rthe result of substitution hypotheses

for example, an hypothesis like 

 ( ∨1s = ∨4s -> ∨3c = ∨5c )

 should allow us to infer from v1s, v4s and v3c what v5c should be

c) out of the 30000+ metamath theorem, migrate all those who can to mephistolus theorems

4) fix bugs

5) Mm0
a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking at you...
b) parse set.mm0
c) extract a list of all mm0 ids

d) write a parser for mm0 statements

e) make the mephistolus Statement able to be build on mm0 stuff

Well, that should keep me busy and happy for the next months.

Le mercredi 22 janvier 2020 11:18:40 UTC+1, Oliv

ier Binda a écrit :

[Mario Carneiro]

On Wed, Jan 22, 2020 at 10:51 AM Olivier Binda <olus....@gmail.com> wrote:

5) Mm0

a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking at you...
b) parse set.mm0
c) extract a list of all mm0 ids

d) write a parser for mm0 statements

e) make the mephistolus Statement able to be build on mm0 stuff

I can send you the translated set.mm0 file (or you can run mm0-hs yourself to perform the translation), but I don't think it is necessarily representative of the things you will normally find in an MM0 file. It has no "def"s, for example, because set.mm uses axioms for definitions and the translator doesn't yet know enough to derive the equivalent def statement. A more representative sample is peano.mm0. If you want to parse theorems in set.mm, then the simplest way to get these is to read set.mm rather than translating it first.

There are also tools for reading an MM0 file and turning it into an .mmu file, which has all statements and proofs written as s-expressions. This is probably much easier to parse, although it can get a bit big.

[Thierry Arnoux]

Very interesting!

It's nice to see that apart from entering the input at the very beginning, and apart from the substitutions, you only deal with the graphical display of the equations.
Do you have any idea how the last use of dummy variables (v1c, v3c), for substitutions, could be eliminated?

I wonder what is the operation "order" towards the top of the list, which results in "0". Does it mean it cannot be applied? Could you then simply omit to list it?

Of course an interesting topic to discuss is the choice of when/where to add parenthesis, we had an extensive discussion about this when I introduced the
I saw some cases where it seems to be they can obviously be removed, like in " ( k e. ( { A ... B } ) ) " at 2:10. That's parenthesis where even set.mm does not have any! ;-)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/af959f49-b997-48f3-9ae8-8705f04da967%40googlegroups.com.

[OlivierBinda]

Le 23/01/2020 à 05:39, Thierry Arnoux a écrit :

Very interesting!

It's nice to see that apart from entering the input at the very beginning, and apart from the substitutions, you only deal with the graphical display of the equations.
Do you have any idea how the last use of dummy variables (v1c, v3c), for substitutions, could be eliminated?

Yes. There is no reason a computer would need 3 substitutions when a human only uses 1 + mechanical computation.
That is, when you shift an index in a sum, you should just need to give the amount of shifting

It should be possible to make Mephistolus accomplish this by having it analyze the hypotheses of a theorem,
find the ones where a substitution or a computation happens to define another substitution
and only ask for the values needed to infer other substitutions automatically

That's my plan

I wonder what is the operation "order" towards the top of the list, which results in "0". Does it mean it cannot be applied?

It is a dud : as I rushed to build mephistolus 6, I display the actions that could, eventually, be applied to get a mutation
but, as of now, some operations don't work (because hypotheses are missing or false) or cannot be made to work by himself by mephistolus (require human help).
Also, I did not filter out some properties, like transitivity, that populate the action menu with lots of irrelevant possibilities (most of the time)

Could you then simply omit to list it?

Yes. Next time, I'll do a better job about it :
I'll filter out the garbage, show working operations (or show potentially working operations tagged with the need for human help), order the actions with respect to some better category (theorems that move stuff around (like commutativity), ...) and with some relevance score (like proximity from the goal, or like less complexity

I mean if you have |- a = b, most of the time, you don't want to have |- a = b + 0 or |- a = ( b x. 1 ) next

Of course an interesting topic to discuss is the choice of when/where to add parenthesis, we had an extensive discussion about this when I introduced the

when you introduced the ?

May I have a link to this discussion (this interests me a lot, as you can guess).
In the mean time, I'll dig into the metamath discussions, Thierry Arnoux posts to try to find clues about that

I saw some cases where it seems to be they can obviously be removed, like in " ( k e. ( { A ... B } ) ) " at 2:10. That's parenthesis where even set.mm does not have any! ;-)

Yes ^^ :) lol

I have only just started removing useless parenthesis
(like 4 days ago and this is my first try)

I basically walk the tree structure for a metamath statement and, for each pair of (child, parent),
I decide if the child needs a parenthesis.

There are quite a lot of things that can be done with that.
I mostly look :
   - if the child has at least 2 children
   - if the child operation priority is less than the parent operation priority

at the moment, with only partial coverage of the operators I use.
So, there are still parentheses that can be removed (around sums also)

Thanks for the feedback and the pointer (I'll go start looking for your posts now)

Best regards,

Olivier

[Olivier Binda]

Hello Mario

I just wrote a (multi-target pure kotlin) antlr parser for parsing mm0 files.
It is buggy, at the moment because it seems that there is an issue with the antlr-kotlin project (that I have reported) with EOF) but It still parses everything except peano.mm0 and x86.mm0

I had to taylor the grammar that you described in mm0.md to antlr and I expect to have made a few errors (I know I have made one with the way I fetch MathString).
But I'll soon fix everything. Once I do, I'll publish the antlr grammar file. mm0.md was a great help, I understand a bit more of mm0 and I expect to understand even more soon, once I play with it.

Please, could you send me your translated file for set.mm ?

(I tried seting up haskell on my computer and to translate it myself and finally gave up... also, I have really no use for Haskell)

I'll soon start to write the secondary mm0 parser for math strings. Do you have any advice about it, that could help me ?

Also, on another subject :
I build Mephistolus for the browser target but there are issues in the transpiling process from kotlin to javascript. I fixed some of them but at this point the app launches but there are (bloody silent javascript) exceptions when I try to reduce statements
So I have some more debugging to do (meanwhile I take a pause by looking at mm0 ^^).

Best regards,
Olivier