The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 21/12/2015 11:11, Robbert Krebbers wrote:
> Hi coq-club,
> 
> since Ssreflect's rewrite tactic is much better when dealing with goals
> involving canonical structures, I am wondering whether we can get a
> similar behavior for Coq's rewrite tactic.
> 
> I know of "Set Keyed Unification", but that does not really seem to help
> (see a simple example in the attachment).
> 
> Robbert
> 
> PS : I could just use Ssreflect's rewrite tactic instead, but I am
> really missing something like "rewrite foo by tac" as we have in vanilla
> Coq. The by flag is convenient when dealing with lemmas with many
> side-conditions (as we often have in formalizations of computer
> science). I know of "rewrite foo //", but I would really like to use an
> arbitrary tactic, such as eauto/ring/omega, and that tactic to be used
> solely on the side-conditions, not the resulting goal itself.

I suppose you already considered the following solution, but just in
case you didn't, here it is. While it is a bit more verbose and less
readable than "by tac", you can use ";[|tac..]" to achieve the same kind
of goal solving.

Best regards,

Guillaume