The Coq mailing list

[Ilya Sergey <ilya.sergey AT imdea.org>]

Dear Hugo.

I'm curious what are the applications that require this sort of automation and why simple selective occurrence rewriting doesn't work in your case. If you're interested in rewriting specific occurrences depending on some decidable conditions on the arguments, I'd recommend to exploit the mechanism of Coq's type families as conditional rewriting rules.

The code below implements the condition-generic logic for rewriting by commutativity of the addition (it requires Ssreflect 1.5 to compile). 

Notice how the second line of the proof of the final goal rewrites just the second sum (for which the condition H holds), but not the first one. You can, indeed, instantiate the conditional rewriting lemma condAddRwP with different condition arguments c.

(****************************************************)

Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrnat. 

CoInductive CondAddRw (cond : nat -> nat -> bool) n m : nat -> Set := 

  | DoRewrite (pf : cond n m) : CondAddRw cond n m (n + m).

Lemma condAddRwP {cond : nat -> nat -> bool} {n m : nat} 

                 (c : cond n m) : CondAddRw cond n m (m + n).

Proof. by rewrite addnC; constructor. Qed.

Section TestRewrite.

Variables (n m : nat) (my_cond : nat -> nat -> bool).

Hypothesis H : my_cond n m.

Goal forall a b, (a, b) = (n, m) -> 4 * (a + b) = 4 * (m + n).

Proof.

intros.

case: (condAddRwP H)=>_. 

by case: H0=>->->.

Qed.

End TestRewrite.

(****************************************************)

I hope, it helps.

Kind regards,

Ilya

On Mon, Sep 21, 2015 at 3:02 PM Hugo Carvalho <hugoccomp AT gmail.com> 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?