[opentheory-users] redundant import check

[Ramana Kumar]

Hi Joe,

Thanks for the clarification. I think you interpreted my question correctly.
After reading your description, I think the checks for redundant imports in
a theory block are correct as is.

In general, though, I note that it is effectively impossible to define a
constant in OpenTheory without also proving a theorem about it.
To get around this, I prove a trivial theorem (|- c = c) about a new
constant c to ensure its definition is picked up.

My original question was motivated by a problem that I still have. Namely,
I receive unexpected warnings about 2 different constants with the same
name. I thought this was because I hadn't imported the block that defines
the constant into all the blocks that use it, but (hopefully I checked this
right) if I add any of those import lines they are flagged as redundant.
The warning about different constants therefore looks like a red herring;
the resulting theory package doesn't appear to have any problems like
unexpected axioms or assumptions or ungrounded constants.

Perhaps you could explain further the circumstances under which the 2
different constants warning occurs. I can also provide the relevant
articles and theory packages but they are quite large and unwieldy so I'd
rather hold off on that at first.

Cheers,
Ramana

On 31 March 2016 at 18:18, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> There are a couple of different redundant warnings the tool can
> generate: I assume your question is about the "redundant import X in
> theory block Y" warning message, not the "redundant requires: X"
> warning.
>
> I've just looked at the code, and for an import X to be reported as
> redundant in theory block Y both of the following must hold:
>
> 1. The theorems of X and the assumptions of Y are disjoint.
> 2. The defined symbols in the theorems of X and the input symbols in
> theorems of Y are disjoint.
>
> If I interpret your question correctly, you are concerned about
> removing a redundant import X containing a defined symbol S that is
> used in Y but not exported in a theorem. After scratching my head for
> some time I cannot see how removing X from the imports of Y could
> result in the creation of different symbols with the same name, but
> perhaps I am missing something.
>
> Do you have a problem scenario in mind?
>
> Cheers,
>
> Joe
>
>
> On Tue, Mar 29, 2016 at 3:03 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Hi Joe,
> >
> > I have not had time to investigate this thoroughly yet, but I have a
> > suspicion that the redundant import check might not check for constants
> that
> > don't appear in any theorems. Therefore, removing a "redundant" import
> might
> > result in two different constants with the same name. Do you think this
> is
> > possible?
> >
> > Cheers,
> > Ramana
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160401/be260482/attachment.html>