The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

So does

generalize dependent x; rewrite LeftIdentity; intros.

which is essentially what the [simultaneous_rewrite] tactic does, and what I had settled on doing before, which was

repeat match goal with

           | [H : _ |- _ ] => generalize H; clear H

         end;

  repeat (repeat rewrite LeftIdentity; try intro); intros.

I'm looking for a general tactic that doesn't rely on me knowing where a particular term occurs or what it depends on, like [rewrite LeftIdentity in *] and [subst].

-Jason

On Mon, Jul 2, 2012 at 3:21 PM, Chung-Kil Hur <gil.hur AT gmail.com> wrote:

revert x e; rewrite LeftIdentity; intros.
works.

I am not sure whether this is what you want.

- Gil

On Mon, Jul 2, 2012 at 8:16 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
> [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
>> >
>> >
>
>