Using non-pattern equalities as rewrites

[chaudhuri]

Currently if there is a non-pattern equation in the hypotheses, it cannot be directly used as a rewrite. This can be hacked by a temporary cut (assert) between a lemma of the form forall X Y, X = Y -> foo X -> foo Y---where foo is some formula that matches the thing we want to rewrite from/to---but there should be support for directly using the equality as a rewrite. We can steal the syntax from Coq.

[kyagrd]

I actually came across the need for rewriting and had to resort to some hack, ignoring assumptions that may have capture problems and try to focus the "rewrite" on a single assumption. This happens when there is an equality between terms involving higher-order terms. For instance

P1 P2 X Y
H1: forall X Y, f (P1 X Y) (P1 X Y) -> conclusion
H2 : f (P1 X Y) (P2 X Y)
H3: P1 X Y = P2 X Y
---------------------------------------
conclusion

In these situations what I do is assert f (P1 X Y) (P1 X Y). To prove this subgoal by assertion, first clear H1. to avoid capture when rewriting and then assert P1 = P2. skip.

P1 P2 X Y
H2 : f (P1 X Y) (P2 X Y)
H3: P1 X Y = P2 X Y
H4. P1 = P2
---------------------------------------
f (P1 X Y) (P1 X Y)

Then case H4. search. proves the subgoal and I get an additional assumption, which is the result of rewriting H2 using H3, as below, to continue the proof.

P1 P2 X Y
H1: forall X Y, f (P1 X Y) (P1 X Y) -> conclusion
H2 : f (P1 X Y) (P2 X Y)
H3: P1 X Y = P2 X Y
H5:  f (P1 X Y) (P1 X Y)
---------------------------------------
conclusion

[chaudhuri]

Interesting.

I'm going to give this FR a high priority for the next release, given how often rewriting seems to be cropping up.