The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

I am not sure that Guillaume's suggestion has been understood
completely here. In the following (the ".." is real syntax here)

tac;[> tac' | tac''..].

This will apply tac' to the first subgoal and tac' to *all others* ASFAIU.

Best regards,
Pierre


2015-12-21 12:42 GMT+01:00 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