The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Still, one attractive way to proceed is to prove a lemma with extra side conditions that are not logically necessary, if your heuristic can be phrased that way.

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

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?