The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Fri, Feb 08, 2008 at 09:21:43AM -0500, Damien Pous wrote:
> Hi,
> 
> I had the same problem two months ago, you can use the set tactic in
> order to isolate the occurrence of the term you want to rewrite:
> 
> Require Import Setoid.
> Variable meq: nat -> nat -> Prop.
> Axiom meq_refl: reflexive _ meq.
> Axiom meq_trans: transitive _ meq.
> Axiom meq_sym: symmetric _ meq.
> Add Relation nat meq 
> reflexivity proved by meq_refl
>   symmetry proved by meq_sym
>     transitivity proved by meq_trans as meq_Relation.
> 
> Variables a b c: nat.
> Axiom ab: meq a (a+b).
> Goal meq a (a+c).
> set (x := a) in |- * at -1.
> rewrite ab.

That's a nice trick! I tried to abstract it to a tactic:

  Ltac rewrite_first t t' := 
    let H := fresh in
    set (H := t) in |- * at -1 ;
    rewrite t' ;
    subst H.

which can then be used as

  Variables a b c: nat.
  Axiom ab: meq a (a+b).
  Goal meq a (a+c).
  rewrite_first a ab.

which is reasonably nice (we should introduce some custom notation,
perhaps). It would be nicer if we should pass in a position, but
unfortunately if we define

  Ltac rewrite_at t t' pos := 
    let H := fresh in
    set (H := t) in |- * at pos ;
    rewrite t' ;
    subst H.

then
  
  rewrite_at a ab 1.

gives

  User error: Ltac variable pos is bound to a term
    which cannot be coerced to an integer
 
and 

  rewrite_at a ab -1.

even gives a syntax error at the '-'

  Syntax error: '.' or '...' expected after [tactic:tactic] (in
    [subgoal_command])

I don't know if that can be solved. 

Thanks,

Edsko