Ssreflect Users Discussion List

[Beta Ziliani <>]

You can also use normal tactic concatenation:

rewrite H ; [|omega|omega].

will solve the last two goals using omega. Or

rewrite H ; try omega.

will try omega on every sub-goal.

Any of the solution proposed work with any other tactic, not only rewrite.





On Tue, Sep 3, 2013 at 8:22 AM, t x <> wrote:
> With apologies for my inability to comprehend the ssreflect manual/tutorial,
> does this generalize to when I have more than one hypothesis, i.e. a goal
> of:
>
> H: P1 -> P2 -> P3 -> foo = bar
>
> and I want to do a "rewrite H", and tell Coq to only go on if P1, P2, and P3
> can all be solved by Tactic.
>
>
> It seems like in Coq wo ssreflect, there's this notion of "try to kill all
> premises with Tactic", -- and is there no way to formulate this in
> ssreflect's rewrite?
>
>
>
>
> On Tue, Sep 3, 2013 at 6:11 AM, Beta Ziliani <> wrote:
>>
>> Hi,
>>
>> First, note that ssrnat's < is not compatible with omega. Also, 3 < 5
>> can be solved by simplification. Finally, I suppose you meant "rewrite
>> H by omega", since H1 and H2 doesn't exist in your example.
>>
>> That said, you can use
>>
>> rewrite H ; last by <tactic>
>>
>> to solve the second sub-goal with the hypothesis for H.
>>
>> Hope it helps,
>> Beta
>>
>>
>> On Tue, Sep 3, 2013 at 1:58 AM, t x <> wrote:
>> > Hi,
>> >
>> >   Suppose I have something like
>> >
>> >
>> > H: forall a b, (3 < 5) -> a + 3 = 2 * b
>> > ==============================
>> >  .... a + 3 ...
>> >
>> >
>> >   In non-ssreflect Coq, I can do something like:
>> >
>> >   rewrite H1 in H2 by omega, where "omega" is used to solve (3 < 5).
>> >
>> >
>> >   Ssreflect, however, takes over the meaning of "by."
>> >
>> >
>> >   Now, is there some way in ssreflect for me to say:
>> >
>> >   rewrite H in the goal, try to solve required premises using Tactic,
>> > and
>> > have the rewrite fail if the premises can't be solved with Tactic.
>> >
>> > Thanks!
>
>