The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

There is also case_eq tactic.

And if you want to do it in a low level way (that may help to
understand how to do some funny tricks in Coq), you can do:

set (t := <expr>)
generalize (eq_refl t).
generalize t at 1.
subst t.
intros [].

Le Fri, 31 May 2013 22:32:58 -0700,
Math Prover 
<mathprover AT gmail.com>
 a écrit :

> Exactly what I was looking for. Thanks!
> 
> 
> On Fri, May 31, 2013 at 10:29 PM, Gabriel Scherer
> <gabriel.scherer AT gmail.com
> > wrote:
> 
> > Since 8.4 you can use
> >   destruct <expr> eqn:<naming intro pattern>
> >
> >
> > http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic65
> >
> > The previous (< 8.4) syntax was
> >   destruct <expr> as ... _eqn
> > or
> >   destruct <expr> as ... _eqn:<naming intro pattern>
> >
> > This "eqn:" syntax also work for "remember" and "induction".
> >
> > On Sat, Jun 1, 2013 at 4:57 AM, Math Prover 
> > <mathprover AT gmail.com>
> > wrote:
> > > Hi!
> > >
> > >   This is a minimal test case of a problem I'm running into.
> > >
> > >   Often, when I do "destruct [big complicated expression]", I
> > > would like
> > to
> > > have a hypothesis of the form:
> > >
> > > H: [big complicated expression] = value1
> > >
> > >   The reason this shows up is that often I destruct expression,
> > > but then later, when I unfold another expression, I need access
> > > to the initial destructed expression. Thus, my question: is there
> > > a way to do something like "destruct expr; but also remember that
> > > expr = ... as a hypothesis"
> > >
> > > Thanks!
> >