Calculational rendering of Metamath proofs, using Greasemonkey/Firefox

[Marnix Klooster]

Hi all,

For quite a while I've been looking into different ways to render Metamath proofs-- and Thierry's rendering experiments (which look great!) inspired me to do some experiments in JavaScript.

To allow me easy experimentation, I've chosen to use Greasemonkey on Firefox.

To use this, you need to install the Greasemonkey add-on (https://addons.mozilla.org/en-GB/firefox/addon/greasemonkey/), and then open or install my script from https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc.user.js .  (I think your Firefox Greasemonkey should auto-update when I change this script the correct way, but I'm not sure yet.)

(Caveat emptor: For any Greasemonkey script you run, make sure you get it from a trusted source, and analyze the source code if you're not sure.  The above script runs with no special permissions.)

The goal of this script is to make a proof look more like a 'calculation', which (for me at least) usually makes them easier to follow.  For example, try it on http://us.metamath.org/mpeuni/ru.html or http://metamath.tirix.org/ru.html (with all steps expanded).

The current version of this script only re-indents the formulas in a way that makes more sense to me than the usual tree structure.  (Tested on metamath.org Gif+Unicode and metamath.tirix.org.)

I have ideas for other changes/improvements, but I have no idea whether I will have the time...

Anyway, feedback welcome, and enjoy!

Groetjes,

 <><

Marnix

--

Marnix Klooster
marnix....@gmail.com

[Thierry Arnoux]

Hi all,

Because not everybody has Firefox and Greasemonkey, I've included Marnixes scripts on my pages.
You can switch to this indentation by clicking the "M" on the top right of the proof tables (you have to reload page to switch back to the original display).

Marnix, you did not provide much explanation, could you tell how it's working?

BR,
_
Thierry

[fl]

There is something sociologists call the bias of confirmation: we always choose the data that work well with what we want to prove.

Try your algorithm on a page where the steps are numerous, the indentations are deep and, the formulas are long.

Those pages are numerous in set.mm

-- 

FL 

[Norman Megill]

Your comment provides no information and is not helpful.  Please provide examples of pages that you are talking about, and describe what you think the problems are and how they could be improved.

Norm

[Marnix Klooster]

(Forgot to include the group...)

Hi Thierry,

Thanks for including, and so quickly! :-)

What that indentation algorithm does, is take a tree like

  2: F

      4: E

    3: D

    3: C

  2: B

1: A

and make it look like a calculation, by indenting the first parent/antecedent of a step the same as the step, the second one level deeper, etc.:

2: F

  4: E

  3: D

    3: C

  2: B

1: A

This is intended to match the following calculational proof:

    F

==>  "by sub-proof"

         E

     ==>

         D

     ==>  "by C"

         B

    A

I'm trying to update my Greasemonkey userscript to collapse/expand on the granularity of such calculations and sub-calculations, and to render proofs more and more in this form.

Even with the current limited indentation form, with basically your (Thierry's) expand/collapse, a number of proofs start to be actually a bit readable to me. :-)

And yes, a large proof will still indent quite a lot, and my indentation size might a bit too large-- but still for me it is an improvement on the standard metamath /html format.  I think that my algorithm actually indents less than the original format...

Groetjes,

 <><

Marnix

--

Marnix Klooster
marnix....@gmail.com

--

Marnix Klooster
marnix....@gmail.com

[Raph Levien]

I'll point out that this is the same indentation scheme as used (by convention) in (Python) Ghilbert proofs, and with the same motivations.

Regarding indentation depth, it becomes something you can optimize for. For example, "A B C 3bitri" can become "A B bitri C bitri". I personally tend to prefer the latter and feel that it's more of the "calculational style".

Raph

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

I'll note that triple inferences like 3bitri can be expanded into bitr*i references with the command "expand 3bitr*i" in MM-PA, then the proof saved and displayed.  We probably want to keep the original 3bitr*i in set.mm, though, because they result in shorter proofs.

Norm

On Wednesday, June 6, 2018 at 1:12:44 PM UTC-4, Raph Levien wrote:

I'll point out that this is the same indentation scheme as used (by convention) in (Python) Ghilbert proofs, and with the same motivations.

Regarding indentation depth, it becomes something you can optimize for. For example, "A B C 3bitri" can become "A B bitri C bitri". I personally tend to prefer the latter and feel that it's more of the "calculational style".

Raph

Hi Thierry,

[Marnix Klooster]

Hi Norm,

Thanks for introducing me to that 'expand' command, I didn't know about that, very helpful for uses like this!

Note (but that should be a separate thread probably) that personally I don't understand where the emphasis on shorter proofs comes from.  My goal is to have _clearer_ proofs, and mostly I find "macros" like 3bitri hinder readability than they help.  But that may be my 'calculational upbringing'. :-)

And I just realized a simpler way to express my (and Ghilbert's) indentation algorithm: indent each step by the size that the proof stack has, after applying the step.

Finally, I've put a @version 3 of my Firefox Greasemonkey userscript at the same location (https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc.user.js).  Re-install seems required.

New features: expand/collapse at the (sub-)calculation level; antecedent highlighting, both copied from Thierry.  Visually ugly, but works for my current purposes.

Enjoy!  (And/or complain. :-) )

Groetjes,

 <><

Marnix

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--

Marnix Klooster
marnix....@gmail.com

[David A. Wheeler]

> >> 2018-06-06 16:34 GMT+02:00 Thierry Arnoux:
> >>> Because not everybody has Firefox and Greasemonkey, I've included
> >>> Marnixes scripts on my pages.
> >>> You can switch to this indentation by clicking the "M" on the top right
> >>> of the proof tables (you have to reload page to switch back to the original
> >>> display).

All of this is really cool. A few kibitzes to improve it further:
* If you have an "M" to emphasize indenting, there should be a way to undo it.
* The vertical space in each step is excessive for ru (Russell's), since it only has
forall, x, etc. Can you reduce that so you can see more steps at one time?
* The various actions need some tooltips so that you can more easily
determine what they do. That way, you can hover over the "M"
(or whatever) on a laptop to find out what it does.
* In the longer term, it might be nice to support specifying
steps to show or hide by default to override the
algorithm that selects the "important" steps. No algorithm is perfect!
Obviously the steps that are important can change if
the theorem changes, but usually when theorems change the number of
steps changes, so we normally could avoid accidentally applying such directives
by noting the "number of steps expected" and ignore the directive if it's
the wrong count. E.g., the comment text could say:
Important steps (out of 17) include 10, 12, and 14.
Unimportant steps (out of 17) include 1 and 2.

--- David A. Wheeler

[Raph Levien]

Yes, that's exactly the way I expressed this in Ghilbert - indentation level is stack depth at the end of the line. This is maybe subtly different in Ghilbert because the format encourages multiple steps per line. I'd very often end a line with a "reduce" step that integrates the line with the rest of the calculation, often some variant of ax-mp, syl, bitr, eqtr, or (more advanced) pm2.61. To me, this started to get into almost a linguistic structure, such a step would signal the end of a "phrase", and perform a function not entirely unlike a particle in Japanese.

Regarding things like 3bitr, I'm not saying they should be mechanically expanded, I'm saying that optimizing for cleanest presentation (especially with this indentation strategy) might lead you to a different result than, say, optimizing for the minimum number of proof steps (which seems to be the default assumption in MM).

R

[Marnix Klooster]

Hi all,

Yesterday I got tired of manipulating the existing HTML proof tables in my Greasemonkey script, so I hacked up 'mm-calc2' which more directly renders to the proof format I have in mind, leaving the original proof table untouched.  Get it at https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc2.user.js.  Above each proof table, it renders a calculational equivalent of the table.  It currently also works on metamath.tirix.org.

Try it, for example, on http://us.metamath.org/mpeuni/eulerth.html and http://metamath.tirix.org/eulerth.html.  Or on http://us.metamath.org/mpeuni/ru.html and http://metamath.tirix.org/ru.html.

This initial version of mm-calc2 does not yet do collapse/expand, and it just shows both formats at the same time.  So it will look not look too good on large proofs-- but I'd argue the table format is not easier to understand for large proofs anyway. :-)

Also, it has a bug in that it doesn't show reused steps correctly.  (For example, in http://us.metamath.org/mpeuni/pm5.54.html, the second reference to step 2 / bicomd is missing.)

But despite these restrictions, it already helps me read some proofs more easily, especially with the formatting on metamath.tirix.org.

And for the future this gives me a kind of 'test bed' to try different orderings of the same calculation, e.g. using a chain of <== instead of ==>, choosing not the first antecedent but a different one, or even using set.mm operators like <-> and = in the left hand column, instead of just the 'meta-implications' ==> and <==, and removing repetition by extracting common contexts like this:

In context ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ...) we have

	(1...(ϕ‘𝑁)) ≈ {𝑘 ∈ (0..^𝑁) ∣ (𝑘 gcd 𝑁) = 1}
⇒	“using sylib 189 and bren 7108”
	∃𝑓 𝑓:(1...(ϕ‘𝑁))–1-1-onto→{𝑘 ∈ (0..^𝑁) ∣ (𝑘 gcd 𝑁) = 1}

Again, no idea when I'll continue work on this, feedback welcome.

Groetjes,

 <><

Marnix

--

Marnix Klooster
marnix....@gmail.com

[fl]

- What confuses me: The collabse/expand. Why should
   I need that when I can sroll the window content?

The collapse/expand interface may be useful when you want to reduce the quantity

of displayed information. For instance if you have a theorem 1 and 3 premisses 5 7 9 you could

have only a table like

9 | ...     | a line of ymbols

7 | ...     | a line of ymbols

5 | ...     | a line of ymbols

1 | 5 7 9 | a line of ymbols

Easier to read.

Then if you want to know how to prove the step 9 you expand it and a page like 

18 | ...     | a line of ymbols

13 | ...     | a line of ymbols

9 | 13 18 | a line of ymbols

appears.

But well you need to use the arrow keys instead of the mouse with such an interface otherwise

the carpal tunnel would suffer.

-- 

FL

[fl]

Ok I see this navigation is already available,
you can check here:
http://metamath.tirix.org/risefacval.html#6

Yes this is not bad. But the proof is short. How could you use that with a long proof since you must put the mouse on
a step so that the premisses get enlightened. The enlightment must be sticky.

--
FL

[fl]

Basically I would be more intrested in an ability to click on
symbols than to click on hypothesis. Like clicking on the
word RiseFac and getting automatically transported to

its definition. These symbol clicks would be something
new. I just see that the original proof without any
collapse/expand has already hypothesis links.

No clicking. Clicking is the worse interface in the world.

To show the definitions of the symbols, I'd rather have a hoovering window.

--
FL

[Thierry Arnoux]

Hi all,

I've setup a Git repository with the web-based UI additions for Metamath
proofs: https://github.com/tirix/mm-web-ui
This shall help to track both issues and code changes.

I've also included there the first version of Marnixes script for
re-indentation of the proofs.

You all have raised many comments/issues/wishes about the display, thank
you for that!
I've tried to list the issues already mentioned in the mailing list:
https://github.com/tirix/mm-web-ui/issues
Feel free to add more/comment there! Some may still be missing.

Note that these scripts (highlighting, collapsing, etc.) are rather
generic could also be applied to the "Unicode" version of the pages, too.
(though "Copy to clipboard" requires additional information in the
generated HTML pages)
BR,
_
Thierry

[Thierry Arnoux]

Hi all,

For those who don't follow the Github repository: I've made several changes on the scripts for displaying proofs (mm-web-ui) during the last few days:

• keyboard based browsing is supported (#4). Move up/down with the up/down arrow keys, expand with the left arrow key, collapse with the right arrow key (you still need to hover on the proof to initiate : I need to add that).
• step highlighting is now "sticky" (#7): the step stays highlighted even if you move the cursor out of it
  
• colors are softer (#3), the rows are not colored alternatively anymore (#10). Though, colors are really a matter of taste...
  
• as an experiment, only in ~birthday, (some) tokens in the formulas are clickable, and link to their definitions. This currently requires adding the links directly in the rules file (I've committed the changes in set.mm), but this is probably not a very good solution since it would require to keep the file aligned with the labels of the definitions if they were to change. A solution which dynamically inserts the right definition label in the link might be a better alternative... but will be more complex.
  

BR,
_
Thierry

[Mario Carneiro]

I'm not sure I understand the concern with the links in birthday. If the labels change, it seems reasonable that the syntax file will also change. As long as it isn't referring to pages like mmtheorems179.html it should be fine. I think that the links are presented well - they are not visible unless you mouse over them, and they all seem to go to the right places.

Mario

[Thierry Arnoux]

My concern was about duplication of information, and the additional maintenance cost. But these definition shall not change often, so it’s indeed probably not worth the additional effort.

I’ll go on and add these links to all symbols. 

This will increase (again) the resulting HTML file sizes, but I think it’s worth it.

Note that for several commonly used constructs like ( A ^ B ) (A to the power of B), there is no displayed symbol to add the link on. For those, the list of definitions at the bottom of the page is still available.

_

Thierry

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Norman Megill]

There are no precedence tables in the Metamath language nor any way to specify left or right association.  There is no way to make /\ bind tighter than ->, and parentheses are used to determine grouping as well as left or right association.

In general, prefix operators bind more tightly than infix operators.  For example, ( A. x ph -> ps ) means ( ( A. x ph ) -> ps ) and not ( ( A. x ) ( ph -> ps) ) as it does in some conventions.  Infix operators resulting in wffs but whose arguments are not wffs usually omit parentheses since there is no ambiguity; for example, ( x = y -> ph ) means ( ( x = y ) -> ph ).  Otherwise, parentheses are used to disambiguate and to show association.  (There are no postfix operators in set.mm.)

Whether parentheses are needed around, say, x = y is specified by the syntax definition.  We typically omit them when there is no ambiguity as in this case.  For infix operators such as -> whose arguments and result are all wffs, we must specify parentheses in the syntax definition in order for parsing to be unambiguous.

If the syntax of an infix operator is specified to use parentheses, then it must always have parentheses, even when they are the outermost parentheses who omission causes no ambiguity.  So we must say "( ph -> ps )" instead of "ph -> ps".

The standard web page display shows the sequence of symbols directly translated from their ASCII tokens, with no effort made to do things like strip outer parentheses.  This is done purposely so the reader can see the exact sequence of symbols used in the database, in order to eliminate any guesswork.  A more advanced reader who doesn't want to be so pedantic can use Thierry's pages, which omit many parentheses and use conventional groupings.

Norm

On Tuesday, January 8, 2019 at 4:42:31 PM UTC-5, j4n bur53 wrote:

I have a question concerning the unicode rendering
and metamath in general. Lets look at this rendering:

   ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
   http://us.metamath.org/mpeuni/sbth.html

Do operators in metamath have some operator
precendence? My expectation was that I would see:

    𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 → 𝐴 ≈ 𝐵

In case this was already asked, sorry for duplicate post.

[Norman Megill]

Everything is verbatim, including the proof steps.

Norm

On Wednesday, January 9, 2019 at 12:49:33 PM UTC-5, j4n bur53 wrote:

So the operator precedence is derived from the
arity, the type and the argument types.

And http://us.metamath.org/mpeuni/sbth.html shows the theorem verbatim.
But I guess verbatim does not hold for the proof. Or do the proofs take
lemmas also verbatim, and even substitute verbatim?

[Norman Megill]

You may be interested in Mario's analysis:  http://us.metamath.org/downloads/grammar-ambiguity.txt

There is nothing in the Metamath language per se that defines its grammar.  The grammar is completely determined by the $a statements that introduce syntax constructions.  The current grammar, which requires an LALR(7) parser, was (mostly) chosen by me to be what I thought was similar to textbook notation and relatively human-friendly, within the constraint of unambiguous parsing.

Sometimes I have wondered if it would have been better to choose a simpler grammar, for example Polish prefix or S-expressions.  That would be more in keeping with Metamath's spirit of simplicity.  But I think it would be harder to work with directly in the .mm file, and we would need a translator to reformat expressions for the web pages to make them palatable for most readers.  Right now we display the symbol strings exactly as they appear in the .mm file, after converting the ASCII tokens to corresponding math symbols (which are determined by the htmldef and althtmldef statements in the set.mm comment starting with "$t").

(As I mentioned, Thierry has written a more human-friendly translator for set.mm expressions - that was the original topic of this thread.  Its output can be accessed with the "structured version" link at the top right of each theorem's web page.)

Nonetheless, if someone does prefer an alternate notation in set.mm, it would be straightforward to do so.  All that is needed is a parser to convert the existing formulas to Polish prefix or whatever, then replace the existing formulas with the new ones.  No conversion would be needed for the proofs, which would remain exactly the same.  That such a conversion could be done relatively easily is a motivation to stay with a more human-friendly, if more complex, grammar.

For an example of what Polish prefix would look like, see Bob Solovay's http://us.metamath.org/metamath/peano.mm.

Norm

[Thierry Arnoux]

Hi Jan,

The "structured" rendering is actually using MathJax, which is the software which provides the contextual menu you mention (just look at the last line of the menu, it says "About MathJax").

However MathJax is slow when rendering big amounts of mathematics, and it took tens of seconds to render a single page, so I switched to off-line rendering: the "Structured" pages are rendered into a static format, SVG, and the contextual menu is lost in the process. SVG is also the reason why text selection is not possible: you have the same result if you choose "Math Settings/Math Renderer/SVG" in the contextual menu in Math Stack Exchange: the math becomes unselectable.

As you point out, as a commodity, the original Metamath "source" is shown when hovering over the formulas, and it's possible to copy that "source".

_
Thierry

On 13/01/2019 06:25, j4n bur53 wrote:

I just tried now. Structured view doesn't use right click mouse
event for anything. Shows the usual browser menu.

Oki Doki

Am Samstag, 12. Januar 2019 23:23:18 UTC+1 schrieb j4n bur53:

Concerning the disabled mouse select for copy. MSE has
an elegant solution. You can right click mouse on some
math text, and it shows you a menu:

    Show Math as
    -------------------
    Math Settings ...
    ....

And Show Math as is a submenu:

    MathML Code
    Tex Commands
    ...

I am using this quite frequently. Tex Commands opens a little
window, and I can still decide whether I copy it, or only copy
a part of it whatever. Just take any MSE page to play with it:
https://math.stackexchange.com/q/3071418/4414

Am Samstag, 12. Januar 2019 23:16:00 UTC+1 schrieb j4n bur53:

Oh its now possible to click on symbols, and get
to the defintion, thats great!

Am Samstag, 12. Januar 2019 23:13:47 UTC+1 schrieb j4n bur53:

The structured view does eliminate some parenthesis:

Normal view:
⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∉ 𝑥) → (𝑦 ∈ 𝑦 ↔ ¬ 𝑦 ∈ 𝑦))
⊢ ({𝑥 ∣ 𝑥 ∉ 𝑥} ∈ V ↔ ∃𝑦 𝑦 = {𝑥 ∣ 𝑥 ∉ 𝑥})
http://us.metamath.org/mpeuni/ru.html

Structured view:
Its shown without the outer parenthesis
Its shown without the outer parenthesis
http://metamath.tirix.org/ru.html

But it cannot do my initial example:

Normal view:
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
http://us.metamath.org/mpeuni/sbth.html

Structured view:
Its shown without the outer parenthesis,
but the parenthesis around the conjunction are still there
http://metamath.tirix.org/sbth.html

I cannot show here what the structured view shows,
since the HTML has mouse selection disabled(*) for
the corresponding HTML divs.

(*)
BTW: I guess it uses:
https://stackoverflow.com/a/52457561/502187
Was too lazy to use web browser debug and CSS liveedit
to enable it. Why is this disabled, doesn't make any sense
if there is anyway a copy button for the metamath original?
Some copy right fear?

--

[Thierry Arnoux]

Hi Jan,

There are two issues to overcome to achieve that:

• As for getting the text when you copy/paste it: I've experimented a bit with alternate texts for embedded SVG, and I did not immediately find a way to get that text copy/pasted like for linked (SVG) images. Alternate texts in SVG are provided by embedding the <title> element, but then it does not get copy/pasted. Do you know how this can be done?
• The flat unicode version of the formula is typically MPEUNI, and right now the program generates the MathML/SVG formula, not the Unicode one (there is a switch to choose one or the other). To get the unicode version (=MPEUNI), I'd typically need to run another generation pass for the formulas. The metamath source which is provided right now is much easier to get.

BR,
_
Thierry

On 13/01/2019 21:49, j4n bur53 wrote:

Ok, I didn't notice its SVG. Isn't it possible to attach an alt text
to the canvas that can be copied, which would be a flat
unicode version of the rendered formula?

When I copy HTML text and it has an img tag with alt
attribute, I usually see the alt text as plain text.
Something like that.

[David A. Wheeler]

On Sat, 19 Jan 2019 09:53:21 -0800 (PST), j4n bur53 <burs...@gmail.com> wrote:
> I just wanted to start using regularly the structured view.
> Like posting links to the structured view, instead of the
> old view. Here is a little bug:
>
> It shows me a strange text:
>
> ...
> *Note*: the natural numbers are a subset of the ordinal numbers
> ?Error: NN ^^ This math symbol is not active (i.e. was not declared in this
> scope).
> ...
> http://metamath.tirix.org/df-om.html

This seems to be triggered by a reference to ~ df-on ; here's the source text:
_Note_: the natural numbers ` om ` are a subset of the ordinal numbers
~ df-on . They are completely different from the natural numbers ` NN `

But df-on is defined, so I don't know *why* the generation is failing. Thoughts?

--- David A. Wheeler

[Thierry Arnoux]

Hi,

Very good catch!

This is most likely due to the ` NN ` in the comment.

When displaying math in comments, the "Structured" output tries to parse the formula, assuming it is a valid one. However the symbol ` NN ` is declared after ~ df-om, so the string ` NN ` is not a valid Metamath formula at that point of the set.mm file (Metamath has a way to check this by giving the "stateNum", the statement number beyond which it shall not search for symbols - that is in the function "parseMathTokens" I use). this triggers the warning.

However this shall not be relevant when parsing comments: in comments, it is not rare to make forwards references like this, and this shall be accepted. When parsing comments, I shall pass "statements", the total number of statements, as "stateNum", so that there is no restriction in the valid tokens.

I've fixed the issue and re-launched a generation of the pages (this takes a lot of time, please be patient if you still find the same issue in the coming days!).

BR,

_
Thierry

PS. This also reminds me I shall take the time to share the code for the generation!

[Thierry Arnoux]

Hi Jan,

About the display of the function value F(x): yes, this is one of the advantages of “structured” typesetting, formulas can be displayed in an (even) friendlier way.
There is a table with different display improvements at the bottom of this page:

http://metamath.tirix.org

About the text in red in the comments, this is again because the formula could not be parsed as a well-formed formula. In this case, the parentheses are missing around the implication -> statement. That’s a generic issue with comments: the formulas embedded in comments are often not well formed.

BR,

_

Thierry

Le 24 janv. 2019 à 04:14, j4n bur53 <burs...@gmail.com> a écrit :

Its red here:

={<.2,6>.,<.3,9>.}->( `3)=9
(A)
  iota
http://metamath.tirix.org/df-fv.html

Am Mittwoch, 23. Januar 2019 21:12:05 UTC+1 schrieb j4n bur53:

Just made a funny discovery. Structured view changes F'A to F(A).
But I guess the red rendering here indicates some problems:

http://us.metamath.org/mpegif/df-fv.html

[Mario Carneiro]

I think metamath really needs an online search feature, but the metamath website is a bit too web 1.0 for that to work. I recall Stefan O'Rear had a javascript verifier that could potentially do this, but that is more of a webapp rather than a server interface, and I don't know if it got to practical usability level.

On Fri, Feb 1, 2019 at 7:11 AM j4n bur53 <burs...@gmail.com> wrote:

What would be great, would be a free text search that can also
search symbols. Like Symbolhound:

   SymbolHound is a search engine that doesn't ignore special characters
   http://symbolhound.com/

Most search engines, their index crawler and query processing
are configured that they only search alphanum.
So you need to have a custom search engine, if you want
to have better recall and precision for text that

contains symbols.

Disclaimer: Again the above link doesn't imply any endorsment
of symbolhood. Just to make a case.

Am Freitag, 1. Februar 2019 13:07:56 UTC+1 schrieb j4n bur53:

Does metamath have a free text search. Like Solr or something
like that. Since recently I guess Google has updated their search
and its not anymore possible to find metamath theorems via

Google search. They only show main entry, and a book by
Chaitin which happens to have the name meta math in it.
So metamath has become less usable.

Apache Solr
https://en.wikipedia.org/wiki/Apache_Solr

Disclaimer: I am not endorsing apache solr. I posted only the link
to explain what I am missing, some free text search, since recently
Google changed their ranking.

[Norman Megill]

This works for me:

site:metamath.org omega

Even symbols can be searched e.g.

site:metamath.org (∃!𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥𝜓))

Norm

On Friday, February 1, 2019 at 7:16:51 AM UTC-5, j4n bur53 wrote:

I also don't see NOINDEX in the pages or some such.
So I guess the pages are not to blame. Roibots txt
seems also ok, nothing that would prevent indexing.

Right?

Symbolhound gives me:
0 results found for ALL OF: omega | FROM SITE: matemath.org

Am Freitag, 1. Februar 2019 13:07:56 UTC+1 schrieb j4n bur53:

Does metamath have a free text search. Like Solr or something
like that. Since recently I guess Google has updated their search
and its not anymore possible to find metamath theorems via

Google search. They only show main entry, and a book by
Chaitin which happens to have the name meta math in it.
So metamath has become less usable.

Apache Solr
https://en.wikipedia.org/wiki/Apache_Solr

Disclaimer: I am not endorsing apache solr. I posted only the link
to explain what I am missing, some free text search, since recently
Google changed their ranking.

[Norman Megill]

I went to https://search.google.com/search-console, and Google gave me a file to upload to http://us.metamath.org.  I did that, and it said the site was verified.  However, it said "Processing data, please check again in a few days" so I'll have to come back later.

Norm

On Friday, February 1, 2019 at 7:20:36 AM UTC-5, j4n bur53 wrote:

If you are the owner of metamath.org, you can place a certifcate
on the website and then go to:

https://search.google.com/search-console

And check what the crawler does. Whether there is some problem.

Am Freitag, 1. Februar 2019 13:16:51 UTC+1 schrieb j4n bur53:

I also don't see NOINDEX in the pages or some such.
So I guess the pages are not to blame. Roibots txt
seems also ok, nothing that would prevent indexing.

Right?

Symbolhound gives me:
0 results found for ALL OF: omega | FROM SITE: matemath.org

Am Freitag, 1. Februar 2019 13:07:56 UTC+1 schrieb j4n bur53:

Does metamath have a free text search. Like Solr or something
like that. Since recently I guess Google has updated their search
and its not anymore possible to find metamath theorems via

Google search. They only show main entry, and a book by
Chaitin which happens to have the name meta math in it.
So metamath has become less usable.

Apache Solr
https://en.wikipedia.org/wiki/Apache_Solr

Disclaimer: I am not endorsing apache solr. I posted only the link
to explain what I am missing, some free text search, since recently
Google changed their ranking.

[David A. Wheeler]

It is possible to implement a search engine, but it is a non-trivial effort. It is much better to make publicly available search engines happy than to build our own. Google has mechanisms like site:metamath.org to limit results to particular sites.

If searches are not finding the site, it might be good to ask why. I have a speculative idea, it may be that there is only HTTP. Google has been warning people for years that it downgrades sites that only support HTTP, because modern sites should be supporting https. I have no idea if that is really an issue, but it might be something to check out.


--- David A.Wheeler

[Thierry Arnoux]

Hi Jan,

The comment of ~df-fv seems to explain the origin and choice for the notation of the value of a function:

The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26.  It means the same thing as the more familiar ` F ( A ) ` notation for a function's value at ` A ` , i.e.  " ` F ` of ` A ` ," but without context-dependent notational ambiguity.

From this sentence, I believed the choice was made based on the ease of parsing. The notation ( F ` A ) is probably better known to logisticians, but the notation ` F ( A ) ` should be more familiar to many, as it was the case for me when I started reading Metamath proofs, so it was the one I chose for the structured view. The structured view has no added value for the first chapters set.mm, including logic, but it should help when more complex notations are introduced, where the notation F(A) is the norm.

Are there cases where this is a problem?

_
Thierry

[Mario Carneiro]

For that syntax tree to work, the notation (ph |-> B) would have to mean something. But this is nonsense, because x is bound in B and there is no x in the notation to perform the binding. So it is necessary for x, A, and B to all appear together in a single composite notation (x e. A |-> B).

On Sun, Mar 3, 2019 at 11:36 AM j4n bur53 <burs...@gmail.com> wrote:

Ok, gotcha, I have to click on the ∈. Thats a little strange,
but well then. Its also part of the definition of mapsto:

     http://metamath.tirix.org/df-mpt.html

As a syntax tree I would read maps to as (the LHS side
of the definition):

           ↦
       /       \
     ∈        B
    /   \
   x     A

But the structured view has its own ideas about that....

On Sunday, March 3, 2019 at 5:32:37 PM UTC+1, j4n bur53 wrote:

Was playing around with metamath and noticed again something
interesting. The structured view provides me with the ability to

click on symbols, and it leads me directly to their definition.
This seems not to work for the mapsto symbol. Why is this so?

For example here, I cannot click on mapsto:

   sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})
   http://metamath.tirix.org/df-sigagen.html

Means I cannot click on ↦ . The other symbols seem to work.
I wanted to explore what is behind the mapsto symbol.

Looks like a kind of dependent type thingy inside
metamath, which makes me courious.

[Mario Carneiro]

This is correct. This is how you would implement it in higher order logic, and in lean would be similar except the names of o and i are different. But really, the better answer is that you don't need |-> in HOL or DTT at all because it's built in to the system - it's called lambda. Metamath doesn't have a built in concept of binder but you can use binding variables and open terms to mimic it. I'm hoping to make this translation more explicit in Metamath Zero, which will have a translation to HOL and also to Metamath.

By the way, we could also have defined (x |-> B) in set.mm with only two arguments, but it's more useful to have an explicit domain, which corresponds to the construction \lambda x: A, B in HOL.

On Sun, Mar 3, 2019 at 12:08 PM j4n bur53 <burs...@gmail.com> wrote:

Corr.: Missing quantification:

    |-> a F = z  <=> forall x,y(<x,y> e z <=> x e a /\ F x = y)

On Sunday, March 3, 2019 at 6:05:59 PM UTC+1, j4n bur53 wrote:

Corr.: The poast was nonsense. Second try:

    |-> : i x (i -> i) -> i

And then:

    |-> a F = z  <=> forall x(<x,y> e z <=> x e a /\ F x = y)

Interestingly metamath can simply use B = y in its definition
inside df-mpt.html . Something I cannot get used to so easly.

On Sunday, March 3, 2019 at 5:50:29 PM UTC+1, j4n bur53 wrote:

I would nevertheless define an operator,
(sketich with set parameters only):

    |-> : i x (i -> o) -> i

Where:

   |-> a (lambda x.B) := { y e a | (lambda x.B)y }

Or for short:

   |-> a P:= { y e a | P y }

Which can be made into:

   |-> a P = z  <=> forall y(y e z <=> y e a /\ P y)

Just some ideas. This avoids overloading e.

On Sunday, March 3, 2019 at 5:43:33 PM UTC+1, j4n bur53 wrote:

Yes I understand. How would you define such a construct
in Lean Theorem Prover? The definition df-mpt.html has a

lot of side conditions, which I guess are necessary to reach
its goal. Can you do the same in Lean Theorem Prover?

[Mario Carneiro]

The requirement T e. W is set.mm's way of saying "T is a set". In HOL there is no need for such an assertion because the type i contains only sets to begin with. But you can imagine if there was another type big_i that was a supertype of i, in the sense that there is an injection "in : i -> big_i" and a reverse map "out : big_i -> i" such that in (out x) = x, then you would be able to say that an element of big_i "is a set" if it is in the range of "in", and in that case you can get the element of i that corresponds to it via "out".

So you should think of T as being a member of "big_i", where big_i = class, and T e. W is the same as saying E. x x = T which is the same as saying that T is in the range of "in" = cv.

By contrast, 'y' in "y e. T" is a member of "i", so it is always "small" in this sense, and it can be used directly in binders.

On Sun, Mar 3, 2019 at 1:38 PM j4n bur53 <burs...@gmail.com> wrote:

Some lambda x:A,B you can only instantiate x. You would need maybe
more like pi A:set pi B:set lambda x:A.B, so that A and B can be also
instantiated. But this might be implicity done by the system, i.e. you

might or might not need to write pi A:set pi B:set as well.
In as far, maybe metamath can be broken down to some smaller
units, type abstraction and value abstraction.

There is actually a separation of abstractions of this kind. There are two kinds of "forall" in metamath. One you are probably familiar with, "A. x ph". You can manipulate this like any other wff, and it always quantifies over elements of "i" = set. Because set theory puts such a rich structure in set, you can mimic all sorts of bounded quantification by restricting attention to the elements of particular sets; this gives you the restricted abstraction "A. x e. A ph" which we normally use as the "typed forall". But it's just a derived notation.

The second kind of forall is baked into the system, and is the quantification over metavariables when you state a theorem. Any theorem you prove with metavariables is effectively universally quantified over them - you have no control over this process, so you can't negate it to get existential theorems or anything like that. But you can substitute for these variables when you are using the theorem to prove another theorem. Note that the quantification goes before all hypotheses to a theorem, which is why you can't substitute into the metavariables of the $e assumptions to a theorem when you are in the proof. Otherwise $e |- ph $p |- ps would be provable, by substituting "ps" for "ph" in the assumption.

In the example "lambda x:A, B" you have both kinds of abstraction. The abstraction over x is of the first kind, an explicit abstraction that can be manipulated in the logic. The abstraction over A and B is of the second kind, an abstraction that lifts to the lop level of the theorem and can't be manipulated. If you define something about lambda x:A, B then it will be true for all values of A and B for the purpose of later theorems, but in the theorem statement and proof A and B are fixed and arbitrary.

 

But I don't know

whether this all works out correctly. Since after all a type which is a
set, is also a value. I am really currious how this all works out.

Here is an example where levels get blured, first we have:

     𝑦 ∈ 𝑇

So T is something like a type. And then:

     𝑇 ∈ 𝑊

So T is something like a value. I am refering to this:

    http://us.metamath.org/mpeuni/sxval.html

But somehow this is not an optimal example, since W is not used
in the theorem. But anyway, I guess it can nevertheless serve
to illustrate what I mean.

[Mario Carneiro]

That theorem is equivalent to the statement forall x, exists A, x e. A, and this statement is either provable or not stateable / not well typed in all of the proof systems under discussion. In metamath, you can't quantify over class variables, but you can prove A. x x e. _V. In HOL you can instantiate A with _V = \lam x, true, and similarly in lean, where A : α -> Prop and x : α, for some type α playing the role of i.

On Sun, Mar 3, 2019 at 5:34 PM j4n bur53 <burs...@gmail.com> wrote:

You wrote: "The abstraction over A and B is of the second kind, an

abstraction that lifts to the lop level of the theorem and can't be manipulated."

Now I have  a little theorem, which I discovered recently, which

would show that this limitation could lead to problems. How would
you with your modelling then proof this here, which is generally valid
in FOL=+ZFC if I am not totally wrong.

     forall A forall x (x e A => P(x)) <=> forall x P(x)

The forall A quantifier is not outside of <=>, its inside the LHS
of <=>. How would you do it in Lean Theorem Prover via a type
variable for A?

[Mario Carneiro]

Can you move this into another thread? This isn't really on topic here.

On Sun, Mar 3, 2019 at 6:31 PM j4n bur53 <burs...@gmail.com> wrote:

Corr.:
Will type variables be sets sometimes? Can we use
them for sets in Lean Theorem Prover.

On Monday, March 4, 2019 at 12:30:33 AM UTC+1, j4n bur53 wrote:

There is a section

0. 10.4 Zermelo-Fraenkel set theory

In Paulsons paper, side remark I don't know whether it has virtual
classes. This doesn't imply that the |-> example and the A type
variable was about virtual classes.

First things first. Will type variables be sets? Later could
discuss virtual classes.

On Monday, March 4, 2019 at 12:26:46 AM UTC+1, j4n bur53 wrote:

No no, A is not a class variable. When I started asking about
a Lean Theorem Prover solution I had this product type in mind:

       pi A:set pi B:set lambda x:A.B

       https://groups.google.com/d/msg/metamath/Df4--aqbjwg/RBSi9hjvAgAJ

So A would be of the some kind "set". Not a class. I did not
specify how this kind "set" is realized, but the idea was only
to look at the set parameter case. I also wrote this when I said

"I would nevertheless define an operator, (sketich with set parameters

only)" You see with set parametrs only. No class thingy. The meta math
|-> is a class thingy. But I wanted to know how to do it set wise

in Lean Theorem Prover. And what I have heard with Lambda x:A.B
left some doubts for me. Because in Isabelle you can access
A,B. There is the level of using a logic, which is mostly done

in the Isar Proof language (Lean looks like a rip off of it, or vice
versa). But the you can also access Isabelle a little bit lowerlevel
and use the other Proof language, where you can mix constructs

from the logic framework with the present logic. It has already
tactics like auto (Lean ripped it off as tidy?) The lower level goes
by the name bla bla, and has its own implication and forall.

Paulson calls it meta-logic if I remember well. Also when you do
proofs in the higher level you might see artefacts from the lower level,
stuff is sometimes displayed when you work on proofs, the hints and

everything you get etc.. is still pickeld with this meta-logic. This
meta-logic allows you to make different "logics" inside Isabelle.
See also:

Isabelle: The Next 700 Theorem Provers - Lawrence Paulson
https://www.researchgate.net/publication/1960971_Isabelle_The_Next_700_Theorem_Provers

I have the feeling to do something in Lean Theorem Prover towards
metamath, you need also to have access to the meta-level of the Lean
Theorem Prover, if there is such a level. Or then follow some

other approaches. Not sure.

[Jim Kingdon]

𝐴 ∈ V suffices.

http://us.metamath.org/mpeuni/mptexg.html

And yes this is proved using replacement, as seen by ax-rep in the "This theorem was proved from axioms" section of that web page.

On March 4, 2019 3:09:13 AM PST, j4n bur53 <burs...@gmail.com> wrote:

Disclaimer: For metamath I have only conjectured A e V /\ B e V
then (x e A |-> B) e V. Didn't dig up whether there is already

some such proves, or whether there are some nudges that
would prevent such a lemma or theorem....

On Monday, March 4, 2019 at 12:07:00 PM UTC+1, j4n bur53 wrote:

In my naivity I would do something pi A:set pi B:set |->
(lamdda x:A.B) : set. So simply say that mapsto gives a set again.

In as far I wonder why in metamath the replacement axiom of set
theory, is no where mentioned in connection with

     http://metamath.tirix.org/df-mpt.html

If I look here:

     http://us.metamath.org/mpegif/ax-rep.html

I don't find any references to df-mpt. But they are somehow related,
like for example could prove A e V /\ B e V then (x e A |-> B) e V.

P.S.: This is also nice, Peter Aczels sup: 4.1 The Sets

Sets in Types, Types in Sets (1997) Cached

by Benjamin Werner

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Thierry Arnoux]

