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

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.


Proofpower mailing list

Reply via email to