The Coq mailing list

[Dan Krejsa <dan.krejsa AT gmail.com>]

Hi,

I'm quite new at Coq; sorry if this is silly or has been covered before.

Suppose I have an Gallina term of the form

   match (let pattern1 := term1 in E) [in ... return ...] with
   | pat1 => v1
   | pat2 => v2
   ...
   end

as part of a proof goal, say.  It looks to me like that _expression_ should
be equivalent to

   let pattern1 := term1 in
   match E [in ... return ...] with
   | pat1 => v1
   | pat2 => v2
   ...
   end

with the proviso that the variables bound in pattern1 in the later case
don't capture anything from the match outside of E due to their larger scope;
i.e. the transformation ought to be OK modulo a possible alpha-conversion.

If that is correct, and I want to rewrite a proof goal according to such
a transformation, how would I go about it in general? Is there a tactic that
does this sort of rewrite of Gallina built-in syntax?

Side note: In my particular case it looks like E would clearly match just one
of the specific patterns (e.g. pat1) and so the _expression_ ought to simplify;
but the first form doesn't simplify, at least not with 'simpl', and I'm assuming
that it is the 'let' _expression_ in the discriminee that is fouling things up...

- Dan