On Sat, Jan 9, 2021 at 1:15 PM Benoit <[email protected]> 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
--
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/CAFXXJStM3tAo0RaCxujMGghAtCO-y4Y-k9_eamtW3C092wZ28w%40mail.gmail.com.
