The Coq mailing list

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

Hi Cédric,

On Mon, Feb 4, 2013 at 1:01 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

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

Yes, case_eq works for what I needed, thanks much!

By the way, the origin of the 'let (x1, x2) := x in ...' _expression_ was one of
my definitions, and I was able to rewrite the definition to avoid the 'let',
which allowed me to avoid the later difficulty in the proof.  Still, it's good to have
case_eq in my arsenal!

- Dan