On Tue, Jul 23, 2019 at 11:31 AM vvs <[email protected]> wrote:
> On Tuesday, July 23, 2019 at 3:00:55 AM UTC+3, Mario Carneiro wrote:
>>
>> (By the way, did you notice the automatic definition unfolding? Sweet!)
>>
>
> What definition and where? MM1 or lisp? Can you give an example?
>
Here's a simple example:
def iff (a b: wff): wff = $ (a -> b) /\ (b -> a) $;
infixl iff: $<->$ prec 20;
theorem bi1: $ (a <-> b) -> a -> b $ = 'anl;
where
theorem anl: $ a /\ b -> a $;
In Metamath that proof would not work, because the goal is (a <-> b) -> a
-> b, not (a -> b) /\ (b -> a) -> a -> b. But MM0 has the notion of
unfolding definitions built in, and refine will automatically unfold
definitions in order to resolve a unification failure (in this case, and !=
iff). So that means that almost all definition unfolding is implicit,
although you will be able to unfold explicitly too using a "change" tactic
that says "this is my goal now, make sure it's the same as the current goal
up to unfolding definitions".
> BTW, there are a few other things that seem inconsistent to me. Some
> variables have no hovers in math block, e.g. ps in ax_3.
>
There was a bug in hover support for math blocks (note to self, don't
binary search an array unless it's sorted), but it should be fixed in the
latest version.
Also, variable names are not unified in hovers, so there could be
> ph->ps->ch in one place and b in another, e.g. in a1i. That means more
> mental calculation steps for user and is different from mmj2.
>
When you hover over a theorem statement, it displays (a pretty printed
version of) the source statement, with the source variables. So in this
case since ax_mp was stated with "ph" and "ps" you see it in the hover.
I'm thinking about adding a second hover that displays the "runtime type"
of the assertion, i.e. what we actually got from unification. For example,
if you hover over ax_1 in
theorem a1i (h: $ b $): $ a -> b $ = '(ax_1 h);
you would see
axiom ax_1 (ph ps: wff): $ ph -> ps -> ph $;
---------------------------
$ b -> a -> b $
and if you hover over syl in
theorem a1d (h: $ a -> b $): $ a -> c -> b $ = '(syl h ax_1);
you will see
theorem syl (a b c: wff): $ a -> b $ > $ b -> c $ > $ a -> c $;
---------------------------
$ a -> b $ > $ b -> c -> b $ > $ a -> c -> b $
This should go a long way to recovering a bit of the readability of mmj2
worksheets. (Another alternative for getting this style is a lisp command
like (explode 'a1d) that will display the proof in an mmj2 like style, with
steps and hypotheses and statements on every step.)
Another cosmetic problem: there is a MM0 traceback every time when some
> vscode settings are changed "haskell-lsp:no handler for. Object (fromList
> [("params",Object (fromList [("value",String "off")])),("method",String
> "$/setTraceNotification"),("jsonrpc",String "2.0")])".
>
I'm aware of this, but I haven't done anything about it because I am still
debugging the LSP server and I want to know if I get any unknown commands
from VSCode. "$/setTraceNotification" is a vscode-specific LSP notification
that is not in the specification, but the spec does say that you should
ignore $/ instructions you don't understand.
On Tue, Jul 23, 2019 at 4:37 PM David A. Wheeler <[email protected]>
wrote:
> there would need to be some sort of API that would at least let you (1)
> find current theorem state, and (2) allow you to apply/undo those options
> (and see the new state). Being able to find out "possible options" would
> be nice too.
>
Hm, I'm starting to second guess a decision I made about metavariable
representation now. Currently, metavariables are just mutable state, so
they start out as "expecting type T" and end up as "assigned to term foo".
This is done because metavariables can appear in many places, copied about
by unification, and it is much more efficient to update only one location
and have everything follow. But it makes undo tricky. The user can undo
easily by just writing something else, but that reprocesses the whole file
(for now) so it wouldn't be a good idea to do this in a tight loop (for
example trying a hundred theorems to see which work). Lean uses a more
functional style here, where tactics transform the state into a new state,
and you can just restore the original state and all those unifications are
undone, but it slows down straight line code, which is important for making
full MM1 file checking fast. (It probably still won't be fast enough to
check all of set.mm on each keypress, assuming it was all converted to a
similarly structured MM1 file, but I would like saved MM1 proofs to not
take much longer to run than the resulting MM0 proof takes to check.)
Instead, I think I will have (save-state) and (restore-state s) primitives
so that you can implement call/cc and try/catch on the lisp side. That
should allow this feature to not cause a performance penalty unless it's
being used. (For the particular case of unifying random theorems from the
library to see what sticks, I will have a separate, faster option using
temporary metavariables. But I will defer on this discussion until I have a
working prototype.)
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/CAFXXJSsToBk0h%3Dhkvss6c01THRSVS-UKPjGTh0pYJc7Pdq1FkA%40mail.gmail.com.
