Ssreflect Users Discussion List

[Daniel Selsam <>]

Hi,

Is there a way to enumerate all matches of a given rewrite rule in the goal, 
so that an automated system could try them all?

For example, suppose we have a goal:

<<
  m : nat
  n : nat
  p : nat
  ============================
   m + (n + p) = (n + p) + m
>>

I would like to be able to query

<<
rewrite_matches addnC.
>>

and get the response:

<<
[ (m,n+p,1), (n,p,2), (n+p,m,1) ]
>>

so that:

<<
rewrite (addnC m (n+p))
rewrite {1}(addnC n p)
rewrite {2}(addnC n p)
rewrite (addnC (n+p) m)
>>

are the four possible ways of rewriting left to right with [addnC].

I assume there is a way to write this tactic with only a few lines of OCaml, 
but I am not sure how.

Thanks very much,

Daniel