5

我正在尝试开发一种基于尽快防止错误输入的编程风格。例如，对于自然数的先行函数，而不是以下似是而非的定义：

Definition pred1 n :=
  match n with
    | O   => None
    | S n => Some n
  end.

我想写如下：

Theorem nope n (p : n = O) (q : n <> O) : False.
  contradict q.
  exact p.
Qed.

Definition pred2 n (q : n <> O) :=
  match n with
    | S n => n
    | O   =>
      let p := _ in
      match nope n p q with end
  end.

但我不知道用什么代替_。我的直觉告诉我，分支中一定有一些assumption : n = O可用的。| O =>Coq 是否确实引入了这样的假设？如果有，它的名字是什么？

4

1 回答 1

5

Coq 不会自动引入这样的假设，但您可以使用完整的match构造形式明确地引入它：

Definition pred2 n (q : n <> O) :=
  match n as n' return n = n' -> nat with
    | S p => fun _ => p
    | O   => fun Heq => match q Heq with end
  end (eq_refl n).

说明：

  • return引入带有整个match ... end表达式类型的类型注释；
  • as引入了一个可在此类型注释中使用的变量名，并将在每个分支中用左侧替换。这里，
    • 在第一个分支中，右侧有 type n = S p -> nat；
    • 在第二个分支中，右侧有 type n = O -> nat。因此，q Heq有类型False并且可以匹配。

参考手册中的更多信息，在扩展模式匹配一​​章中。

于 2012-12-29T21:24:20.257 回答