使用来自定理的信息进行模式匹配
Pattern matching using information from theorems
我有以下问题,请看代码。
(* 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
的一个版本,它总是 returns 类型 A
的值。像这样:
Definition f x: A :=
match f_opt x with
| Some y => y
end.
但我收到以下错误:
Non exhaustive pattern-matching: no clause found for pattern None
.
我知道我需要对类型做一些工作,但我不明白我应该做什么。
您需要将存在性证明 always_not_none
放入 Set
或 Type
中才能这样做:
Theorem always_some: forall x, { y: A & f_opt x = Some y}.
...
Qed.
然后您可以执行以下操作(或使用 refine
或 Program
):
Definition f (x: B) : A :=
let s := always_some x in let (x0, _) := s in x0.
在 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
的定义没有任何构造函数,当我们匹配False
类型的项时,没有分支需要处理,整个表达式可以return 我们想要的任何类型——在本例中,A
.
这段代码的奇怪之处在于匹配项上的类型注释,它 return 是一个函数,而不是直接 A
类型的东西。这样做是因为依赖模式匹配在 Coq 中的工作方式:每当我们想要使用我们从匹配的特定分支中获得的信息时(这里,f_opt x
等于 None
在那个分支中),我们必须明确地使匹配 return 成为一个函数——Adam Chlipala 称之为 convoy pattern。这样做是为了让 Coq 知道您打算在哪里使用这些额外信息,并检查它是否正确完成。在这里,我们使用 f_opt x
是 None
来提供 always_not_none x
推导出矛盾所需的假设。
虽然这会解决您的问题,但我通常建议您不要这样做。例如,如果您知道 A
类型包含某些元素 a : A
,那么您可以简单地在该分支上创建 f
return a
。这样做的好处是可以避免在函数中提及证明,这在简化和重写术语时经常会造成阻碍。
使用 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
模块在幕后做了很多工作,在完整的显式定义中,您必须使用 "convoy pattern" 来编写这些工作。但是请注意,有时 Program
往往会在 JMeq
和公理 JMeq_eq
上产生很多依赖关系,当涉及依赖类型时,即使它可能不是必需的。)
我有以下问题,请看代码。
(* 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
的一个版本,它总是 returns 类型 A
的值。像这样:
Definition f x: A :=
match f_opt x with
| Some y => y
end.
但我收到以下错误:
Non exhaustive pattern-matching: no clause found for pattern
None
.
我知道我需要对类型做一些工作,但我不明白我应该做什么。
您需要将存在性证明 always_not_none
放入 Set
或 Type
中才能这样做:
Theorem always_some: forall x, { y: A & f_opt x = Some y}.
...
Qed.
然后您可以执行以下操作(或使用 refine
或 Program
):
Definition f (x: B) : A :=
let s := always_some x in let (x0, _) := s in x0.
在 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
的定义没有任何构造函数,当我们匹配False
类型的项时,没有分支需要处理,整个表达式可以return 我们想要的任何类型——在本例中,A
.
这段代码的奇怪之处在于匹配项上的类型注释,它 return 是一个函数,而不是直接 A
类型的东西。这样做是因为依赖模式匹配在 Coq 中的工作方式:每当我们想要使用我们从匹配的特定分支中获得的信息时(这里,f_opt x
等于 None
在那个分支中),我们必须明确地使匹配 return 成为一个函数——Adam Chlipala 称之为 convoy pattern。这样做是为了让 Coq 知道您打算在哪里使用这些额外信息,并检查它是否正确完成。在这里,我们使用 f_opt x
是 None
来提供 always_not_none x
推导出矛盾所需的假设。
虽然这会解决您的问题,但我通常建议您不要这样做。例如,如果您知道 A
类型包含某些元素 a : A
,那么您可以简单地在该分支上创建 f
return a
。这样做的好处是可以避免在函数中提及证明,这在简化和重写术语时经常会造成阻碍。
使用 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
模块在幕后做了很多工作,在完整的显式定义中,您必须使用 "convoy pattern" 来编写这些工作。但是请注意,有时 Program
往往会在 JMeq
和公理 JMeq_eq
上产生很多依赖关系,当涉及依赖类型时,即使它可能不是必需的。)