[opentheory-users] the Unwanted namespace

[Ramana Kumar]

On Tue, Dec 6, 2011 at 7:36 PM, Joe Hurd <joe at gilith.com> wrote:
> The solution is to ensure that every instance of Unwanted.id in theory
> assumptions and theorems is fully applied. This should always be the
> case for constants used to tag terms, which are the main use-case of
> Unwanted.id.

I'm not so sure about that. This theorem is from the HOL4 library
(combinTheory.literal_case_FORALL_ELIM):

|- literal_case f v ⇔ (!) (S ((==>) o Abbrev o C (=) v) f)

The "Abbrev" constant in the middle there is a tag for abbreviations
(which I map to Unwanted.id).
(This is where, I believe, my axiom in the lazy list theory was coming from.)

I'm not sure why this theorem has the form it does, but it could be an
example of a useful not-fully-applied tag.
Perhaps someone who knows more about that theorem could clarify...

>
> Cheers,
>
> Joe
>
> On Tue, Dec 6, 2011 at 11:18 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Will your scheme for eliminating Unwanted.id work in terms where it
>> does not appear fully applied, but can still be eliminated?
>> Specifically, when Unwanted.id is composed with another function.
>>
>> On Tue, Dec 6, 2011 at 6:44 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> Thanks for making it quicker :)
>>>
>>> Now, the only place where Unwanted.id seems not to be erased is in an
>>> apparent axiom required by my article.
>>> Can you confirm that the article is actually trying to define Unwanted.id?
>>> I generated the article from a HOL4 theory that I don't think should
>>> be defining anything mapped to Unwanted.id, so I'm a bit confused
>>> about that at the moment...
>>>
>>> On Tue, Dec 6, 2011 at 4:58 AM, Joe Hurd <joe at gilith.com> wrote:
>>>> Hi Ramana,
>>>>
>>>> I fixed a performance bug in the proof rewriting, and your example
>>>> goes through pretty quickly now (see below). The fix is both pushed
>>>> and released in the latest version of the opentheory tool.
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> ________________________________________________________________
>>>>
>>>> dimholt:~/dev/opentheory$ gzcat ~/Desktop/ll.art.gz | time
>>>> bin/mlton/opentheory info --inference article:-
>>>> WARNING: 38 objects left on the stack by -
>>>> WARNING: 473,658 objects left in the dictionary by -
>>>> Primitive inferences:
>>>> eqMp ............ 150,377
>>>> deductAntisym ... 129,584
>>>> subst ............ 76,065
>>>> appThm ........... 20,748
>>>> assume ........... 18,086
>>>> refl .............. 9,363
>>>> betaConv .......... 7,461
>>>> absThm ............ 4,564
>>>> axiom ............... 193
>>>> defineConst .......... 25
>>>> defineTypeOp .......... 1
>>>> Total ........... 416,467
>>>>       24.40 real
>>>>       15.30 user
>>>>         9.07 sys
>>>>
>>>> dimholt:~/dev/opentheory$ time bin/mlton/opentheory info --inference
>>>> foo.art Primitive inferences:
>>>> eqMp ............. 68,100
>>>> subst ............ 56,228
>>>> deductAntisym .... 51,689
>>>> appThm ........... 17,378
>>>> betaConv .......... 6,866
>>>> refl .............. 6,325
>>>> absThm ............ 4,267
>>>> assume ............ 1,608
>>>> axiom ............... 190
>>>> defineConst .......... 26
>>>> defineTypeOp .......... 1
>>>> Total ........... 212,678
>>>>
>>>> real    0m5.289s
>>>> user    0m5.027s
>>>> sys     0m0.256s
>>>>
>>>> _______________________________________________
>>>> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list