在匹配块的分支内,如何使用匹配表达式等于分支的数据构造函数表达式的断言？

Question

我正在尝试开发一种基于防止错误输入的编程风格.例如,代替自然数上的前任函数的以下合理定义:

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确实引入了这样的假设吗？如果是这样,它的名字是什么？

Answer 1

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引入了一个可以在此类型注释中使用的变量名称,并将在每个分支中用左侧替换.这里,
  • 在第一个分支中,右侧有类型n = S p -> nat;
  • 在第二个分支中,右侧有类型n = O -> nat.因此,q Heq有类型False和可以匹配.

有关扩展模式匹配的章节中的参考手册中的更多信息.