The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.

Attachment: test2.v
Description: application/extension-v