The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/25/2014 12:11 PM, Jason Gross wrote:
> This is untested, but I think the following should work:
>
> lazymatch goal with
>    | [ |- ?lhs = ?e ?x ] => let lhs' := (eval pattern x in lhs) in change
> (lhs' = e x)
> end

That works!  Thanks.  I didn't know that pattern was one of the tactics 
accepted by compute.  But - now I see it in the refman (page 249-250).

By the way, reflexivity doesn't work on the result, but unify does via:

match goal with |- ?A = ?B => unify A B end.

Shouldn't reflexivity be doing that?  Auto works as well, but since 
info_auto doesn't work, I don't know what auto did.

-- Jonathan

> On Fri, Jul 25, 2014 at 5:08 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > Suppose one has a goal of the form:
> >
> >    <some expression with free X> = ?42 X
> >
> > where ?42 is an evar with the proper function type.  Is there a way to
> > abstract out X from just the lhs of the equality (via beta expansion)?
> >   Like a variant of pattern that could be focused on just the lhs of the
> > equality, allowing ?42 X to unify easily with the resulting beta-expansion?
> >
> > -- Jonathan