Ssreflect Users Discussion List

[t x <>]

This also seems like an important limitation in that often times, more than one rule can work for rewrite -- and if Ltac picks the wrong rewrite rule, I get to a state that is unprovable. Thus, it's important to me that when I do rewrites, I can check whether all of the premises the rewrite depends on can be easily solved.

On Tue, Sep 3, 2013 at 6: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!