The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[replace] has no [in *] or [in H] variant, in so far as I can tell, and [rewrite _ in *] fails in the case I'm interested in, I presume because it tries to rewrite things one at a time, rather than all-together, like [subst].  Here's an example of a solution my mentor (Adam) came up with, and a slightly simplified example of the code that I use it in:

Set Implicit Arguments.

(* rewrite fails if hypotheses depend on one another.  simultaneous_rewrite does not *)

Ltac simultaneous_rewrite' E :=

  match type of E with

    | ?X = _ => generalize E; generalize dependent X; intros; subst

  end.

Ltac simultaneous_rewrite E :=

  match type of E with

    | forall x : ?T, _ =>

      let y := fresh in evar (y : T);

        let y' := (eval unfold y in y) in clear y; simultaneous_rewrite (E y')

    | ?T = _ => let H := fresh in

      match goal with

        | [ _ : context[?F] |- _ ] =>

          assert (H : T = F) by reflexivity; clear H

      end; simultaneous_rewrite' E

  end.

Parameter Object : Type.

Parameter Morphism : Object -> Object -> Type.

Parameter Identity : forall o, Morphism o o.

Parameter Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'.

Parameter LeftIdentity : forall s d (m : Morphism s d), Compose (Identity _) m = m.

Goal forall X Y (f : Morphism Y X)

  (x : { m : Morphism Y X | Compose (Identity _) f = m })

  (e : forall x' : { m : Morphism Y X | Compose (Identity _) f = m },

    x' = x),

  False.

  intros.

  try rewrite LeftIdentity in *. (*Error: Nothing to rewrite.*)

  try change (Compose (Identity _) f) with f in *. (*Error: Not convertible.*)

  replace (Compose (Identity _) f) with f by (rewrite LeftIdentity; reflexivity). (* does nothing/has no 'in _' variant *)

  simultaneous_rewrite LeftIdentity.

Is there a simpler/built-in way to do this?

Thanks!

-Jason

On Mon, Jul 2, 2012 at 4:29 AM, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

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
>
>