在 coq 中推导模式匹配的事实

Question

考虑以下程序

Definition useGt0 (n: nat) (witness: n > 0) : nat :=
  10.


Definition createGt0(n: nat) : nat :=
  match n with
  | O => 42
  | S(n') => useGt0 n  (#???)
  end.

显然，n > 0 是有人居住的，因为 n = S n'。但是，我如何获得 n = S n' 的证明？从n = S n'我们可以得出n > 0.

总的来说，我想了解：如何从模式匹配中提取信息？

Answer 1

定义 createGt0 函数的标准方法是使用护航模式（您可以使用 [coq] [convoy-pattern] 在 Whosebug 上搜索查询找到多种解释）。标准 link 是 A. Chlipala 的 CPDT 书。

这是一个解决方案：

Definition createGt0 (n : nat) : nat :=
  match n as x return (n = x -> nat) with
  | O => fun _ => 42
  | S n' => fun E => useGt0 n (eq_ind_r (fun n => n > 0) (gt_Sn_O n') E)
  end eq_refl.

另一种选择是使用 Program 机制，它允许您以非依赖类型的风格编程，将证明义务推迟到以后：

Require Import Program.

Program Definition createGt0 (n : nat) : nat :=
  match n with
  | O => 42
  | S n' => useGt0 n _
  end.
Next Obligation. apply gt_Sn_O. Qed.

最后，您可以使用策略来构建您的函数：

Definition createGt0 (n : nat) : nat.
Proof.
  destruct n eqn:E.
  - exact 42.
  - refine (useGt0 n _).
    rewrite E.
    apply gt_Sn_O.
Defined.

如果你的函数以 Qed 结束，Coq 会认为它是不透明的，不会减少。尝试使用 Qed 和 Defined 结束函数并执行以下命令：

Compute createGt0 0.

在 coq 中推导模式匹配的事实

deriving facts on pattern matching in coq

coq

coq-tactic