Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

```Further to my last on this topic, I now see that simple_eq_match_conv
already does what is needed for the solution of the first approximation
to the requirement.```
```
If you take a theorem of the form:

forall x, y. P(x,y) ==> A(x,y) = B(x,y)

and infer:

P(x,y) |- A(x,y) = B(x,y)

then supply this to simple_eq_match_conv you get
a conversion which will rewrite using the equation
and instantiate the assumption P(x,y) appropriately.
If you use that in a tactic the assumptions will get
subgoaled.

If you have a conversion which does that you can
apply it to get the relevant conditions (Ps), use that
to infer the corresponding equations (A=Bs) and add them
into the assumptions.
i.e. you get instances of:

P(x,y) |- A(x,y) = B(x,y)

which you asm_tac causing the equations to go into the
assumptions and the conditions to be subgoaled.

That's reasonably simple!

Probably not very intelligible, but I can fill out the details if necessary.

Roger

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
```