The Coq mailing list

[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?