[opentheory-users] the Unwanted namespace

[Joe Hurd]

Hi Ramana,

I've taken a look at your file and your error messages, and I think
perhaps it will help if I explain the current proof rewriting strategy
for eliminating Unwanted.id.

It's only two OpenTheory commands, appTerm and appThm, that change
their behavior thusly

appTerm (Unwanted.id) (tm) --> (tm)

appThm (|- Unwanted.id = Unwanted.id) (|- x = y) --> (|- x = y)

In the first error you encountered the proof involved deducing something like

|- Unwanted.id = Natural.+ 0

and then using appThm with this as the first argument, but that
doesn't fit into the pattern above for eliminating Unwanted.id.

[I'm not entirely sure what's going on in your second example, but the
theorem (|- Unwanted.id = \x. F) on the stack is perhaps cause for
concern.]

This proof post-processing is extremely simple and ad-hoc right now,
and as you can see it can only handle one very special kind of
pattern. I'd be interested in discussing ways to expand its scope, or
alternatively perhaps there are ways to recast your proofs into the
existing pattern.

Cheers,

Joe

On Sat, Oct 8, 2011 at 12:02 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> I've uploaded a much smaller (~2000 lines) gzipped article to
> cam.xrchz.net/Unwanted.art.gz which fails with a similar error:
>
> FATAL ERROR: opentheory failed:
> in Article.fromTextFile:
> error in file "Unwanted.art" around line 1769:
> eqMp
> 313
> def
> while executing eqMp command:
>  stack =
>    [|- Unwanted.id x <=> let x <- x in F,
>     |- (x <=> let x <- x in F) <=> x <=> F,
>     |- (x <=> F) <=> (x <=> F) <=> T, x,
>     |- (!x. x <=> F) ==> let x <- x in x <=> F,
>     |- (let x <- x in x <=> F) <=> x <=> F, [[], [[x, T]]], |- (~) = (~),
>     |- (~T <=> ~F) <=> ~T <=> T, |- (<=>) (T <=> F) = (<=>) (T <=> F),
>     |- (<=>) = (<=>), |- Unwanted.id = \x. F]
> in ObjectProv.mkEqMp:
> in Thm.eqMp:
> terms not alpha-equivalent:
>     Unwanted.id x <=> let x <- x in F
>  vs x <=> let x <- x in F
> different term structure at path 01 subterms: Unwanted.id x vs x
>
> However, in this case I would want processing to fail somewhere
> (perhaps not like this), because I think otherwise the article's
> exports would include |- T = F (and it would have consistent imports).
> Perhaps the same safeguard (if that is indeed what I'm running into
> here) is preventing my original article from being read, and so I'm
> not using Unwanted.id correctly there somehow..?
>
> On Fri, Oct 7, 2011 at 10:05 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> it occurs to me that it might be a types problem - would the
>> opentheory tool require the Unwanted.id constant to be created with a
>> particular type?
>>
>> On Fri, Oct 7, 2011 at 10:03 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>>> 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.)
>>>>
>>>> Is there any way of reducing your problem to a simple case that I could look at?
>>>>
>>>
>>> Maybe - any suggestions? In the meantime the complete (gzipped)
>>> article is available here http://cam.xrchz.net/llist.art.gz. Maybe
>>> running opentheory with some extra debugging code to see whatever it
>>> does to Unwanted.id tags during reading this article will be
>>> helpful...
>>>
>>> FYI the error I get is
>>>
>>> ...
>>> in ObjectProv.mkEqMp:
>>> in Thm.eqMp:
>>> terms not alpha-equivalent:
>>>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>>>       (Number.Numeral.bit1 Number.Numeral.zero) =
>>>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>>>       (Number.Numeral.bit1 Number.Numeral.zero)
>>>  vs Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>>>       (Number.Numeral.bit1 Number.Numeral.zero) =
>>>     Unwanted.id
>>>       (Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>>>          (Number.Numeral.bit1 Number.Numeral.zero))
>>> different term structure at path 10 subterms:
>>>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>>>  vs Unwanted.id
>>>
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>