[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

> So let's have the discussion about ways to expand its
> scope.

Sure!

> I eventually came to the conclusion that appTerm and appThm are the
> only commands that would ever need to change, because they are the
> only way a term of the form (Unwanted.id t) can enter the virtual
> machine's state.

Unfortunately I can see other ways that terms like these could enter
the state, such as

appThm (|- (\f. f x) = t) (|- Unwanted.id = u)

followed by betaConv of the LHS at a later point.

> Perhaps opentheory should automatically just do an explicit proof
> after absThm (|- Unwanted.id = f) (|- x = y) of (|- x = f y), for all
> x y and f, using an assumption (|- Unwanted.id x = x). Also, you would
> need to prevent the name Unwanted.id from being used by defineConst.

I'd really like a scheme that eliminates all occurrences of the
Unwanted.id constant from a proof, if that was possible. And by this I
mean that grepping the resulting article for occurrences of the
"Unwanted" namespace will not turn up any results.

I believe the highly specialized scheme that the opentheory tool
currently implements has this property, but I don't know if it's
possible in general. If there is a proof rewriting strategy that
achieves this, I speculate that it will not require an explicit
definition of Unwanted.id in the form of a theorem.

Cheers,

Joe