coq - 如何用复杂的模式匹配进行推理？

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 induction是一种方式。
• 最近，Equations还允许您定义模式匹配，并自动派生归纳原理(您可以使用 funelim 调用)。 为了说服 coq 案例可以因式分解，您必须使用 View 的概念。 它们在方程 in the examples 的上下文中进行描述。 。 我将详细说明如何使您的示例适应它。

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.