如何推理复杂的模式匹配？

Question

Coq允许编写复杂的模式匹配，但随后将它们分解，以便其内核可以处理它们。

例如，让我们考虑以下代码。

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

我们在列表和第二个元素上都进行模式匹配。打印f显示Coq存储了它的更复杂的版本。

Print f.
(* f = fun l : list bar => match l with
                        | [] => 2
                        | [_] => 2
                        | _ :: A :: _ => 1
                        | _ :: B :: _ => 2
                        | _ :: C :: _ => 2
                        end
     : list bar -> nat
*)

问题在于，在处理证明时f，我必须处理5个案例而不是仅处理2个案例，其中4个是多余的。

处理此问题的最佳方法是什么？是否有一种方法可以像完全定义那样推理模式匹配？

Answer 1

您说对了，因为Coq实际上简化了模式匹配，从而出现了很多冗余。但是，有一些方法可以根据您的意思进行案例分析，而不是Coq理解。

• 使用Function和功能归纳是一种方法。
• 最近，方程式还允许您定义模式匹配，为其自动导出归纳原理（可以使用调用funelim）。为了说服常见问题，可以使用观点概念。在示例中的方程式上下文中对它们进行了描述。我将详细介绍如何使您的示例适应于此。

From Equations Require Import Equations.
Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Equations discr (b : list bar) : Prop :=
  discr (_ :: A :: _) := False ;
  discr _ := True.

Inductive view : list bar -> Set :=
| view_foo : forall x y, view (x :: A :: y)
| view_other : forall l, discr l -> view l.

Equations viewc l : view l :=
    viewc (x :: A :: y) := view_foo x y ;
    viewc l := view_other l I.

Equations f (l : list bar) : nat :=
    f l with viewc l := {
    | view_foo _ _ => 1 ;
    | view_other _ _ => 2
    }.

Goal forall l, f l < 3.
Proof.
    intro l.
    funelim (f l).
    - repeat constructor.
    - repeat constructor.
Qed.

如您所见，funelim仅生成两个子目标。

它可能有点繁重，所以如果您不想使用函数方程，则可能必须手动证明自己的归纳原理：

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

Definition discr (l : list bar) : Prop :=
    match l with
    | _ :: A :: _ => False
    | _ => True
    end.

Lemma f_ind :
    forall (P : list bar -> nat -> Prop),
        (forall x y, P (x :: A :: y) 1) ->
        (forall l, discr l -> P l 2) ->
        forall l, P l (f l).
Proof.
    intros P h1 h2 l.
    destruct l as [| x [|[] l]].
    3: eapply h1.
    all: eapply h2.
    all: exact I.
Qed.

Goal forall l, f l < 3.
Proof.
    intro l.
    eapply f_ind.
    - intros. repeat constructor.
    - intros. repeat constructor.
Qed.