[metis-users] rewrite structure in Metis

[Joe Hurd]

Hi James,

> In general, the problem with backtracking is that most Metis structures are
> well set up to accept new clauses but are much less happy about giving them
> back again! (This is not a criticism of Metis, I think most theorem provers
> are written in the same way.)

I think you have put your finger on the root of the problem here, and
I can illustrate why this is in a simple example.

Suppose the rewrite set contains one equation

{ a = b }

and down one branch of a split the same equation happens to be added
(which I will mark with a *):

{ a = b, a =* b }

During inter-reduction it might be the case that the original equation
is rewritten:

{ b = b,  a =* b }

which would then get thrown out as a useless instance of reflexivity:

{ a =* b }

If you attempted to modify this rewrite set when going down the other
branch you would be left with the empty set of rewrites

{ }

which is incomplete.

This is a simple example which would probably not appear in practice
because the second equation would be simplified before it could be
added to the rewrite set and inter-reduced, but it is illustrative of
a class of problems deriving from an attempt to delete rewrites after
they have affected the state in hard-to-undo ways.

One solution to this is save the original rewrite set at the split
point, and then add extra equations that have been derived down one
branch that do not depend on the split. Then you're only adding
equations but obtaining the benefit of the extra equations that do not
depend on the split.

Does this strategy work in your use-case?

Cheers,

Joe