Re: [ProofPower] z_%mem%_seta_conv issue
Phil, On 2 Aug 2011, at 16:26, Phil Clayton wrote: > On 31/07/11 16:33, Rob Arthan wrote: >> Phil, >> >> On 30 Jul 2011, at 17:18, Rob Arthan wrote: >> >>> >>> On 28 Jul 2011, at 18:10, Phil Clayton wrote: >>> There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema declaration. >>> >>> Yes. This needs to be fixed. >> >> I hope the work-around I posted was useful. >> >> I have been thinking about how to fix z_%mem%_seta_conv and can do so, >> but I don't like the fix much, so I thought I would share it with you >> (and the list) to see if we can come up with something neater. The >> fundamental problem is with the conversion z_%exists%_intro_conv1... > > My current understanding is that z_%exists%_intro_conv1 is being passed a > denormalized Z term. Are conversions supposed to handle denormalized Z terms? There is no convention on what a conversion should or shouldn't do other than return an equation whose LHS is alpha-equivalent to the term passed as argument to the conversion. I don't quite know what you mean by "denormalized". I would just say "not Z". But the argument of z_%exists%_intro_conv1 is expected to be Z, it's expected to be an HOL existential quantification whose matrix is like the matrix of a Z existential quantification when viewed as HOL. It make sense to me for z_%exists%G_intro_conv1 to make up for something that is very likely to have gone wrong with the matrix from the Z point of view when it was being manipulated as HOL. (This applies to the analogous conversions for universal and unique existential quantifications too). > Thinking that they weren't, I was going to look into a fix to > seq_binder_simple_%alpha%_conv or prot_%alpha%_conv to prevent this happening > in the first place. If it can be made to work, is that an acceptable > solution? I don't think it is desirable (a) because it is unnecessary in several of the places where those conversions are used (the documentation is overcautious/wrong about this as far as I can see, e.g. I don't believe z_%mu%_rule ever needs rename Z bound variables) and (b) because it requires a "deep" term traversal: essentially you will have to map z_dec_rename%down%s_conv over the whole term. I would rather leave it to the user to decide whether to do that. I think it will be more useful to make z_%exists%_intro_conv and friends more accommodating. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] z_%mem%_seta_conv issue
On 31/07/11 16:33, Rob Arthan wrote: Phil, On 30 Jul 2011, at 17:18, Rob Arthan wrote: On 28 Jul 2011, at 18:10, Phil Clayton wrote: There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema declaration. Yes. This needs to be fixed. I hope the work-around I posted was useful. Yes, thanks - I have that working. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] z_%mem%_seta_conv issue
On 31/07/11 16:33, Rob Arthan wrote: Phil, On 30 Jul 2011, at 17:18, Rob Arthan wrote: On 28 Jul 2011, at 18:10, Phil Clayton wrote: There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema declaration. Yes. This needs to be fixed. I hope the work-around I posted was useful. I have been thinking about how to fix z_%mem%_seta_conv and can do so, but I don't like the fix much, so I thought I would share it with you (and the list) to see if we can come up with something neater. The fundamental problem is with the conversion z_%exists%_intro_conv1... My current understanding is that z_%exists%_intro_conv1 is being passed a denormalized Z term. Are conversions supposed to handle denormalized Z terms? Thinking that they weren't, I was going to look into a fix to seq_binder_simple_%alpha%_conv or prot_%alpha%_conv to prevent this happening in the first place. If it can be made to work, is that an acceptable solution? Phil ...that turns HOL existentials of a suitable form (specifically the form returned by z_%exists%_elim_conv2) into Z existentials. z_%exists%_intro_conv1 doesn't know how to deal with the case when substitutions have caused bound variables to be renamed - but that case can fairly easily be fixed using z_dec_rename%down%s_conv. Unfortunately z_dec_rename%down%s_conv depends on z_rename%down%s_conv which is defined in the DTD043 module which depends on DTD042 (where z_%mem%_seta_conv lieves) and DTD041 (where z_%exists%_intro_conv1 lives). Teasing out the dependencies so that z_rename%down%s_conv can be moved into DTD041 doesn't look very promising, but maybe I haven't tried hard enough. There may be something I could do with the hated functors, but I don't know what. So the only option is to have a hook in DTD041 for setting a conversion that z_%exists%_intro_conv1 uses where z_dec_rename%down%s_conv is needed and calling that hook (and then filtering it out of the signature) at the end of DTD041. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] z_%mem%_seta_conv issue
Phil, On 30 Jul 2011, at 17:18, Rob Arthan wrote: > > On 28 Jul 2011, at 18:10, Phil Clayton wrote: > >> There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming >> of bound variables is required but the bound variables are introduced by a >> schema declaration. > > Yes. This needs to be fixed. I hope the work-around I posted was useful. I have been thinking about how to fix z_%mem%_seta_conv and can do so, but I don't like the fix much, so I thought I would share it with you (and the list) to see if we can come up with something neater. The fundamental problem is with the conversion z_%exists%_intro_conv1 that turns HOL existentials of a suitable form (specifically the form returned by z_%exists%_elim_conv2) into Z existentials. z_%exists%_intro_conv1 doesn't know how to deal with the case when substitutions have caused bound variables to be renamed - but that case can fairly easily be fixed using z_dec_rename%down%s_conv. Unfortunately z_dec_rename%down%s_conv depends on z_rename%down%s_conv which is defined in the DTD043 module which depends on DTD042 (where z_%mem%_seta_conv lieves) and DTD041 (where z_%exists%_intro_conv1 lives). Teasing out the dependencies so that z_rename%down%s_conv can be moved into DTD041 doesn't look very promising, but maybe I haven't tried hard enough. There may be something I could do with the hated functors, but I don't know what. So the only option is to have a hook in DTD041 for setting a conversion that z_%exists%_intro_conv1 uses where z_dec_rename%down%s_conv is needed and calling that hook (and then filtering it out of the signature) at the end of DTD041. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] z_%mem%_seta_conv issue
On 28 Jul 2011, at 18:10, Phil Clayton wrote:There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema declaration.Yes. This needs to be fixed.I'm guessing this is the reason that stripping is not working in my proof (see attached). It looks trivial but I can't see a way to finish it without getting stuck into the HOL embedding. (As shown, renaming the schema components partially helps.) Can anyone think of a Z work-around for now?I have attached a work-around where the mixed language working is not too bad (you don't see any semantic constants). Higher-order matching saves a little bit of pain in this.Regards,Rob. forphilc110730.tgz Description: Binary data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
