MM0/MM1 tutorial

[Mario Carneiro]

Hi All,

I've finally gotten around to writing a tutorial on MM0 and mm0-rs for the lean together conference this year. Perhaps it will help situate it with respect to other metamath-based theorem provers in terms of feature set.

https://www.youtube.com/watch?v=A7WfrW7-ifw

Mario

[Benoit]

That's a very nice introduction (although a bit fast for me when describing tactics).  I like the explicit dichotomy between the proof assistant, that may be large with many features, versus the proof verifier, that has to be minimal.

I was wondering how "delimiter" works.  Can there be middle delimiters ?  For instance, if I want to allow expresions like {x|ph}, should I write

  delimiter ${$ $|$ $}$;

or

  delimiter ${ |$ $} |$;

Secondly, is it one line per matching pair of delimiters or a single line for all of them:

  delimiter $($ $)$;

  delimiter $[$ $]$;

versus

  delimiter $( [$ $) ]$;

Probably the latter, considering your example

  delimiter $( ~$ $)$;

And lastly, can I have multi-character delimiters like

  delimiter $\[$ $\]$;

or the even more ambiguous

  delimiter $(( ($ $)) )$;

I understand that the tokenizer puts an implicit space after every left delimiter and before every right delimiter, but in the last case I am not sure what it does.

Compared with Metamath, the "|-" type has been replaced with the "provable" qualifier.  I am not sure I see all the implications.  For instance, Metamath has to prove that longer expressions are well-defined, e.g. it has to prove "wff ( ph -> ph )" before proving "|- ( ph -> ph )" (it does it implicitly in the non-essential steps, but this can be made explicit, see e.g. http://us.metamath.org/mpeuni/bj-0.html).  How does this translate in MM0 ?

A smaller thing: I would have said that the opposite of "public" is "private", not "local", but there might be a reason why you chose the latter term ?

Thanks,

Benoît

[Mario Carneiro]

On Sat, Jan 9, 2021 at 1:15 PM Benoit <benoit...@gmail.com> wrote:

That's a very nice introduction (although a bit fast for me when describing tactics).  I like the explicit dichotomy between the proof assistant, that may be large with many features, versus the proof verifier, that has to be minimal.

I was wondering how "delimiter" works.  Can there be middle delimiters ?  For instance, if I want to allow expresions like {x|ph}, should I write

  delimiter ${$ $|$ $}$;

or

  delimiter ${ |$ $} |$;

The second one. Characters can be in both lists, and in that case any token containing a | will always be a token on its own and split the surrounding token cluster.

 

Secondly, is it one line per matching pair of delimiters or a single line for all of them:

  delimiter $($ $)$;

  delimiter $[$ $]$;

versus

  delimiter $( [$ $) ]$;

Probably the latter, considering your example

  delimiter $( ~$ $)$;

Both versions work. I prefer to put all my delimiters in one command at the start of the entire development (fixing them once and for all for a given axiomatization), but you can use the delimiter command multiple times to add more left or right delimiters later, although there is no command to remove delimiters that have been set. This affects the math parser as soon as it is read, so expressions will treat it as not a delimiter before the command and then it becomes a delimiter afterward.

And lastly, can I have multi-character delimiters like

  delimiter $\[$ $\]$;

or the even more ambiguous

  delimiter $(( ($ $)) )$;

I understand that the tokenizer puts an implicit space after every left delimiter and before every right delimiter, but in the last case I am not sure what it does.

This was an early design point in MM0, and the reason why the internal spaces are mandatory in the left/right delimiter lists, but it turns out that the theory of multi character delimiters is quite complicated and I don't think it's appropriate to require MM0 verifiers to have to deal with it. So currently every MM0/MM1 verifier will complain if you use multi-character delimiters, with some message that implies that it may be supported in the future.

Compared with Metamath, the "|-" type has been replaced with the "provable" qualifier.  I am not sure I see all the implications.  For instance, Metamath has to prove that longer expressions are well-defined, e.g. it has to prove "wff ( ph -> ph )" before proving "|- ( ph -> ph )" (it does it implicitly in the non-essential steps, but this can be made explicit, see e.g. http://us.metamath.org/mpeuni/bj-0.html).  How does this translate in MM0 ?

In fact, metamath *doesn't* have to prove that. You can prove a nonsense version of idi like $e |- -> ph ps $p |- -> ph ps $., even in set.mm and you will get no complaints from metamath, although the grammatical parser in mmj2 will notice that there is no parse for these expressions so the overall CI will fail, but that's all just unofficial extensions on the metamath spec. It is true that in practice, we want every $e and $p statement of the form |- ph to imply that wff ph is provable, but there is nothing in the metamath spec that requires this, and even figuring out which typecode to expect here requires some explicit $j annotations.

 

The MM0 version bakes this into the system with "provable sort". Every hypothesis and axiom must be parsed (and the parse is part of the proof file) to show that it is some provable sort. Note that there can be multiple provable sorts; it's not very useful for set.mm but this is one way to represent a system with multiple provability judgments in it (for example the mutually recursive typing and definitional equality judgments of dependent type theory).

A smaller thing: I would have said that the opposite of "public" is "private", not "local", but there might be a reason why you chose the latter term ?

"Private" I think gives the wrong idea, because in particular if you have a big development spanning many .mm1 files you might think that privacy means something, and it doesn't - you can refer to any theorem or def in any later file, there is no modularity or information hiding at this level. Maybe a better naming would be something like "main theorem", since that reflects better the sense in which this is exposed. "extern theorem"? Eh, now it sounds like it doesn't happen here but is getting proved elsewhere.

Mario