On Dec 6, 2011 11:02 PM, "Michael Norrish" <<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>> wrote: > > I think the mistake here is mapping the Abbrev constant to Unwanted. I'd say it was probably worth preserving. Why? What does it mean outside of HOL4? > > 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 <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> wrote: > >> On Tue, Dec 6, 2011 at 7:36 PM, Joe Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> 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 <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 > >>>>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > >>>>>> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > >>>> > >>>> _______________________________________________ > >>>> opentheory-users mailing list > >>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > >>>> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > >>> > >>> _______________________________________________ > >>> opentheory-users mailing list > >>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > >>> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > >> > >> _______________________________________________ > >> opentheory-users mailing list > >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > >> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > > > > _______________________________________________ > > opentheory-users mailing list > > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > > <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/mailman/listinfo/opentheory-users">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >