Mephistolus (towards Milestone 5)

[Olivier Binda]

I do a lot of cow boy coding and nothing is set in stone but : 

1) I would like to start looking into mm0 and building Mephistolus over mm0
(because at one point, I will want user to be able to add definitions of their own and I will need the added soundness, as well as the simpler parsing, and maybee other stuff that I don't understand yet)

Also, by building mephistolus on mm and mm0, It'll become more generic and probably better (closer to true maths).

2) I need to extend the capacities of Mephistolus
I couldn't export a few mephistolus theorems to metamath because the Mephistolus 4 features wre lacking (regarding location of expression in various sets, proving that some stuff is =/= 0 ). 
Exporting them to metamath will drive Mephistolus features developement

Also, Mephistolus only supports a very limited set of operators as of now (->, <->, -., +, -, x, /, -u). I need to slowly add more operators (I have to rework the quickly hacked sum_ support I had, prod_, forall, exists...) to make Mephistolus more useful

3) Some core Statement api may still be improved

a) I just realized today that I had to enable the user to apply a theorem to an equality like in 

|- 2 < 3

apply x |-> -u x to get

|- -u 3 < -u 2

We have all used this process so many times that we would miss it if it wasn't there...
I just have to figure out a good way to bake it in

b) my current api (with .eq, .imp, .a .b .c ...) is quite nice to work with but I got another idea to make it more generic and simpler, I want to explore that

4) making metamath theorems available in mephistolus 

a) now that I have proved a lot of Mephistolus theorems in metamath, and that I know what I am doing, I should write a method to enhance most metamath theorems into mephistolus theorems.
I should be able to convert 10000+ metamath theorems into mephistolus to make them available (Mephistolus can, out of the box, use any metamath theorem but Mephistolus theorems are a lot better to work with because the Mephistolus api is designed to work with them)

b) I should implement something that makes it easy for a user (not me) to select a mephistolus theorem

For example, I don't want user to have to learn ids like "ltsubrpd" to be able to call |- ( ph -> ( A - B ) < A )

