The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I am not used to setoid_rewrite tactic, but for the generalize and set tactic, the "at m n o p …" means that only the mth, nth, oth, pth occurrences are to be generalized. I suspect it is the same for setoid_rewrite. "setoid_rewrite at m n o p …" would mean that only m n o and p occurrences are to be rewritten. For the rewrite tactics, there are cases where rewriting all occurrences lead to an error, while rewriting only a subset of them is correct. Maybe it is the same with setoids.

Example:

Parameter T : nat -> Type.
Parameter TS : forall n, T (S n) -> Type.
Parameter P : nat -> Prop.

Goal forall m n (H : S m = n) (K : T (S m)), P (S m) -> TS m K.
intros m n H.

Here H can be rewritten at occurence 2 (_:P (S m)), but not at occurrence 1 (K:T (S m)), as it would break typage in "TS m K".

2014-03-10 9:34 GMT+01:00 Jason Gross <jasongross9 AT gmail.com>:

Hi,

Can someone explain to me the difference between [setoid_rewrite ... at 1] and [setoid_rewrite ...]?  In particular, why might the first succeed when the second fails?  (This seems to me to be a bug, so I reported it, with a test case, at https://coq.inria.fr/bugs/show_bug.cgi?id=3253.)

Thanks,

Jason

--
.../Sedrikov\...