Hi Jan,

Thanks for your remarks!

I've fixed at least the links to Lim, Ord, and "maps to" (link to GitHub commit), and a few others in other commits (I've also caught up with newly added symbols).

I've launched the regeneration of the pages just now; this usually takes a few days to complete.

_
Thierry

On 08/03/2019 13:29, j4n bur53 wrote:

Now I stepped into a new problem, that clicking on symbols doesn't
work. A recent problem was "mapsto". But now "Lim" doesn't work either.
I wanted to click on "Lim" here:

𝜔 = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)
http://metamath.tirix.org/df-om.html

But no reaction of the system. I was expecting that it sends me to here:

(Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
http://metamath.tirix.org/df-lim.html

Also "Ord" doesn't work. On the other hand "On" and "U" do work.
Also the links back to the non-structured unicode view don't work.
When clicking on the right top "Unicode version" in the structure

view I get the following error:

Not Found

The requested URL /mpeuni/df-lim.html was not found on this server.

http://metamath.tirix.org/mpeuni/df-lim.html

[Mario Carneiro]

The syntax breakdown of axioms is only there to fill space on the page. Metamath doesn't do parsing in normal operation, so the syntax of the hypothesis there could be not well formed and metamath wouldn't complain. This data is not stored anywhere because it isn't present AFAIK. However, many tools like mmj2 (and MM-PA to some extent) require that all hypotheses and conclusions of theorems are valid wffs, and will parse the formula to make sure. So these tools will have an internal representation of the hypothesis as a structured term, although most of them don't provide a means for you to view it directly.

Mario

On Sun, Mar 10, 2019 at 9:10 PM j4n bur53 <burs...@gmail.com> wrote:

Thank you!

I have a small question. Is the syntax of a hypothesis in
definition not broken down? Bug or feature?

I was just looking at:

     http://us.metamath.org/mpegif/df-cleq.html

And I have the feeling there is no breakdown
of df-cleq.1. Is there a trick to see it somewhere?

Bye

[Norman Megill]

In addition to what Mario said, there are only 3 axioms and definitions that have hypotheses (ax-mp, ax-gen, and df-cleq):

MM> search df-*,ax-* '|- $* |-' /join
47 ax-mp $e |- ph $e |- ( ph -> ps ) $a |- ps
4125 ax-gen $e |- ph $a |- A. x ph
7198 df-cleq $e |- ( A. x ( x e. y <-> x e. z ) -> y = z ) $a |- ( A = B <-> A.
    x ( x e. A <-> x e. B ) )

and I didn't think it was worth writing extra code just for these special cases.  On the MPE Home Page it says, "In the case of axioms and definitions, we do show their detailed syntax breakdown, because there is free space on those web pages not used for anything else. These can help you become familiar with the syntax...." So the breakdown is meant to provide a helpful hint but isn't necessarily comprehensive.  We also don't provide syntax breakdowns for $p statements, for example.  Because the grammar is unambiguous, the hypothesis part should be easy to parse by hand, especially since in df-cleq the hypothesis has only existing symbols with nothing new introduced.  I don't feel it is important enough to consider it a bug.

On Sunday, March 10, 2019 at 9:10:27 PM UTC-4, j4n bur53 wrote:

Thank you!

I have a small question. Is the syntax of a hypothesis in
definition not broken down? Bug or feature?

I was just looking at:

     http://us.metamath.org/mpegif/df-cleq.html

And I have the feeling there is no breakdown
of df-cleq.1. Is there a trick to see it somewhere?

Bye

On Saturday, March 9, 2019 at 8:56:43 AM UTC+1, Thierry Arnoux wrote:

[Marnix Klooster]

Hi all,

Last week, I've made a number of updates (dare I say improvements?) to my 'userscript' mm-calc2 (link to latest version, currently at version 7).

It still does essentially the same thing, namely display a calculation above any 'proof table' on metamath.org (and metamath.tirix.org), on every Unicode page (so not the GIF pages).  It does not only work with GreaseMonkey which is Firefox-specific, but I've verified that it also works in Chrome with either Tampermonkey or Violentmonkey, and probably it works in any modern userscript-supporting browser.

The new version makes some changes that are probably not for everyone, but for me personally, it helps me tremendously to read metamath.org proofs.  It might help others as well.

Changes since version 3 of June 2018, most visible ones first:

• The calculations are now 'up-side-down', starting with the goal.
• Initially only the top-level calculation is shown, the rest can be expanded.  (Yes!)
  
• I now use two very crude heuristics to find which hypothesis to use as the next step in each calculation (see function guessMainSubproof()):
• Take the hypothesis which is closest in length to the conclusion;
• But avoiding if possible a 'reused' step.
• Reorder the references in each 'hint', to make the 'key' step usually appear first and the 'auxiliary' steps last.
• Bugfix: Now points correctly to 'reused' steps (although they can be hard find as they're usually initially inside hidden subproofs).

Again, this script is by no means perfect, but for most proofs it really helps me understand the structure of the proof better, and it surprised me how effective the above simple heuristics are.

Feedback welcome, but again, I have no idea when I'll again be able to spend significant time on this.

Groetjes,

 <><

Marnix

Op za 9 jun. 2018 om 09:35 schreef Marnix Klooster <marnix....@gmail.com>:

Hi all,

Yesterday I got tired of manipulating the existing HTML proof tables in my Greasemonkey script, so I hacked up 'mm-calc2' which more directly renders to the proof format I have in mind, leaving the original proof table untouched.  Get it at https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc2.user.js.  Above each proof table, it renders a calculational equivalent of the table.  It currently also works on metamath.tirix.org.

Try it, for example, on http://us.metamath.org/mpeuni/eulerth.html and http://metamath.tirix.org/eulerth.html.  Or on http://us.metamath.org/mpeuni/ru.html and http://metamath.tirix.org/ru.html.

This initial version of mm-calc2 does not yet do collapse/expand, and it just shows both formats at the same time.  So it will look not look too good on large proofs-- but I'd argue the table format is not easier to understand for large proofs anyway. :-)

Also, it has a bug in that it doesn't show reused steps correctly.  (For example, in http://us.metamath.org/mpeuni/pm5.54.html, the second reference to step 2 / bicomd is missing.)

But despite these restrictions, it already helps me read some proofs more easily, especially with the formatting on metamath.tirix.org.

And for the future this gives me a kind of 'test bed' to try different orderings of the same calculation, e.g. using a chain of <== instead of ==>, choosing not the first antecedent but a different one, or even using set.mm operators like <-> and = in the left hand column, instead of just the 'meta-implications' ==> and <==, and removing repetition by extracting common contexts like this:

In context ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ...) we have

	(1...(ϕ‘𝑁)) ≈ {𝑘 ∈ (0..^𝑁) ∣ (𝑘 gcd 𝑁) = 1}
⇒	“using sylib 189 and bren 7108”
	∃𝑓 𝑓:(1...(ϕ‘𝑁))–1-1-onto→{𝑘 ∈ (0..^𝑁) ∣ (𝑘 gcd 𝑁) = 1}

Again, no idea when I'll continue work on this, feedback welcome.

Groetjes,

 <><

Marnix

2018-06-06 18:07 GMT+02:00 Marnix Klooster <marnix....@gmail.com>:

(Forgot to include the group...)

Hi Thierry,

Thanks for including, and so quickly! :-)

