[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

> Is the Unwanted namespace documented?

There is currently not any documentation for the Unwanted namespace.

> What is the intended usage?

As a place to map evil theorem-specific "tags" that could be
post-processed away by the opentheory tool, rather than burdening the
proof exporter with the task.

> I am attempting to use Unwanted.id for various HOL4 constants that are
> semantically identity functions, although sometimes at specific types
> (these constants include arithmetic$NUMERAL and marker$Abbrev). I was
> hoping, naively, to just record proofs that might contain these
> constants as they are, translating each one to Unwanted.id, and have
> the opentheory tool remove them automatically. Is this a realistic
> hope?

Yes, that is exactly how I use it with the HOL Light NUMERAL tag.

> Currently the tool is failing to process an article because at
> some point an extra Unwanted.id means two terms that should be
> alpha-convertible aren't. (But I don't think it's the first occurrence
> of Unwanted.id in the article.)

The main problem I found was that I'd get extra theory assumptions of the form

|- !n. n = n

because I hadn't accounted for the definition of NUMERAL:

|- !n. NUMERAL n = n

Is there any way of reducing your problem to a simple case that I could look at?

> Maybe I'm supposed to do some kind of
> extra work preprocessing theorems before recording their proofs...?

No, the intent is that the opentheory tool does all the work as a
post-processing step.

> Would it make sense for other names to live in the Unwanted namespace,
> with semantics different from the identity function?

Perhaps. I believe "K" term tags are also used in HOL4, where

!x y. K x y = x

which might result in a similar use for Unwanted.k in the future.

Cheers,

Joe