The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

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.


An `at' argument to the rewrite tactic would certainly be nice, but
there is also an other situation which I find even more frustrating:
let's do exactly the same thing with a partial order:

Variable le: nat -> nat -> Prop.
Axiom le_refl: reflexive _ le.
Axiom le_trans: transitive _ le.
Add Relation nat le 
reflexivity proved by le_refl
  transitivity proved by le_trans as le_Relation.

Variables a b c: nat.
Axiom ab: le a (a+b).
Goal le a (a+c).
(* set (x := a) in |- * at -1. *)
rewrite ab. (* fails *)

Setoid fails to rewrite because it attempts to rewrite both
occurrences, and the one on the right cannot be rewritten
(contravariance stories). The same trick as before does the job, but
in this case, it seems to me that a more intuitive (and useful)
behaviour would be to rewrite all the occurrences of the left
hand-side...

Could this easily be fixed ?

Damien


Edsko de Vries 
<devriese AT cs.tcd.ie>
 writes:

> Hi,
>
> Suppose I have something like
>
>   Lemma foo : equiv a'' (or a'' a')
>
> Say I want to rewrite the first occurrence of a'' with (or a'' false).
> When I do
>
>   rewrite <- (or_id a'').
>
> both occurrences of a'' are replaced (following Adam's suggestion I've
> setup the setoid stuff for my boolean expressions). If I do
>
>   pattern a'' at 1 ; rewrite <- (or_id a'')
>
> it complains about the argument being in a covariant position.
>
>   replace a'' at 1 with (or a'' false)
>
> gives me a subgoal
>
>   a'' = or a'' false
>
> which is too strong (they are merely equivalent, not equal), and 
> setoid_replace does not seem to have an 'at 1' option. 
>
> Is there a way to apply the setoid rewriting to a particular occurrence
> only?
>
> Thanks,
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club