`match goal` doesn't match let destructuring expression

Question

I'm trying to prove a theorem involving a function that uses a destructuring let expression, and am trying to use the match goal tactic to destruct the right hand side, but for some reason the pattern doesn't match like I'd expect it to:

match goal with
  (* why doesn't this match? *)
  | [ |- context[let _ := ?X in _] ] => destruct X
end.

Here's a code snippet that should be runnable, if you have Cpdt from Certified Programming with Dependent Types (I'm a huge convert to his style of automation).

I have found a proof, but I'm planning on proving many more theorems with a similar shape, and I'd like to have an automated tactic capable of proving many of them.

Set Implicit Arguments. Set Asymmetric Patterns.
Require Import List Cpdt.CpdtTactics.
Import ListNotations.

Section PairList.
  Variable K V: Set.
  Variable K_eq_dec: forall x y: K, {x = y} + {x <> y}.
  Variable V_eq_dec: forall x y: V, {x = y} + {x <> y}.

  Definition Pair: Type := (K * V).
  Definition PairList := list Pair.
  (* ... *)

  Fixpoint set (l: PairList) (key: K) (value: V): PairList :=
    match l with
    | [] => [(key, value)]
    | pr::l' => let (k, _) := pr in
      if K_eq_dec key k then (key, value)::l' else pr::(set l' key value)
    end.

  Theorem set_NotEmpty: forall (before after: PairList) key value,
    after = set before key value -> after <> [].
  Proof.
    intros before after. induction before.
    - crush.
    - intros. rewrite -> H. simpl.

      (* the context at this step:
        1 subgoal

          K, V : Set
          K_eq_dec : ...
          V_eq_dec : ...
          a : Pair
          before : list Pair
          after : PairList
          IHbefore: ...
          key : K
          value : V
          H : ...
          ============================
          (let (k, _) := a in
           if K_eq_dec key k
           then (key, value) :: before
           else
            a :: set before key value) <> []
      *)

      (* a successful proof
        destruct a.
        destruct (K_eq_dec key k); crush.
      *)

      match goal with
        (* why doesn't this match? *)
        | [ |- context[let _ := ?X in _] ] => destruct X
        | [ |- context[(() <> [])] ] => idtac X
      end.
      (* the above command prints this:
        (let (k, _) := a in
         if K_eq_dec key k
         then (key, value) :: before
         else
          a :: set before key value)
      *)
  Qed.
End PairList.

Answer 1

Destructuring lets are actually matches, so you need to look for a match. When a tactic doesn't match, you can see all expressions in your goal desugared with Set Printing All.

      match goal with
        | [ |- context[let _ := ?X in _] ] => destruct X
        (* ADD THIS LINE *)
        | [ |- context[match ?X with _ => _ end]] => destruct X
        | [ |- context[(() <> [])] ] => idtac X
      end.