The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

By looking at your condrewrite tactic, I'd guess that you are trying to 
create canonical forms for arithmetic terms using reflection.  If so, 
maybe you should look at the code for the ring tactic?

-- Jonathan

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?