[opentheory-users] the Unwanted namespace

[Joe Hurd]

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