I have finally written 3 parsers : - primary parser for mm0 files - dynamic parser for mm0 formulas - primary parser for mmu files
and a mm0-mmu proof-checker (thanks to the explanations of Mario). Though I believe it to be incomplete (it doesn't respect bound/unbound variables), it still proof-checks the mm0/mmu translation of set.mm in 15s. Once I fix things and cleans the code, I'll publish everything in this public repository, https://github.com/Lakedaemon/mm0-kotlin-tooling Now, the translation of set.mm to the mm0 format has : - 3 sorts (wff, setVar, class) - 1201 terms (basically the class/setVar/wff statements) - 1276 axioms (true axioms and all mm definitions) - 34946 theorems - 0 coercion (I was expecting a set > class coercion) - 0 simple definition (by adding those, you can customize the dynamic parser for your needs) - 0 definition (in there should go the mm constructs like { x | ph } ) - 0 input (I see how this is usefull for formalizing stuff but not for formalizing maths) - 0 output (same) - 0 comments (the "modification discouraged", "deprecated", "should not use" tags would be handy to have though) So basically, at the moment, it is possible to do mm-like work on mm0 but the set.mm.mm0 lacks the coercions/definitions/simple definitions to unlock all mm0 benefits Maybee I'll write a plugin for intellij idea to handle mm0/mmu files (no promise there, maybee it is too hard/complex/long/not needed for me). If I managed to write one and if it is nifty, I'll publish it too (in the same repository). I know that using visual code could allow me to do what I want, but I really do not want to use visual code (I love intellij idea though) and also it might not even be possible for me (I live in ubuntu land). Also, I would like to explore the possibility to have formalized theorems in mm0 of the kind if Context |- a= 1 and Context |- b = 2 then Context |- ( a + b ) = 3 where Context has any number of antecedents (0+). This would enable vararg antecedent -> stuff I need those for mephistolus (It allows having proof that are 2600 steps long instead of 1000000 single mm steps without compression) and I had to use (Mario-style ph->stuff) and implement mephistolus theorem on top of metmath theorem to get that. But maybee this is not necessary anymore in mm0 with a sort context Got to play with mm0 (or get Mario's advice) to see if it is possible Best regards, Olivier -- 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/240ea690-da52-4d75-8c27-30617e0d5f1c%40googlegroups.com.
