On 23/09/15 13:03, Lin, Yuhui wrote:
> 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.
> 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
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
