[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

Hi Rob,

> I am looking forward to seeing how this works out when I finish
> upgrading my reader/writer for ProofPower to version 6.  Will
> it be possible to do the conversion with the opentheory tool
> as a filter (so a script to import an article can just convert it
> to its preferred version on the fly)?

Indeed, this is already supported. This command reads an article (of
any version) from stdin and writes an equivalent article on stdout
using version 6:

opentheory info --article --output-version 6 article:-

> If you are going to say that the extra argument to the thm command
> must be processed in the same way, then you are going to have
> to extend the OpenTheory virtual machine to include the theorem
> metadata, so that you can define that processing. Were you planning
> to do that?

No, I wasn't: my intention was that the theorem meta-data would be
interpreted in a reader-dependent way. The proposal was merely a
standard format for representing meta-data as finite maps represented
by nested lists of names, not processing it.

> If you weren't planning to change the virtual machine, then
> this seems to me like a good candidate for a standardised
> pragma as Mario suggests.

It would certainly be possible to specify theorem meta-data using
pragmas, and perhaps this is after all the best way to do it.

However, in the spirit of yesterday's unsolicited philosophy lecture,
I would like to take a stand against "standardized pragmas". Once a
particular pragma has demonstrated its usefulness, my favoured
approach would be to define a new command in the next version of the
article spec standardizing its behaviour, rather than adding it to a
set of standardized pragmas. This is what I meant when I said I saw
pragmas as an experimental laboratory for new commands.

Given this approach, there is no standardized behaviour for pragmas,
and so the opentheory tool does not have the information to maintain
them in articles it processes. Consider maintaining a "debug" pragma
during processing that compresses an article by merging equivalent
objects, or maintaining a "thmName" pragma during processing that
reorders the exported theorems.

My theorem meta-data proposal was an attempt to standardize the
behaviour of thmName as a new command (i.e., the existing thm command
with an extra argument) so that the opentheory tool could maintain the
information during processing, but this discussion is persuading me
that the benefit of the change may not be worth its cost.

Cheers,

Joe