Ssreflect Users Discussion List

[Daniel Selsam <>]

Hi,

Thank you for responding so quickly. 

I am experimenting with machine-learning assisted automated theorem proving 
in Coq. Right now my system gets stuck on some simple lemmas from ssreflect 
that involve rewriting an instance of a pattern besides the first, because I 
have not been able to systematically enumerate a sufficient action space.

Note: I realize that the ssreflect tactic language is designed for clarity 
and precision, perhaps at the expense of compatibility with automation. 
Despite this, I have chosen to start with ssreflect for two reasons. First, 
the proof style in ssreflect/MC epitomizes the style for which I think 
machine learning may be able to help: short, surgical proofs where one of the 
main challenges is retrieving a few relevant facts from a vast database; 
second, the Feit-Thompson development constitutes an ideal dataset to train 
and test on.

Any help or feedback would be greatly appreciated.

Thanks very much,

Daniel

----- Original Message -----
From: "Enrico Tassi" <>
To: 
Sent: Friday, February 6, 2015 1:07:05 AM
Subject: Re: [ssreflect] enumerating matches of a rewrite rule

On Thu, Feb 05, 2015 at 08:19:31PM -0800, Daniel Selsam wrote:
> <<
> 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.

Not so sure it can be done in 2 lines, since the rules for ssr patterns
are that that you find the first instance of the pattern and then you
look for all of its occurrences.  Here you want to find all the possible
instances and for each of them all of their occurrences.

I can surely help, but I'd like to know why you need that.  What is your
real objective?

Best,
-- 
Enrico Tassi