Ssreflect Users Discussion List

[t x <>]

Hi,

  Thanks for the suggestions. Due to my vagueness, I think I miscommunicated the problem (I can't get any of the techniques -- Anders, Pierre-Yves, Beta) to work.

  Here is my minimal example:

https://gist.github.com/anonymous/ca23a70041e81d762fec

  Here are the main things:

  (1) Imagine "apply Hf" is a cheap tactic.

  (2) Imagine "apply Hhy" is an ridicously expensive tactic.

  (3) I'm not looking for a tactic to solve the entire subgoal. (It's too expensive to make a recrusive call to "apply Hhy" )

  (4) I want to avoid bad rewrites.

  A good rewrite is "rewrite H_good" because all the premises can be solved by the cheap tactic (apply Hf)

  A bad rewrite is "rewrite H_bad" because some of the premises can not be solved by the cheap tactic (apply Hf)

  In plain Coq, tactic_rewrite' works -- because the solve causes "rewrite H_bad" to fail since the cheap tactic can't solve the premises.

  (5) Determining if "all the premises have been solved" by "calling 'apply Hhy' and seeing if all subgoals has been solved" is not an acceptable solution because "apply Hhy" represents an expensive tactic, and what I want are "cheap rewrites that don't land me in a unprovable state."

  (6) It might be helpful to imagine that line 8,

Variable Hhy: h y.

did not exist, and the main goal was to just end at "h y"

  (7) It's not valid to assume that there are exactly 3 premises in H_bad / H_good.

  Thanks again for everyone's patience in dealing with my confusing question.

On Tue, Sep 3, 2013 at 8:29 AM, Anders <> wrote:

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