On Fri, Nov 27, 2020 at 1:17 AM David A. Wheeler <[email protected]> wrote:
> On November 27, 2020 12:14:09 AM EST, Mario Carneiro <[email protected]> > wrote: > step folding is also an option although I don't know how to make > >that not annoying. > > If it can be done easily without JavaScript, you should do it that way > instead. It's generally faster do to it that way, and it'd be nice to have > some functionality work when client-side JavaScript is disabled. There are > obviously diminishing returns where that doesn't make sense. > I'm not fussed about the technology used to achieve it, but my point is that if you use step folding you will be clicking on unfold icons all day to get through a 200 step proof. MM0 has a heavy linear sequence due to its use of @ , so perhaps we can fold steps off that linear path; the parenthesis nesting is usually only 3 or 4 (and often lower) except in some highly automated proofs, while the actual step depth increases linearly with the proof size (so it could be 20 or 30 for an average proof). > Basic text search is already built into browsers; I don't know if people > need more than that for searching. No? I use metamath's search function all the time when the web site can't help, and I guess URLs pretty often when metamath is not on hand. I'm talking about finding *theorems*, not steps. And anything with a fancy unification search isn't going to be usable with just browser search. Granted, the index page can probably be text-searched, but I doubt it will stay as one page forever; I think there are over 200 mmtheorems*.html pages. > > Another thing that is somewhat important for MM0 is > >"expr-folding", where subexpressions that are used in many contiguous > >steps > >(like the proof context) are abbreviated. MM/MM0 like to work with such > >expressions as they can be unified in constant time, but the standard > >metamath proof display format makes this look very repetitive (and it > >is > >also expensive to print), suggesting that somehow the print isn't > >capturing > >"the essence of the proof" because it appears to be more repetitive > >than is. > > A fair point. The metamath proof display has this problem also. > > In some texts you would show at the beginning some definitions to make > notation simpler, followed by the text that uses it. Perhaps you could > automatically detect sequences of symbols of a certain length that get > reused more than a certain number of times, give them special symbols, and > put them at the top as shorthand definitions. E.g., $1, $2, and so on. Each > list would be local to a particular theorem. They could even other > shorthand definitions. I don't know if that would actually help, but I'm > throwing it out there as an idea. > My idea is that the user selects a target step and a "width" (a configurable constant, say 10), and then all subexpressions that are not "destructured" in the steps which are less than distance 10 from the chosen point along the graph are abbreviated. (In other words, this is what you would get if you wrote all those steps in mmj2 without the formulas and let it find them by unification.) If you consider all the steps, you probably won't get any abbreviations, but the more "local" you make it the more aggressively it will shrink terms. This will require the pretty printer to be in JS, though. Interestingly, this actually more closely reflects the way the proof author sees the proof they wrote; the author sees metavariables for the unwritten parts and they only go away gradually as they complete the proof; if you go back and look at the completed lines they are less readable then they were when the author looked at that same line. 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/CAFXXJSunUaLksj4PMz%3DRee37H5uCzPGoP%2BHf3E1Dzp-vGM%2BaOw%40mail.gmail.com.
