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/c772b424-c3cd-4016-4907-b0983290b80f%40gmx.net.
