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

[Lin, Yuhui]

Hi,

I want to write a tactic to performance the following action,

assume that the goal is
h_1, … h_n |- g
and thm is
forall x, y. P(x,y) ==> A(x,y) = B(x,y)
where A(x,y) can be matched with a subterm of the current goal. After applying the tactic, the following subgoals are generated:

1)h_1, … h_n, A(x’,y') = B(x’,y') |- g
2) h_1, … h_n |- P(x’,y’)

where x and y are instantiated as the related terms (x’ and y') in the matched subterm.

Is there any existing function I can use? If not, how can I write such a tactic ? Thanks in advance.

best,
Yuhui

-----
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

[Roger Bishop Jones]

Post by Lin, Yuhui
Hi,
I want to write a tactic to performance the following action,
assume that the goal is
h_1, … h_n |- g
and thm is
forall x, y. P(x,y) ==> A(x,y) = B(x,y)
1)h_1, … h_n, A(x’,y') = B(x’,y') |- g
2) h_1, … h_n |- P(x’,y’)
where x and y are instantiated as the related terms (x’ and y') in the matched subterm.
Is there any existing function I can use? If not, how can I write such a tactic ? Thanks in advance.
I don't know an easy way to traverse a term other than for a conversion,
so I might go for a conversion which

I don't think there is anything which easily yields that result.

I'm not the best person to advise, not that hot on tactical programming,
but here's my
first thoughts on how to do something like that.

It looks to me like it would probably be easier to implement something which
actually rewrites the term g with the relevant equations, since that
functionality
can be achieved with the existing rewrite facilities by adding a new way
of creating
the elements of the discrimination nI don't know an easy way to traverse
a term other than for a conversion,
so I might go for a conversion whichets which control the rewriting.
So I'll say a bit about how I would go about doing that, and that may be a
good enough clue to how to do what you want.

The entries in the discrimination nets which are normally generated from the
theorems supplied for rewriting include a conversion created by applying:

simple eq match conv1

to the equational theorems derived by canonicalising the rewriting theorems.
(look in the reference manual to see what it does).

You need an alternative function which will take a conditional rewrite and
do something similar, i.e. perform the rewrite on the right of the condition
creating a theorem which has the appropriately instantiated left hand side
of the condition in the assumptions.

Lets call that: cond_eq_match_conv

You may be able to figure that out by looking at the code for simple eq
match conv1.

If you then rewrite using discrimination net entries involving conditional
equations and using cond_eq_match_conv on the right, then the rewrite
will result in equations with assumptions.
If this is done in a goal oriented proof then the goal package will
automatically
add subgoals for the new assumptions, so the effect is that rewriting
tactics
implement the following:

Under the conditions you specified you get the following new subgoals:

1)h_1, … h_n |- g [ B(x',y')/ A(x',y')]
2) h_1, … h_n |- P(x’,y’) where x and y are instantiated as the related
terms (x’ and y') in the matched subterm.

Then you need to figure out a convenient way of getting the required
equational context for the rewriting.

As to how to get exactly what you wanted, I haven't figure that out.
I don't know an easy way to traverse a term other than for a conversion,
so I might go for a conversion which does something like the above,
but instead of adding the P instances as assumptions, adds the instances
of the A = B equations which were used.
Then, instead of plugging it into the rewrite system, just map it over
the goal conclusions (MAP_C or a variant), and extract the assumptions
from the resulting
theorem (and throw it away), then prove all the relevant instances of
P |- A = B from the theorem and add them into the assumptions
of the goal using asm_tac (causing the corresponding instances of P to
be subgoaled).

I wrote all this assuming you wanted to pick up multiple matches if the
exist, but of course you could get it to stop after the first one.

As to how usable this would be that is moot.
It may well produce unprovable subgoals, you would expect a conditional
rewriting facility to discharge the condition before doing the rewrite.


Roger Jones

[Roger Bishop Jones]

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

[Lin, Yuhui]

Hi Roger,

Thank you very much. Your solution works perfectly for me. Just be a little curious, what dose the following promoted message means when applying the tactic

'Tactics proof introduced the subgoal 2 but did not request it as a subgoal"


best,
Yuhui

Yuhui,
See attached a rough cut at what you were looking for.
Roger Jones
<cond_rewrite.doc>

-----
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.

[Roger Bishop Jones]

Post by Lin, Yuhui
Thank you very much. Your solution works perfectly for me. Just be a little curious, what dose the following promoted message means when applying the tactic
'Tactics proof introduced the subgoal 2 but did not request it as a subgoal"

That's because the tactic doesn't really work properly, and the goal
package had
to intervene to patch up the proof.
I mentioned in my description of a suggested method that if a conversion
produces
an equation with extra assumptions, then if you use it as a tactic those
assumptions
will get subgoaled.
This is true, and it works, but the tactic is not really doing what it
should and the
subgoal package is fixing the problem,

I thought that was a bit off, and also I wasn't sure that the subgoal
created by
the goal package would always have the right assumptions so I did it
properly,
and include the result, for the record, below,

Its still very crude, some of the choices are arbitrary and not thought out
(like the parameters to prim_rewrite_conv, also the canon could do more)
But it does what was asked for.

(I did it in theory real because there was a nice conditional equation
available there for testing it, it doesn't really need to be there)

Roger


open_theory "%bbR%";

fun thm_eqn_cxt1 (thm : THM) : TERM * CONV = (
let val cnv = simple_eq_match_conv thm
val lhs = fst(dest_eq(snd(strip_%forall% (concl thm))));
in
(lhs, cnv)
end);

fun cond_rewrite_canon thm = [strip_%implies%_rule (all_%forall%_elim thm)];

val cond_rewrite_conv = prim_rewrite_conv
empty_net
cond_rewrite_canon
(Value thm_eqn_cxt1)
MAP_C
[];

cond_rewrite_conv [%bbR%_over_times_over_thm] %<%2./3.*4./5.%>%;

fun cond_rewrite_tac thm (asml, conc) =
let val thm2 = cond_rewrite_conv [thm] conc
in MAP_EVERY (fn p => (LEMMA_T p
(fn q => MAP_EVERY asm_tac (forward_chain_rule [thm] [q]))))
(asms thm2)
(asml, conc)
end;

set_goal ([%<%H1:BOOL%>%, %<%H2:BOOL%>%], %<%2./3.*4./5. = 0.%>%);
a(cond_rewrite_tac %bbR%_over_times_over_thm);