coq - sumbool 和 sum 的区别

Question

对于任何A B : Prop,sum A B和sumbool A B是同构的, 通过以下,

Definition from_sumbool (A B : Prop) (x : sumbool A B) : sum A B :=
  match x with
  | left l => inl l
  | right r => inr r
  end.

Definition to_sumbool (A B : Prop) (x : sum A B) : sumbool A B :=
  match x with
  | inl l => left l
  | inr r => right r
  end.

那么为什么我们有sumbool呢？似乎只是对 的限制sum，其中A B是Prop而不是，Type结果是Set而不是Type。

“bool”听起来像 sumbools 有 2 个元素。然而，这只是sumbool True True. sumbool False False并且sumbool False True分别有 0 和 1 个元素。

同样，对于A B : Prop的 OCaml 提取sum A B比 的更详细sumbool A B。我没有看到明确的原因：我们假设提取知道AandB的类型Prop，因此它可以使用与本例相同的简化sumbool。

通常，Coq 似乎定义了 3 次相同的函数：forType和. 它对所有归纳类型 ( 和 ) 的归纳方案执行此操作。对于不相交的联合，我们有和。这使得要记住的功能增加了 3 倍。SetProp_rect_rec_indsumsumboolor

标签： coq

Answer 1

在某种程度上，我认为这只是sumbool为了服务于与 不同的目的sum，并且使用唯一的名称和符号来突出和记录这一事实。

Asum只是一个通用的求和类型，但 asumbool旨在用作类似布尔值的结果，其中“真”和“假”值带有证据。因此，当您看到类似以下的库函数时：

Definition le_lt_dec n m : {n <= m} + {m < n}.

很明显，这种定义的目的是构建一个类似布尔值的决策值，我们可以在计算中使用它，就像 一样leb : nat -> nat -> bool，但在每个条件分支中也有可用的证据。

作为一个更实际的问题，该类型sumbool : Prop -> Prop -> Set允许在编译/提取时擦除证据，这对于更通用的类型Prop不会发生。sum

作为一个公认的愚蠢示例，如果我们有一个head需要非零列表长度证据的函数：

Lemma nlt_0_r : forall n, ~(n < 0). Proof. intros n H. inversion H. Qed.
Definition head {A : Set} (l : list A) (E : 0 < length l) : A :=
  match l return (0 < length l -> A) with
  | x :: _ => fun _ => x
  | nil => fun E1 => except (nlt_0_r _ E1)
  end E.

我们想写一个head_with_default定义，使用 a 可能很自然sumbool：

Definition head_with_default {A : Set} (x : A) (l : list A) :=
  match le_lt_dec (length l) 0 : {length l <= 0} + {0 < length l} with
  | left _ => x
  | right E => head l E
  end.

我们也可以用普通sum类型来写：

Definition le_lt_dec' (n m : nat) : (n <= m) + (m < n). Admitted.
Definition head_with_default' {A : Set} (x : A) (l : list A) :=
  match le_lt_dec' (length l) 0 : (length l <= 0) + (0 < length l) with
  | inl _ => x
  | inr E => head l E
  end.

如果我们提取这两个定义，我们可以看到证据已从sumbool版本中删除，但仍保留在sum版本中：

Extraction head_with_default.
(* let head_with_default x l = *)
(*   match le_lt_dec (length l) O with *)
(*   | Left -> x *)
(*   | Right -> head l *)

