Ssreflect Users Discussion List

[t x <>]

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!