Ssreflect Users Discussion List

[Anders <>]

You can also do:

rewrite H; do ?Tactic.

This will rewrite with H and then try to solve the generated goals by Tactic.

--
Anders

On Tue, Sep 3, 2013 at 9:50 AM, Pierre-Yves Strub <> wrote:

BTW, in addition to (last k tactic) and (first k tactic), ssreflect could come with (last -k tactic) and (first -k tactic) for achieving:

  last k idtac || [tactic] and first k idtac || [tactic]

Pierre-Yves.

On 09/03/2013 09:48 AM, Pierre-Yves Strub wrote:

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 <
<mailto:>> 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 <
    <mailto:>> 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 <
    <mailto:>> 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 <
    <mailto:>> 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!
     >
     >