“匹配目标”与匹配条件不符，可以破坏表达式

如何解决“匹配目标”与匹配条件不符，可以破坏表达式

我正在尝试证明一个涉及使用解构let表达式的函数的定理，并且正在尝试使用match goal策略来破坏右侧，但是由于某种原因，模式不符合我的预期：

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

如果您有Certified Programming with Dependent Types的Cpdt，那么这是一个应该可运行的代码段（我非常喜欢他的自动化风格）。

我找到了一个证明，但我打算证明更多具有相似形状的定理，并且我希望有一种能够证明其中许多定理的自动化策略。

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.

解决方法

解构函数实际上是匹配项，因此您需要查找match。如果战术不匹配，您可以看到目标中所有用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.