The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

To complete Arnaud's answer. It is unlikely you want to have a subst
equivalent for non variable terms. subst replaces a variable by it
value everywhete *and then* removes the equality used for that from
the context. This is a tactic "with no loss of information" because it
only works on variables. Doing this with t = u where t and u are two
non variable terms would lose some important information. You can
always do "cear H" if you want to forget a hypothesis H anyway.

Cheers,
Pierre Courtieu

2012/7/2 Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>:
> replace
> rewrite
>
> These are what you are looking for.
>
>
> On 2 July 2012 06:25, Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
>>
>> Hi,
>> I was wondering if there's a version of [change] that requires only
>> equality, rather than convertibility, or a version of [subst] that applies
>> to terms and not just identifiers?  [change] only works when the terms are
>> convertible, and [subst] only works if one them is an identifier.  I wrote 
>> a
>> version myself (see below), but I'm wondering if there's something that 
>> does
>> this in Coq, already.  Thanks.
>>
>> (* equivalent to [change x with y], but requires that [x = y] be provable
>> with [taceq],
>>    rather than that [x] and [y] are convertible *)
>> Tactic Notation "generalized_change" constr(x) "with" constr(y) "by"
>> tactic(taceq) :=
>>   let xeqy := fresh in
>>     assert (xeqy : x = y) by (taceq || symmetry; taceq);
>>       let x' := fresh in
>>         pose x as x';
>>           let xeqx' := fresh in
>>             let x'eqy := fresh in
>>               assert (xeqx' : x = x') by reflexivity;
>>                 change x with x';
>>                   assert (x'eqy : x' = y) by (transitivity y; exact xeqy
>> || symmetry; exact xeqy || trivial);
>>                     clear xeqx';
>>                       clearbody x';
>>                         subst x';
>>                           clear xeqy.
>>
>> -Jason
>
>