2

我有以下问题，请看代码。

  (* Suppose we have type A *)
  Variable A: Type.

  (* Also we have a function that returns the type (option A) *)
  Definition f_opt x: option A := ...

  (* Then, I can prove that this function always returns something: *)
  Theorem always_some: forall x, exists y, f_opt x = Some y.
  Admitted.

  (* Or, equivalently: *)
  Theorem always_not_none: forall x, f_opt x <> None.
  Admitted.

现在我想获得一个f_opt总是返回 type 值的版本A。像这样的东西：

  Definition f x: A :=
    match f_opt x with
      | Some y => y
    end.

但我收到以下错误：

非详尽的模式匹配：没有找到 pattern 的子句None。

我知道我需要对类型做一些工作，但我不明白我到底应该做什么。

4

3 回答 3

6

在 Coq 的基础理论中，每个模式匹配都必须是详尽的——也就是说，它必须明确地考虑所讨论的归纳类型的所有构造函数。这就是您收到您看到的错误消息的原因。

我们如何绕过这个限制？有几个解决方案。首先，让我们看看如何让 Coq 相信None分支永远不会发生。为此，我们将使用您的always_not_none定理：

Definition f x : A :=
  match f_opt x as res return res <> None -> A with
  | Some y => fun _ => y
  | None => fun H => match H eq_refl with end
  end (always_not_none x).

这段代码乍一看可能看起来很奇怪，但它几乎可以执行您想要的模式匹配。为了向 Coq 解释这种None情况永远不会出现，它结合了在该分支上得出矛盾always_not_none的事实。f_opt x = None这是该H eq_refl分支上的术语。然后，match这个矛盾足以让 Coq 相信这个分支是虚假的。更正式一点，因为False矛盾的命题是在没有任何构造函数的情况下定义的，当我们在 type 的术语上匹配时False，没有要处理的分支，整个表达式可以返回我们想要的任何类型——在这种情况下, A.

这段代码的奇怪之处在于匹配上的类型注释，它返回一个函数而不是A直接返回某个类型。这样做是因为依赖模式匹配在 Coq 中的工作方式：每当我们想要利用从匹配的特定分支中获得的信息（这里，f_opt x等于None在那个分支中），我们必须显式地使match 返回一个函数——Adam Chlipala 称之为护航模式。这样做是为了让 Coq 知道您计划在哪里使用这些额外信息并检查它是否正确完成。在这里，我们使用它f_opt x来提供推导矛盾None所需的假设。always_not_none x

虽然这会解决您的问题，但我通常建议您不要这样做。例如，如果你知道你的A类型被某个元素占据a : A，那么你可以简单地在那个分支上f返回。a这样做的好处是避免在您的函数中提及证明，这在简化和重写术语时通常会妨碍您。

于 2017-06-07T13:28:09.470 回答
5

使用 Coq 的Program模块，您可以编写详尽的模式匹配，但注释某些分支应该无法到达，然后提供证明是这种情况：

Require Import Program.
Program Definition f x : A :=
match f_opt x with
| Some a => a
| None => !
end.
Next Obligation.
destruct (always_some x). congruence.
Qed.

（该Program模块在幕后做了很多工作，在完整的显式定义中，您必须使用“护航模式”编写。但是请注意，有时Program会产生大量的依赖关系，并且在依赖时会产生JMeq公理JMeq_eq涉及类型，即使它可能不是必需的。）

于 2017-06-08T18:27:07.673 回答
1

您需要将您的存在证明always_not_none放入Set或Type这样做：

Theorem always_some: forall x, { y: A &  f_opt x = Some y}.
...
Qed.

然后您可以执行以下操作（或使用refineor Program）：

Definition f (x: B) : A :=
   let s := always_some x in let (x0, _) := s in x0.
于 2017-06-07T13:26:42.400 回答