Extraction head_with_default'.
(* let head_with_default' x l = *)
(*   match le_lt_dec' (length l) O with *)
(*   | Inl _ -> x *)
(*   | Inr _ -> head l *).

更新： 跟进评论，请注意，这种提取差异并不是真正的“优化”。Coq 并没有看到——在这种特殊情况下—— Props 中的 ssumbool可以被优化掉，但sum由于编译器不够智能，所以无法执行相同的优化。就是整个 Coq 逻辑都建立在这样的思想之上：在PropUniverse 中，证明值可以并且将会被擦除，但在SetUniverse 中，“证明”值很重要，并且会在运行时反映出来。

进一步更新：现在，您可能会问（正如您在进一步的评论中所做的那样），为什么这不是提取级别的优化？为什么不在 Coq 中使用单个sum类型，然后更改提取算法，以便它擦除在编译时已知为Props 的所有类型。好吧，让我们试试吧。假设，使用上面的定义，我们写：

Inductive error := empty | missing.
Definition my_list := (inr 1 :: inr 2 :: inl missing :: inr 4 :: nil).
Definition sum_head := head_with_default' (inl empty) my_list.

提取看起来像这样：

type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b

(** val my_list : (error, nat) sum list **)
let my_list = ...

(** val sum_head : (error, nat) sum **)
let sum_head =
  head_with_default' (Inl Empty) my_list

现在，天真的提取head_with_default'如上。如果我们想写出一个优化的版本，我们不能重用 type sum，因为它的构造函数有错误的数量。我们需要sum使用已擦除的 props 生成优化类型：

type sumP =
| InlP
| InrP

let head_with_default' x l =
  match le_lt_dec' (length l) O with
  | InlP -> x
  | InrP -> head l

这工作正常。当然，如果有人试图创建 a nat + (x == 0)，也称为 a sumor：

Definition nat_or_zero (x : nat) : nat + (x = 0) :=
  match x with
  | O => inr eq_refl
  | _ => inl x
  end.

那么我们将需要该sum类型的第三个版本：

type ('a) sumSP =
| InlSP of 'a
| InrSP

let nat_or_zero x = match x with
| O -> InrSP
| S _ -> InlSP x

sumPS除非我们有充分的理由拒绝，否则我们将需要第四个版本(x==0) + nat。

任何可能对sums 进行操作的函数，例如：

Fixpoint list_lefts {A B : Type } (l : list (A + B)) : list A :=
  match l with
  | nil => nil
  | inr x :: l' => list_lefts l'
  | inl x :: l' => x :: list_lefts l'
  end.

还需要在多个版本中提取。至少对于A : Set, 两者B : Set和都B : Prop可能有用：

(** val list_lefts : ('a1, 'a2) sum list -> 'a1 list **)

let rec list_lefts = function
| Nil -> Nil
| Cons (s, l') ->
  (match s with
   | Inl x -> Cons (x, (list_lefts l'))
   | Inr _ -> list_lefts l')

(** val list_leftsSP : ('a1) sumSP list -> 'a1 list **)

let rec list_leftsSP = function
| Nil -> Nil
| Cons (s, l') ->
  (match s with
   | InlSP x -> Cons (x, (list_lefts l'))
   | InrSP -> list_lefts l')

您可以争辩说其他两个没有用，但是如果有人不同意您的观点并试图申请list_lefts'一个list ((x=0)+(x=1))怎么办？显然，优化版本的第一次破解并不能消除__：

(** val list_leftsP : sum' list -> __ list **)

let rec list_leftsP = function
| Nil -> Nil
| Cons (s, l') ->
  (match s with
   | InlP -> Cons (__, (list_lefts l'))
   | InrP -> list_lefts l')

但这仅仅是因为我们没有提取优化版本list：

type listP =
| NilP
| ConsP of listP

让我们写：

(** val list_leftsP : sumP list -> listP **)

let rec list_leftsP = function
| Nil -> NilP
| Cons (s, l') ->
  (match s with
   | InlP -> ConsP (list_leftsP l')
   | InrP -> list_leftsP l')

这表明list_leftsP（以及我遗漏的第四个变体）可能很有x=1用，因为它执行计算给定的证明数量的非平凡计算l : list ((x=0) + (x=1))。

现在我们准备定义：

Definition ugh {A B C D : Type} : A + B -> C + D ->
  A*C + A*D + B*C + B*D := ...

并使用它的 16 个版本之一，如ughPPPS，以及四个版本的子集prod来表示其结果。但是，不清楚 ML 返回类型是否ughPPPS应该是幼稚的：

(((prodP ('d prodPS) sum) prodP sum) ('d prodPS) sum)

无法删除无用的 type 条款prodP，或者是否应该将其优化为：

(((('d prodPS) sumPS) sumSP) ('d prodPS) sum)

事实上，Coq 可以走这条路，归纳地追踪类型对Propsvs的依赖，Sets并根据需要为程序中使用的所有变体生成多个提取。相反，它需要程序员在 Coq 级别决定哪些证明是重要的Set（Prop结果是提取将密切反映 Coq 类型，而不是成为fooPPSPPSP优化变体的沙拉。（如果您尝试在任何非 Coq 代码中使用提取，这是一个很大的优势。）