What that indentation algorithm does, is take a tree like

  2: F

      4: E

    3: D

    3: C

  2: B

1: A

and make it look like a calculation, by indenting the first parent/antecedent of a step the same as the step, the second one level deeper, etc.:

2: F

  4: E

  3: D

    3: C

  2: B

1: A

This is intended to match the following calculational proof:

    F

==>  "by sub-proof"

         E

     ==>

         D

     ==>  "by C"

         B

    A

I'm trying to update my Greasemonkey userscript to collapse/expand on the granularity of such calculations and sub-calculations, and to render proofs more and more in this form.

Even with the current limited indentation form, with basically your (Thierry's) expand/collapse, a number of proofs start to be actually a bit readable to me. :-)

And yes, a large proof will still indent quite a lot, and my indentation size might a bit too large-- but still for me it is an improvement on the standard metamath /html format.  I think that my algorithm actually indents less than the original format...

Groetjes,

 <><

Marnix

2018-06-06 16:34 GMT+02:00 Thierry Arnoux <thierry...@gmx.net>:

Hi all,

Because not everybody has Firefox and Greasemonkey, I've included Marnixes scripts on my pages.
You can switch to this indentation by clicking the "M" on the top right of the proof tables (you have to reload page to switch back to the original display).

Marnix, you did not provide much explanation, could you tell how it's working?

BR,
_
Thierry

On 06/06/2018 04:10, Marnix Klooster wrote:

Hi all,

For quite a while I've been looking into different ways to render Metamath proofs-- and Thierry's rendering experiments (which look great!) inspired me to do some experiments in JavaScript.

To allow me easy experimentation, I've chosen to use Greasemonkey on Firefox.

To use this, you need to install the Greasemonkey add-on (https://addons.mozilla.org/en-GB/firefox/addon/greasemonkey/), and then open or install my script from https://gist.github.com/marnix/7c2ab51156b34b8a54c61861bec452a3/raw/mm-calc.user.js .  (I think your Firefox Greasemonkey should auto-update when I change this script the correct way, but I'm not sure yet.)

(Caveat emptor: For any Greasemonkey script you run, make sure you get it from a trusted source, and analyze the source code if you're not sure.  The above script runs with no special permissions.)

The goal of this script is to make a proof look more like a 'calculation', which (for me at least) usually makes them easier to follow.  For example, try it on http://us.metamath.org/mpeuni/ru.html or http://metamath.tirix.org/ru.html (with all steps expanded).

The current version of this script only re-indents the formulas in a way that makes more sense to me than the usual tree structure.  (Tested on metamath.org Gif+Unicode and metamath.tirix.org.)

I have ideas for other changes/improvements, but I have no idea whether I will have the time...

Anyway, feedback welcome, and enjoy!

Groetjes,

 <><

Marnix

--

Marnix Klooster
marnix....@gmail.com

--

Marnix Klooster
marnix....@gmail.com

--

Marnix Klooster
marnix....@gmail.com

--

Marnix Klooster
marnix....@gmail.com

--

Marnix Klooster
marnix....@gmail.com

[Marnix Klooster]

Hello all,

Here is my irregular update on my Metamath userscripts, which keeps getting more useful (for me, so perhaps for you as well!).

(Please see earlier emails for how to use it, it probably works with any modern browser with any userscript manager extension.)

I released version 8 earlier today (link to latest version).  This time let me first show you what this browser extension actually does: In the metamath.org 'Unicode' proof pages (and the ones on metamath.tirix.org), it shows the proof also as in the following screenshot of php, where buttons expand subproofs.  Compare this to the original at http://us.metamath.org/mpeuni/php.html.

The only change in this version 8, which I feel is a real improvement, is the way the 'spine' of the calculation is chosen.  Or in other words, the way to determine the 'main' or 'key' $e hypothesis of a proof step's $a or $p statement.  And the nice thing is that there seems to be a simple measure for this. Roughly,

the main $e hypothesis is the one that has the smallest relative difference w.r.t. the $a/$p expression.

For example, for the php screenshot, in the step where syl5ibrcom is used: in this instantiation of that statement.

• the difference between syl5ibr.1 and syl5ibrcom is  '... 𝐵 ... ¬ suc 𝑥 ...'  vs '... 𝐴 ... (𝐵 ⊊ 𝐴 → ...)';
• the difference between syl5ibr.2 and syl5ibrcom is '... ... (... ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵)...' vs '... 𝑥 ∈ ω → (... ... ...'.

Both sides of the first diff are similar in length, while for the second diff, the second/conclusion side is much shorter.  Therefore we decide that syl5ibr.2 is an 'information-injecting' hypothesis, and syl5ibr.1 is the 'main' / 'spine' hypothesis.  Which leads to the rendering from the screenshot.

The implementation is only a rough approximation: It uses the length in characters of the HTML (so not the number of tokens, and certainly it doesn't try to do any parsing); it uses the instantiated rule (and not the underlying $a/$p statement with its hypotheses); it uses 'longest common subsequence' to compute the diff (which means that X = Y in a hypothesis and Y = X in the conclusion will seem very different); and it only uses a 'greedy' approximation of LCS that is much more efficient to compute.

But with all that said, even this simple implementation makes it a lot easier (for me) to read the metamath.org proofs.  And for those interested, you can see more examples in the attached zip-file.

Thanks for your attention!  (And if someone actually read this far and is using or planning to use this userscript, feel free to let me know!)

Groetjes,

 <><

Marnix

Op di 5 mei 2020 om 14:24 schreef Marnix Klooster <marnix....@gmail.com>:

--

Marnix Klooster
marnix....@gmail.com