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.

## Advertising

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