Блог

Я пытаюсь доказать теорему, включающую функцию, которая использует let выражение деструктурирования, и пытаюсь использовать match goal тактику для уничтожения правой стороны, но по какой-то причине шаблон не соответствует, как я ожидал:

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

Вот фрагмент кода, который должен быть доступен для выполнения, если у вас есть 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.