如何用复杂的模式匹配进行推理?

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调用(。 为了说服coq案例可以被分解，你必须使用视图的概念。 它们在示例中的方程式上下文中描述。 我将详细介绍如何使您的示例适应它。

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.