On 10 Aug 2012, at 14:11, Roger Bishop Jones wrote:
> The new version of ProofPower breaks a differential geometry
> proof (probably one of yours!) in my t003.
> Were you expecting this to happen at this stage, I thought I
> had already sucessfully built all my stuff on the version
> with the higher order rewriting?
> The changes history does not seem to be different in this
> version from what is in the 110814 version, what really
> happened since then?
> (I suppose you are going to tell me to look at the diffs, but
> there are a lot of files!).
But only one of them contains the implementation of higher-order matching!
There were two bugs in higher-order matching. (1) a form of variable capture
stopped matching working in some case when subterms of the pattern contained
type variables that appeared in the target. Now it renames type variables in
the pattern as necessary to ensure this cannot happen. (2) it did not have a
proper notion of a rigid variable, i.e., a variable that is to be treated like
a monomorphic constant. It now does and when you are rewriting the free
variables in your theorems are treated as rigid. Previously if f was free, a
pattern like f(t x) would not match anything (it isn't linear if f is an
ordinary variable), but it will match now just as if f were a constant.
Both fixes should only make rewriting work better. Of course, that can still
Proofpower mailing list