Ssreflect Users Discussion List

[Beta Ziliani <>]

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!