Ssreflect Users Discussion List

[Pierre-Yves Strub <>]

Hi,

If I understand your problem correctly, you may want this:

your-tactic; first 1 idtac || [your-second-tactic]

Pierre-Yves.

On 09/03/2013 09:25 AM, t x wrote:
> Thanks for your responses -- and apologies for a vague question.
>
> Below is a tactic I frequently use in Coq.
>
> Ltac subst_all :=
>    match goal with
>      | H: ?_ |- _ => rewrite H by (solve [intuition])
>    end.
>
>
> The idea is: if I have some hypothesis, and I can solve the premises of
> the hypothesis, let me just try to do a rewrite with it.
>
> Furthermore, when I "rewrite H", I don't know how many premises is
> generated, it could be 0, 1, 2, or ...
>
> My question is -- is there a way to write this tactic in ssreflect. The
> first response of "last" seems to imply it can only handle 1 premise,
> and the second response of "; [omega | omega ]" seems to imply I need to
> know how many premises are generated.
>
> Sorry for the confusion. Thanks again for your help.
>
>
>
> On Tue, Sep 3, 2013 at 6:28 AM, Beta Ziliani <
> <>> wrote:
>
>     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!
>      >
>      >