Ssreflect Users Discussion List

[Bas Spitters <>]

You might be interested in ML4PG:
http://staff.computing.dundee.ac.uk/katya/ML4PG/

On Fri, Feb 6, 2015 at 5:19 AM, Daniel Selsam <> wrote:
> 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
>