coq - 使用假设删除匹配语句中的案例

Question

我想在函数中使用假设来排除match中的一些情况。声明。我想知道这是如何在 Coq 中完成的。

一个非常简单的例子是一个使用 match 的函数在nat上。我想使用一个假设 n <> 0这样我就不必为 0 提供匹配模式，像这样:

Fixpoint minus_1 (n:nat) (H:n<>0): nat :=
  match n with
    | S n' => n'
  end.

上面的例子给出 Error: Non exhaustive pattern-matching: no clause found for pattern 0 .

如何使用H不必提供 0 的模式？

Answer 1

您可以依靠程序库来填补一些空白，例如:

Require Import Arith Program.

Program Fixpoint minus_1 (n: nat) (h: n <> 0) : nat :=
  match n with
    | S p => p
    | _ => _
  end.

或者您可以使用策略“手动”构建术语(在 v8.4 中):

Fixpoint minus_1 (n: nat) (h: n <> 0) {struct n} : nat.
destruct n as [ | p ].
- case h; reflexivity.
- exact p.
Defined.

这是一个适用于旧版本 Coq 的版本:

Definition minus_1 (n: nat) (h: n <> 0) : nat.
revert h.
elim n.
intros heq; case heq; reflexivity.
intros p _ _; exact p.
Defined.

在所有情况下，您都可以使用Print minus_1.来查看结果项。