[ProofPower] Type-check bug?

[Stephen Brackin]

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.

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

a(z_%exists%_tac %SZT%id S%>%);

though, I get the error response

Exception-
   Fail
      * %SZT%id S%>% cannot be interpreted as a binding that matches
      %SZT%%SML%decl_of%SZT%[f : S %fun% S]%>%%>%%>% [z_%exists%_tac.41021]
* raised
Exception+ Fail * nid SR cannot be interpreted as a binding that matches
 n'decl_ofn[f : S - S]RRR [z__tac.41021] * raised

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:

val (asms,concl) = top_goal();
val (decl,_,_) = dest_z_%exists% concl;
val decs = dest_z_decl decl;
val bvars = flat (map (fst o dest_z_dec) decs);
val x = z_type_of (hd bvars);
val y = z_type_of (%SZT%id S%>%);

As expected, I got the response:

:) val bvars = [%SZT%f%>%] : TERM list

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:

1,2c1,2
< :) val x = z_type_of (hd bvars);
< val x =
---
> :) val y = z_type_of (%SZT%id S%>%);
> val y =
133c133,134
<              v1, v2 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
---
>              v1 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
>              v2 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
138,139c139,142
<              v3, v4, v5, v6 : %pset%
<                [v7 : %bbU%; v8 : %pset% %bbU%]];
---
>              v3 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
>              v4 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
>              v5 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%];
>              v6 : %pset% [v7 : %bbU%; v8 : %pset% %bbU%]];

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.

Bug or not, will someone tell me how to get around this so that
z_%exists%_tac accepts the witness I want to provide?

Steve

Stephen Brackin
Senior Security Analyst
CygnaCom Solutions, Inc.
an Entrust company
Phone: 607-277-8211 Fax:  607-277-8211
http://www.cygnacom.com

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040919/b7976886/attachment.htm>