[opentheory-users] the Unwanted namespace

[Michael Norrish]

I think the mistake here is mapping the Abbrev constant to Unwanted.  I'd say it was probably worth preserving.

Michael

On 07/12/11 09:35, Joe Hurd wrote:
> Hi Ramana,
> 
> Good job digging up a counter-example to my claim about how tags are
> used, but I think it's probably not worth the effort to handle exotic
> cases. Perhaps the theorem you found could be deduced from a form with
> a fully applied tag?
> 
> Cheers,
> 
> Joe
> 
> On Tue, Dec 6, 2011 at 11:53 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> 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
>>
>> _______________________________________________
>> 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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 554 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20111207/3c00fc13/attachment.pgp>