<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<META NAME="Generator" CONTENT="MS Exchange Server version 5.5.2657.73">
<TITLE>Type-check bug?</TITLE>
</HEAD>
<BODY>
<P><FONT SIZE=2>I'm working with a schema that contains proprietary information, so I can't send the actual data, but I've prepared sanitized extracts from it that show the problem. I've apparently run into a ProofPower type-checking bug and need a work-around.</FONT></P>
<P><FONT SIZE=2>I'll call the schema I'm working with S. S is a complicated generic schema, but I'm trying to prove a trivial function-existence theorem about it that can take the identity relation on S as the existential witness. When I execute</FONT></P>
<P><FONT SIZE=2>a(z_%exists%_tac %SZT%id S%>%);</FONT>
</P>
<P><FONT SIZE=2>though, I get the error response</FONT>
</P>
<P><FONT SIZE=2>Exception-</FONT>
<BR><FONT SIZE=2> Fail</FONT>
<BR><FONT SIZE=2> * %SZT%id S%>% cannot be interpreted as a binding that matches</FONT>
<BR><FONT SIZE=2> %SZT%%SML%decl_of%SZT%[f : S %fun% S]%>%%>%%>% [z_%exists%_tac.41021] * raised</FONT>
<BR><FONT SIZE=2>Exception+ Fail * nid SR cannot be interpreted as a binding that matches</FONT>
<BR><FONT SIZE=2> n'decl_ofn[f : S - S]RRR [z__tac.41021] * raised</FONT>
</P>
<P><FONT SIZE=2>Following Philip Clayton's suggestion, I computed and compared the Z types of the existentially quantified bound variable in the goal and the identity relation on S as follows:</FONT></P>
<P><FONT SIZE=2>val (asms,concl) = top_goal();</FONT>
<BR><FONT SIZE=2>val (decl,_,_) = dest_z_%exists% concl;</FONT>
<BR><FONT SIZE=2>val decs = dest_z_decl decl;</FONT>
<BR><FONT SIZE=2>val bvars = flat (map (fst o dest_z_dec) decs);</FONT>
<BR><FONT SIZE=2>val x = z_type_of (hd bvars);</FONT>
<BR><FONT SIZE=2>val y = z_type_of (%SZT%id S%>%);</FONT>
</P>
<P><FONT SIZE=2>As expected, I got the response:</FONT>
</P>
<P><FONT SIZE=2>:) val bvars = [%SZT%f%>%] : TERM list</FONT>
</P>
<P><FONT SIZE=2>I compared the types by doing everything in a Linux typescript and running diff on appropriate segments of the result. After sanitization, I got the following:</FONT></P>
<P><FONT SIZE=2>1,2c1,2</FONT>
<BR><FONT SIZE=2>< :) val x = z_type_of (hd bvars);</FONT>
<BR><FONT SIZE=2>< val x =</FONT>
<BR><FONT SIZE=2>---</FONT>
<BR><FONT SIZE=2>> :) val y = z_type_of (%SZT%id S%>%);</FONT>
<BR><FONT SIZE=2>> val y =</FONT>
<BR><FONT SIZE=2>133c133,134</FONT>
<BR><FONT SIZE=2>< v1, v2 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>---</FONT>
<BR><FONT SIZE=2>> v1 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>> v2 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>138,139c139,142</FONT>
<BR><FONT SIZE=2>< v3, v4, v5, v6 : %pset%</FONT>
<BR><FONT SIZE=2>< [v7 : %bbU%; v8 : %pset% %bbU%]];</FONT>
<BR><FONT SIZE=2>---</FONT>
<BR><FONT SIZE=2>> v3 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>> v4 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>> v5 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];</FONT>
<BR><FONT SIZE=2>> v6 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%]];</FONT>
</P>
<P><FONT SIZE=2>I don't use commas in the declaration portion of any schema. Apparently, different pieces of ProofPower software use different representations for Z types, and these different representations sometimes cause identical types to compare as unequal.</FONT></P>
<P><FONT SIZE=2>Bug or not, will someone tell me how to get around this so that z_%exists%_tac accepts the witness I want to provide?</FONT>
</P>
<P><FONT SIZE=2>Steve</FONT>
</P>
<P><FONT SIZE=2>Stephen Brackin</FONT>
<BR><FONT SIZE=2>Senior Security Analyst</FONT>
<BR><FONT SIZE=2>CygnaCom Solutions, Inc.</FONT>
<BR><FONT SIZE=2>an Entrust company</FONT>
<BR><FONT SIZE=2>Phone: 607-277-8211 Fax: 607-277-8211</FONT>
<BR><FONT SIZE=2><A HREF="http://www.cygnacom.com" TARGET="_blank">http://www.cygnacom.com</A></FONT>
</P>
</BODY>
</HTML>