The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Tuesday 14 August 2007 03:37:02 Sean Wilson wrote:
> Hi,
>
> I'm wanting to develop a Coq tactic that, given a database of rewrite
> rules, will perform a search of all possible ways the current goal can be
> rewritten. I'm wanting to experiment with the use of heuristics to guide
> the search.
>
> Specifically, if I had the rewrite rules "a=b", "b=c" and the goal "a+a=b",
> the first stage in the search would be to use each rewrite only once on the
> goal in all possible ways to produce the new goals "b+a=b", "a+b=b"
> and "a+a=c". I would then repeat this for the new goals, using heuristics
> to guide which goals to explore.
<snip>

Hi,

I've been looking at the OCaml implementation of the rewrite tactic. The 
tactic uses the eq_ind_r theorem to justify the substitution it makes. The 
eq_ind_r function is used with the rewrite rule and a modified version of the 
goal to indicate where the substitutions takes place. Here is a short example 
of some trivial goals involving rewrites:

Variables a f: Prop.

Axiom w5 : a = f.

Goal (a/\a) = (f/\f).
(* Change all "a" terms to "f" *)
exact (eq_ind_r (fun P : Prop => (P /\ P) = (f /\ f)) (refl_equal (f /\ f)) 
w5).
Qed.  

Goal (a/\a) = (a/\f).
(* Change first "a" term to "f" *)
exact (eq_ind_r (fun P : Prop => (a /\ P) = (a /\ f)) (refl_equal (a /\ f)) 
w5).
Qed.  

Goal (a/\a) = (f/\a).
(* Change second "a" term to "f" *)
exact (eq_ind_r (fun P : Prop => (P /\ a) = (f /\ a)) (refl_equal (f /\ a)) 
w5).
Qed.

The default behaviour of "rewrite w5" (i.e. replacing all "a" terms) produced 
the term used in the first proof. The second and third proofs show how 
changing the position of the "P" in the supplied function to eq_ind_r changes 
the places in the term where rewriting takes place.

What I want to do is write a OCaml function that produces a list of all 
possible ways a rewrite can be used once. For instance, the last goal has 
three places where "a" could be replaced with an "f" so I would want to 
produce three rewritten goals.

I've traced the OCaml code and see can see where it builds up an unification 
problem of using eq_ind_r with the goal and the rewrite as parameters. The 
unification algorithm then produces a term similar to the one used in the 
first goal above. However, I can't work out how to tell it to only unify 
the "P" parameter (like that above) to only one term. I also need the unifier 
to return all possible matches and not just the first one.

Can anyone help me with this? I'd be interested in talking to any Coq 
developers who know anything about the OCaml code as I'm finding it very hard 
get going here.

Thanks,

Sean