The Coq mailing list

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

Le Mon, 4 Feb 2013 10:57:09 -0800,
Dan Krejsa 
<dan.krejsa AT gmail.com>
 a écrit :

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

You are welcome.

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

That seems right.

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

I do not think so. In fact that reminds me a lot of η for records.

Maybe, you would be interested in the "case_eq" tactic.

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

case_eq term1.
⇓

    ∀ x1…xn, pattern1 <using x1…xn> = term1 →
    match E [in ... return ...] with
    | pat1 => v1
    | pat2 => v2
    ...
    end

which is similar to what you wanted (but not the same…).

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

Yes, once again, there is no eta-expansion for records in Coq.
So you cannot reduce the first form. The case_eq tactic would have
allowed it of course, since you almost get the second form.

> 
> - Dan