For the first point, the ${ $} pair can enclose more than one $-statement.
Specifically, once a ${ is seen, the script starts watching for any of $c,
$d, $e, $f, or $v. (That's the last line of the awk script.) If it sees
the matching $} without finding any, then it reports that pair of braces.
I made it ignore braces that do not include any $p statements (the next to
last line) because there are some used solely to contain comments.
For the second point, yes there might still be extraneous dv conditions.
Finding those would take significantly more work. Also note that Thierry
Arnoux found a bug in that script. I will try to fix it this weekend.
On Friday, October 29, 2021 at 4:49:03 AM UTC-6 Benoit wrote:
> 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/301d6504-5e88-42f5-9dba-ea93ad278634n%40googlegroups.com.
