The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

 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?