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

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.

或者，您可以使用策略构建术语“手工”(见8.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.查看结果术语。

Answer 2

您可以在匹配上使用return注释：

Lemma notNotEqual : forall x:nat, (x <> x) -> False.
auto.
Qed.

Definition predecessor (n:nat) : n<>0 -> nat :=
  match n return (n <> 0 -> nat) with
    | 0 =>
      fun H : 0 <> 0 => 
        match notNotEqual 0 H with end
    | S m => fun _ => m
  end.

这在Adam的书““具有依赖类型的认证编程”，从归纳类型一章开始”中有介绍。它还包括在Coq手册第17章，“扩展模式匹配”，克里斯蒂娜科恩斯和雨果赫贝林。

您还可以使用refine将函数样式与策略样式混合使用。

Definition predecessor_alt (n:nat) : n<>0 -> nat.
refine 
  (match n return (n <> 0 -> nat) with
     | 0 => _
     | S m => fun _ => m
   end).
intros; assert False as nope.
auto.
inversion nope.
Defined.