Maybee something like select("a-b<a") where you can select a theorem by giving a utf8 string (that's right, NOT ASCII), with alternatives so ascii could still be an option

It doesn't have to be perfect as, later, if there are ambiguities, the api would suggest completions

Later on, a database with powerfull full text search/indexing capabilities would be used (issue, find a library available in Native, JVM, browser that enable that. I have experience with  Janusgraph and Lucene on the JVM, but they are not multi platform (yet))
to help with that

And that is already enough to make Milestone 5 a lot of work, let's end it here ^^;

[Mario Carneiro]

On Fri, Oct 18, 2019 at 5:21 AM Olivier Binda <olus....@gmail.com> wrote:

I do a lot of cow boy coding and nothing is set in stone but : 

1) I would like to start looking into mm0 and building Mephistolus over mm0
(because at one point, I will want user to be able to add definitions of their own and I will need the added soundness, as well as the simpler parsing, and maybee other stuff that I don't understand yet)

Also, by building mephistolus on mm and mm0, It'll become more generic and probably better (closer to true maths).

Assuming you have a program that thinks for a while and spits out theorem references, you can probably create a .mmu file without too much effort. This is a very simple lisp s-expression syntax for MM0 proofs, which is probably a lot easier to work with than the binary format.

Unfortunately, the .mmu examples on the web page are out of date. The previous version had some nontrivial parsing stuff (keywords, punctuation) and now it's all (pure (s-expressions) (like (this))) to keep it simple.

Alternatively, if you have an MM exporter already, you can just run the resulting .mm file through the MM -> MM0 translator.

One new option in MM0 (rather MM1) is that you could write your program *in* MM1. This is reasonable for simple programs that do pattern matching and such but if it's really complicated it might be a performance problem (plus it's untyped so it's probably not a good idea to write a huge amount of code in it). You should also be able to call Mephistolus from MM1, although the infrastructure for that isn't built yet. Ask me if you have any questions.

 

Mario

[Olivier Binda]

Alternatively, if you have an MM exporter already, you can just run the resulting .mm file through the MM -> MM0 translator.

Indeed. I might be able to do this on the resulting mm proof to turn it into a mm0 proof.
But I would rather have high level proofs of Mephistolus Theorems based on mm0 theorems.

Or, it might also be possible to import mm0 (or mm) theorems as Mephistolus theorems and Have Mephistolus be self reliant, with it's own set of axioms.  
But by doing this, I would lose a very valuable asset : metamath and it's worldwide experts that constantly improve the way metamath describes math.

I have started looking at the Peano file and understanding mm0.

This looks a lot like function signatures, with abstract/concrete bodies.
So Mephistolus statements like "( v1w -> v2w )" might be viewed as a function im (v1w v2w : wff) : wff = $( v1w -> v2w )$
... looking further into it...

[Mario Carneiro]

On Fri, Oct 18, 2019 at 3:29 PM Olivier Binda <olus....@gmail.com> wrote:

I have started looking at the Peano file and understanding mm0.

This looks a lot like function signatures, with abstract/concrete bodies.
So Mephistolus statements like "( v1w -> v2w )" might be viewed as a function im (v1w v2w : wff) : wff = $( v1w -> v2w )$

That depends on what you mean. A "term" or "def" is used to define a new expression constructor, like implication. That looks like this:

term im: wff > wff > wff;

infixr im: $->$ prec 25;

That declares implication as a right arrow (right associative), and from this point on you are permitted to write things like "v1w -> v2w" in statements. It is basically the equivalent of metamath's

wi $a wff ( ph -> ps ) $.

statement.

This is by contrast to theorem statements and hypotheses, which in metamath usually come after a "|-" symbol. In MM0 these appear in "axiom" and "theorem" statements, like this one:

theorem syl (a b c: wff) (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $;

This says that given proofs of a -> b and b -> c, we get a proof of a -> c. In MM0 this ends right away with a semicolon, and in MM1 the proof is given afterwards as a lisp expression:

theorem syl (a b c: wff) (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $ = (proof...);

These are exactly analogous to the theorems that take up the majority of the space in MM databases like set.mm.

[Olivier Binda]

I had to downgrade my requirements for reaching Milestone 5 as I am entering harder country.

Today I downloaded metamath, compiled it on linux and tried proof checking Mephistolus proven theorems.

I was successfull with 

${

     eqEq.1 $e |- ( ph -> ( ps -> ( ka -> ( la <-> rh ) ) ) ) $.

     eqEq.2 $e |- ( ph -> ( ps -> ( ka -> ( mu <-> si ) ) ) ) $.

    $( (Contributed by Mephistolus, 4-Nov-2019.) $)

    eqEq $p |- ( ph -> ( ps -> ( ka -> ( ( la <-> mu ) <-> ( rh <-> si ) ) ) ) ) 

     $= wph wps wa wka wla wmu wb wrh wsi wb wb wi wi wph wps wka wla wmu wb wrh 

      wsi wb wb wi wi wi wph wps wa wka wa wla wmu wb wrh wsi wb wb wi wph wps 

      wa wka wla wmu wb wrh wsi wb wb wi wi wph wps wa wka wa wla wrh wmu wsi wph 

      wps wa wka wa wla wrh wb wi wph wps wa wka wla wrh wb wi wi wph wps wa 

      wka wla wrh wb wi wi wph wps wka wla wrh wb wi wi wi eqEq.1 wph wps wka wla 

      wrh wb wi impexp mpbir wph wps wa wka wla wrh wb impexp mpbir wph wps wa 

      wka wa wmu wsi wb wi wph wps wa wka wmu wsi wb wi wi wph wps wa wka wmu 

      wsi wb wi wi wph wps wka wmu wsi wb wi wi wi eqEq.2 wph wps wka wmu wsi wb 

      wi impexp mpbir wph wps wa wka wmu wsi wb impexp mpbir bibi12d wph wps wa 

      wka wla wmu wb wrh wsi wb wb impexp mpbi wph wps wka wla wmu wb wrh wsi 

      wb wb wi impexp mpbi 

 $.

  $}

I tried exporting proofs in the compress format, but it is too much a bother (with floating hypotheses that don't appear in the labels + I got it working at 90% before I realized that metamath can read uncompressed proofs and compress them,
which is much easier to do. Besides, computing compressed proofs needs quite a lot of computations, and processing uncompressed proofs is a lot easier and faster for mephistolus...So, I gave up on compressed proofs.

Now, I should be able to export Mephistolus proof easily to the set.mm format and get them proofchecked by a battletested proof checker,in addition to my own.

[Olivier Binda]

I finally managed to export and proof-check in metamath the Mephistolus proof for 

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

To achieve that, I had to prove the following Mephistolus theorems in metamath : 

val Sum_CDI = tf("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 )", distinctRequirements = setOf("∨1s" to "∨0w", "∨1s" to  "∨5s", "∨2c" to "∨1s", "∨2c" to "∨5s", "∨3c" to  "∨1s", "∨3c" to "∨5s", "∨4c" to "∨5s", "∨5s" to "∨0w", "∨6c" to "∨1s", "∨6c" to  "∨5s", "∨7c" to "∨1s"))
val ApSumA = tf("sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = ( ∨5c + sum_ ∨1s e. ( ( ∨2c + 1 ) ... ∨3c ) ∨4c )", "∨2c e. ZZ", "∨3c e. ( ZZ>= ` ∨2c )", "( ∨1s e. ( ∨2c ... ∨3c ) -> ∨4c e. CC )", "( ∨1s = ∨2c -> ∨4c = ∨5c )")
val SumA_pA = tf("sum_ ∨1s e. ( ∨2c ... ∨3c ) ∨4c = ( sum_ ∨1s e. ( ∨2c ... ( ∨3c - 1 ) ) ∨4c + ∨5c )", "∨2c e. ZZ", "∨3c e. ( ZZ>= ` ∨2c )", "( ∨1s e. ( ∨2c ... ∨3c ) -> ∨4c e. CC )", "( ∨1s = ∨3c -> ∨4c = ∨5c )")
val Sum_CDV = th("( ∨0w -> sum_ ∨1s e. ∨2c ∨3c = sum_ ∨4s e. ∨2c ∨5c )", "F/_ ∨4s ∨3c", "F/_ ∨1s ∨5c", "( ∨0w -> ( ∨1s = ∨4s -> ∨3c = ∨5c ) )", distinctRequirements = setOf("∨1s" to "∨4s", "∨2c" to "∨1s", "∨2c" to "∨4s"))

I only pulled it off, thanks to the enlighted help of the kind metamath experts, who gave many hints (thanks :) )

In the process, I learned a lot and Mephistolus has grown a lot

So, let's say that Milestone 5 has been reached (I previously set too far goals for Milestone 5, let's be more realistic)
And let's go onward towards Milestone 6 :)