Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hi,
The bracketing isn't quite right: this should read
    rewrite some_rule; first 1 [idtac] || by cheap_tactic.
Note that you can write this using plain Coq tacticals, as
    rewrite some_rule; [| by cheap_tactic..]
The two lines above are equivalent, but not quite equivalent to rewrite .. 
by, which you can still get while using ssreflect by writing
    rewrite -> some_rule by cheap_tactic.
I believe the above can use the success of cheap_tactic to decide which 
occurrence to rewrite, while the top two only control whether the rewrite 
proceeds at all. Of course using the Coq rewrite will deprive you from the 
ssreflect rewrite niceties (including multirules, redex selection, keyed 
matching, and proof-irrelevant generalization). To integrate side condition 
checking with the ssreflect term matching you should require that Coq 
discharge them using one of typeclass mechanisms: either make each side 
condition predicate a Typeclass, which could then be resolved by proof serch 
of a specific Hint Extern, of tie the condition to a specific subterm of the 
rewrite left-hand side using a Canonical Structure. The ssreflect library 
only does the latter, as it tends to be more efficient (condition checking is 
done at the same time as unification, and so can fail earlier), though this 
does requires more technical expertise.

   Cheers,
Georges

-----Original Message-----
From: Pierre-Yves Strub [] 
Sent: 03 September 2013 08:49
To: 
Subject: Re: rewrite-by

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