On Sat, Nov 21, 2020 at 8:11 PM David A. Wheeler <[email protected]> wrote:
> > > > On Nov 21, 2020, at 6:22 PM, Mario Carneiro <[email protected]> wrote: > > If there is enough interest from others that I'm not the only one on the > project, I don't mind taking the lead here. If it incorporates common code > from mm0-rs then that will be a good excuse for me to split it off to a new > project (the MM0 monorepo is getting pretty hefty) and maybe also expose a > library (depending on whether this new verifier is literally mm0-rs under > some settings or a separate executable that just links against a library > with common code from mm0-rs). > > > > That said, I am nearing the end of my PhD and probably shouldn't be > devoting large quantities of time to something that doesn't move my thesis > forward. :P > > :-). If there’s a way to combine them that’d be great. > > > In that case, a good first goal would be to determine what the features > of mmj2 *are*. Specifically, what features are actually used by people? > There are a lot of dead relics. The main ones that come to mind are: > > * unification (kind of a requirement for any proof assistant), > > * filling in a step given all the type info (and also showing all > matches in case some unification is possible), > > * as well as the more recent "auto step" proof search, which applies any > theorem matching some descent criterion (and not on a blacklist). > > Anything else? There are a bunch of options in the RunParms that do > stuff but I don't think any of them are really important (the definition > checker excepted but that's already on the todo list). There is some > documentation as well but it's a mixture of old stuff and new stuff and not > very well organized. This is probably something even the less technically > minded could help with. > > Unification with past/next steps, and unification given the name of an > existing theorem/axiom, are definitely minimums, but they’re also not too > challenging to implement. Those are the keys for me. That includes, when > specifying something, immediately creating its hypotheses & supporting work > variables (or something like them for identifying “don’t know yet”). > Yep, this is all what I would call "unification". When you apply a theorem, metavariables are created for all the variables in the theorem. The context against which the theorem is applied, or the known hypotheses being inserted into the application, yield equality constraints on the types, aka unification constraints, which are resolved by a unification procedure that assigns to the metavariables. MM1 does all of this from day 1. Important item: quietly reordering rules when the proposed order cannot be > unified but another order can be. The simple automation done by leading “!” > Is really helpful. The “replace this step by that step” e.g., “d1::#1” is > not used often but is very helpful when needed. > I didn't include in the list mmj2 solutions to mmj2 problems. Proof order is an mmj2 specific problem. If proofs are terms, then you are just passing terms around, and you just need to ensure that the term is not cyclic, which can be done as appropriate. Order of steps isn't really a thing until it actually gets "baked" into a MM proof. > Being able to double-click on any step & show what *could* be unified (and > what that would produce) is useful. I don’t use it as much as much you > might think. > In vscode, this is supported via autocomplete. You can write a _ anywhere in your proof and mm0-rs will supply the expected type; you can then use ctrl-space and it gives a list of theorems. I had always intended to support listing *applicable* theorems here, but I never got around to implementing it. > The runParms are mostly a pain, partly because it’s a nonstandard way to > do things. Usually you just pass a filename of the file to edit. Optionally > you use options lie -? Or --long_name, and/or an init file. > Yeah I don't see anything worth salvaging there. It's just a complicated way to set options. With MM1 style interaction you can load up your .mm1 file with configuration info, whether that info is standardized for everyone using set.mm or personal to you like a "worksheet" file would be. > > Actually, even if we branch off to a different editor mode, maybe it > would be good to support something roughly like mmj2 for "backward > compatibility" / getting people to use it earlier so they can speed up > development. > > I think that *would* be a good idea, especially if as much as possible it > were built on calls to a library. At least that would provide a familiar > alternative, and a reason to use it instead. Hopefully it would use a text > editor that can help pair parens :-). > I don't know if you have looked at mm1 proof scripts, but they are mostly linear, using the (f @ g x) notation liberally to make most arguments work out as a sequence of theorems with one hypothesis. Marnix would be proud. :) Because anything off the main-line requires extra parentheses for the subproof, several MM theorems had to be slightly changed to put the hardest hypothesis last, and there are even two theorems for "syl" which differ only in hypothesis order. theorem syl (h1: $ b -> c $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (a1i h1 )); theorem rsyl (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 h1); Usually, (syl T ...) is used to apply theorem T in a context, while (rsyl C ...) is used to apply a context manipulation theorem C (like simpl) to the context, changing it without changing the "goal". Even though they are the same theorem from MM perspective the linearization makes them "feel" rather different. 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/CAFXXJSucRe3qsZGG%2BMx5G4fVXRF%2BrcocWwxG2ofc-iYdoZE9QA%40mail.gmail.com.
