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 :)
Le lundi 4 novembre 2019 20:15:44 UTC+1, Olivier Binda a écrit :
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.
>
>
>
>
> Le vendredi 18 octobre 2019 11:21:25 UTC+2, Olivier Binda a écrit :
>>
>> 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 ^^;
>>
>
--
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/3bbb9d3c-a7a6-43b4-99dc-ed8b6c8675c8%40googlegroups.com.
