[opentheory-users] definition of "new" constants? / processing of packages

[Joe Leslie-Hurd]

Hi Gunter,

> I gave it a try, and I found that it is forbidden to use
> two constants with different definitions and the same name
> in exported theorems (using thm) and perhaps also assumptions (using axiom):
> This makes perfect sense for a sound proof checker,
> but it should be part of the specification.

I agree, although I'm not sure whether it's part of the article spec
or the theory spec. If you're reading an article inside a theorem
prover it might be ok to have two different constants with the same
name (depending on the design of the logical kernel), so I hesitate to
forbid it for articles.

However, in the context of a theory constants are imported by name, so
there cannot be two constants in scope with the same name. So perhaps
the theory spec is the place to forbid this:

http://www.gilith.com/research/opentheory/theory.html

> ====================
>>opentheory info two-const-conflict.art
>
> FATAL ERROR: opentheory failed:
> different constants named "C"
> ====================

The opentheory tool reads articles inside an implicit "article block"
(see the theory spec), which is why your test article explodes.

> When opentheory processes a theory, does it read all theory article files
> on which it depends?
> Or is there a way that it just needs to read the theorems from
> other packages that it uses?

It just reads the statement of the theorems generated when the package
is installed. See this FAQ:

http://www.gilith.com/research/opentheory/faq.html#what-are-theorem-files

> What is the checksum entry?

The checksum is the package checksum. The opentheory tool allows you
to specify a package checksum when you install packages, to ensure you
are getting the exact package you want.

> I can somehow guess what the entry
>   show: "Data.Bool"
> in the .thm file means, but it is not completely clear.
> In particular, what happens when there are several "show: " lines?

These are namespace abbreviations, as mentioned in the example package file:

http://www.gilith.com/research/opentheory/example-1.0.html

When printing names the first show: line that matches a prefix of the
namespace gets applied, and the name is either rewritten (if the line
is show: "X" as "Y") or abbreviated (if the line is show: "X").

> Is there a way to eventually look at the theorems that are proved
> in detail in an unambiguous format with all type information? (other than the html
> format with mouse-over?)

In machine-readable format you can look at the generated theorem files
described above. In human-readable format you can see types using:

$ opentheory --show-types info --theory natural-def

and you can additionally bypass any show: declarations by converting
to an article first:

$ opentheory info --article natural-def | opentheory --show-types info article:-

Cheers,

Joe