The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

I have not. From the single line on the documentation, i had deduced this "rewrite LEMMA by LTAC" was to be applied to a LEMMA with side-conditions baked into it, that is, something like "forall v1 v2 v3, ... -> side_condition -> lhs = rhs". In my case, the lemma's conditions for applying are not a part of the theorem.

2015-09-21 10:04 GMT-03:00 Adam Chlipala <adamc AT csail.mit.edu>:

Have you tried [rewrite LEMMA by LTAC]?  Admittedly it doesn't work quite the way I'd like, missing some rewrite opportunities, but it also only succeeds if the lemma side conditions are proved by [LTAC].

On 09/21/2015 09:02 AM, Hugo Carvalho wrote:

 Club,

I'm interested in rewriting conditionally. That is, to use the rewrite tactic only if some condition applies. For example, say we have some way of testing two numbers and will only apply the commutativity of addition if the test goes through. Right now, my tactic looks like this:

Ltac condrewrite :=
 match goal with
   | [ |- context[(plus ?a ?b)] ] =>
   let extravars := (*Some extra computation, such as reflecting a and b into ASTs*) in
   let cmp := (eval compute in (*Test goes here, depends on extravars*) ) in
    match cmp with
    | Gt => rewrite -> (plus_comm a b)
    | _ => fail
    end
 end.

As you might imagine, this is fairly unwieldy. Notice the "context[(plus ?a ?b)]"; i'm replicating, within a ltac match, something i know the rewrite tactic is perfectly capable of doing by itself.

Is there any way of doing this in a cleaner way?