Отчасти, я думаю, что просто sumbool предназначен для использования в целях, отличных от sum, и уникальное имя и обозначение используются для выделения и документирования этого факта.
A sum - это просто общий тип суммы, но sumbool предназначен для использования в качестве логического результата, в котором значения «true» и «false» содержат доказательства. Итак, когда вы видите библиотечную функцию вроде:
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, может быть естественно использовать 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 видел, что - в данном конкретном случае - Prop в sumbool можно было бы оптимизировать, но затем не удалось выполнить ту же оптимизацию в sum, потому что компилятор не был достаточно умен. Дело в том, что вся логика Coq основана на идее, что в Prop значения доказательства вселенной могут и будут стерты, но в Set значения "доказательства" вселенной важны и будут отражены во время выполнения.
Дальнейшее обновление: Теперь вы можете задать вопрос (как вы это сделали в дальнейших комментариях), почему не это оптимизация на уровне извлечения? Почему бы не использовать один тип sum в Coq, а затем изменить алгоритм извлечения так, чтобы он удалял все типы, которые на момент компиляции известны как Prop с. Ну, давай попробуем. Предположим, используя определения выше, мы пишем:
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' было таким же, как указано выше. Если мы хотим выписать оптимизированную версию, мы не можем повторно использовать тип sum, поскольку его конструкторы имеют неправильную арность. Нам нужно сгенерировать оптимизированный тип sum со стертыми реквизитами:
type sumP =
| InlP
| InrP
let head_with_default' x l =
match le_lt_dec' (length l) O with
| InlP -> x
| InrP -> head l
Это работает хорошо. Конечно, если кто-то попытается создать nat + (x == 0), также известный как 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.
Любая функция, которая потенциально может работать на sum с, например:
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)
, который не удаляет бесполезные термины типа prodP, или если вместо этого его следует оптимизировать до:
(((('d prodPS) sumPS) sumSP) ('d prodPS) sum)
Действительно, Coq мог пойти по этому пути, индуктивно отслеживая зависимость типов от Props по сравнению с Sets и генерируя множественные извлечения по мере необходимости для всех вариантов, используемых в программе. Вместо этого он требует, чтобы программист на уровне Coq решал, какие доказательства важны (Set) или не важны (Prop), и - слишком часто - требует множества вариантов типов, конструкторов и функций для работы ( некоторые из) комбинации. Результатом является то, что извлечение будет близко отражать типы Coq, вместо того, чтобы быть fooPPSPPSP салатом оптимизированных вариантов. (Большое преимущество, если вы пытаетесь использовать извлечение в любом не-Coq-коде.)