Nice ! Just to clarify:
The first script finds ${--$} pairs which enclose at most one (or exactly
one?) $-statement, and that $-statement is a $p-statement (what if the
single $-statement is an $a-statement ? the awk program does not seem to
take them into accound).
As for the second: it removes $d conditions among non-occurring variables
(whether in the statement or in the proof, i.e., dummy variables). But
there could still remain extraneous dv conditions. Correct ? Would it be
doable to find these as well ?
Thanks,
Benoît
On Friday, October 29, 2021 at 8:11:28 AM UTC+2 Thierry Arnoux wrote:
> Hi Jerry,
>
> Very nice!
>
> I think we shall remove those unnecessary braces, and the "braces" script
> could be added to our continuous integration, checking at every commit that
> no new useless braces are added.
> At least we shall add the "braces" script to metamath's script directory.
>
> Concerning the distinct variable statements however, I think you have some
> false positives. It for example detects `.x.` at line 728127, that is for
> theorem ~lincresunit2 in AV's mathbox. When I remove this DV, MMJ2
> complains it's missing. `.x.` actually appears in the essential hypothesis
> ~lincresunit.t. There are other examples, it seems to be when the essential
> hypothesis actually appears before the DV declaration.
> Otherwise you seem to have done a good job avoiding the pitfall of
> variables which are introduced in the proof, but don't appear either in the
> theorem statement, nor in the essential hypothesis. Those have to be
> declared as distinct variables anyway. There was a discussion thread about
> removing those, but I think we decided to keep them for the moment.
>
> BR,
> _
> Thierry
>
>
> On 29/10/2021 11:17, Jerry James wrote:
>
> I have been studying parts of set.mm that I want to understand better.
> While doing so, I have occasionally encountered unnecessary ${ $} pairs,
> and occasionally have seen $d statements for variables that do not appear
> in the theorems or proofs in that scope. Tonight I wrote a pair of scripts
> to detect these situations. It is a testament to the simplicity of the
> metamath grammar that I could write both in a single evening.
>
> Here is a 5-line awk script that identifies unnecessary braces:
> http://jamezone.org/pleasure/mathematics/metamath-braces
>
> This is the number of unnecessary brace pairs per mm file (skipping those
> with zero):
> - iset.mm: 51
> - nf.mm: 56
> - set.mm: 207
>
> For the second issue, I started writing awk code as well, but quickly came
> to the realization that the line-oriented nature of awk was not well suited
> to the task. Here is a python script that finds $d statements for
> variables that do not appear below the $d in the same scope:
> http://jamezone.org/pleasure/mathematics/metamath-dvs.py
>
> This is the number of variables it found per file (skipping those with
> zero):
> - hol.mm: 1
> - iset.mm: 1302
> - nf.mm: 390
> - set.mm: 6124
>
> Unnecessary braces and $d statements are not critical issues, of course.
> I offer these scripts to anyone who wants to declutter a metamath database.
>
> Regards,
> --
> Jerry James
> http://jamezone.org/
>
> --
> 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/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%40googlegroups.com
>
> <https://groups.google.com/d/msgid/metamath/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
>
--
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/11fa7624-7b17-48ab-aedd-9cd52ad848aen%40googlegroups.com.
