The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you're ok with copy/paste, you can use the [change] tactic.  If you want to remove the let entirely, you can do something like [cbv beta iota].

Automatically saving the things which are [let] is harder.  The following tactic should work, assuming that [let pattern1 := term1 in E] doesn't appear anywhere else in the goal, and assuming that it is a simple let pattern (i.e., pattern1 is just a variable name).  Someone with more ltac knowledge than I might have an idea of how to take care of the more general case; [let] is just syntactic sugar for a [match], but I don't know how to talk about the cases of a match without knowing the names of the constructors.

Goal match (let x := 2 in (x + x)%nat) with

           | O => True

           | S n => n = n

         end.

    match goal with

      | [ |- match (let x := ?term1 in @?E term1) with _ => _ end ] =>

        match goal with

          | [ |- context G[let x := term1 in @?E term1] ] =>

            let term1' := fresh in

            pose term1 as term1';

              let G' := context G[E term1'] in

              change G'; revert term1'

        end

    end.

More generally, you could do

    Goal match (let (x, y) := (2, 3) in (x + y)%nat) with

           | O => True

           | S n => n = n

         end.

    Ltac fun_app_to_let term tac :=

      match term with

        | ?f ?x => let x' := fresh in

                   pose x as x';

                     fun_app_to_let f ltac:(fun term' =>

                                              let term'' := constr:(term' x') in 

                                              tac term'';

                                           try revert x')

        | (fun _ => _) => tac term

      end.

    Ltac move_let :=

      cbv iota;

      match goal with

        | [ |- match ?E with _ => _ end ] =>

          match goal with

            | [ |- context G[E] ] =>

              fun_app_to_let E ltac:(fun x =>

                                       let G' := context G[x] in

                                       change G')

          end

      end.

    move_let.

This doesn't preserve the patterns of the [let] (i.e., it turns [let (x, y) := (2, 3)] into [let x := 2 in let y := 3], and it destroys all your other [let]s (with [cbv iota]), but it moves them outside the match so you can, e.g., intro them.

-Jason

On Mon, Feb 4, 2013 at 4:12 PM, Dan Krejsa <dan.krejsa AT gmail.com> wrote:

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