列表唯一性谓词可判定性答案

【问题标题】：List uniqueness predicate decidability列表唯一性谓词可判定性
【发布时间】：2017-12-12 20:09:11
【问题描述】：

我想为列表唯一性及其在 Coq 中的可判定性函数定义一个谓词。我的第一次尝试是：

Section UNIQUE.
  Variable A : Type.
  Variable P : A -> Prop.
  Variable PDec : forall (x : A), {P x} + {~ P x}.


  Definition Unique (xs : list A) := exists! x, In x xs /\ P x.

在这里，我刚刚指定了谓词Unique xs 将成立，如果列表x 中只有一个值xs 使得P x 成立。现在，问题来了。当我试图定义它的Unique 可判定性时：

  Definition Unique_dec : forall xs, {Unique xs} + {~ Unique xs}.
    induction xs ; unfold Unique in *.
    +
      right ; intro ; unfold unique in * ; simpl in * ; crush.
    +
      destruct IHxs ; destruct (PDec a).
      destruct e as [y [Hiy HPy]].
  ...

我收到以下令人讨厌的错误消息：

Error: Case analysis on sort Set is not allowed for inductive definition ex.

我用谷歌搜索了这条消息，并在不同的上下文中看到了几个类似的问题。至少在我看来，这样的问题似乎与 Coq 模式匹配的一些限制有关，对吧？

既然问题解决了，我的问题：

1) 我只想为基于可判定谓词的唯一性测试定义可判定性。在标准库中，存在量词和通用量词有类似的测试。两者都可以定义为归纳谓词。有没有办法将“存在唯一”定义为列表上的归纳谓词？

2) 是否可以定义这样的谓词以匹配存在唯一性的标准逻辑含义？像存在！ x, P x = 存在 x, P x /\ forall y, P y -> x = y?

【问题讨论】：

我认为您还需要要求相等的可判定性才能捕获！一点你的谓词。在实践中，我更喜欢避免使用 In 并使用 math-comp 中的 seq 库，其中 Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
请注意，列表上的唯一性谓词有两个合理的定义。除了您提供的那个之外，还有一个更强大的变体，它要求 x 恰好出现在列表 xs 的一个位置。
您可以通过 Arthur 的评论归纳定义更强的版本，例如：Inductive Unique : list A -> Prop := | Unique_base_case : forall x xs, P x -> Forall (fun y => ~ P y) xs -> Unique (x :: xs) | Unique_inductive_case : forall x xs, ~ P x -> Unique xs -> Unique (x :: xs).
对于您提供的较弱版本，可能会将基本情况更改为：forall x xs, P x -> Forall (fun y => P y -> y = x) xs -> Unique (x :: xs)。
我不明白更强的版本捕获了什么。在我的脑海中，我只看到了一个独特的 uniq 定义 [对于可判定的 eqtypes ]

标签： coq

【解决方案1】：

您遇到的问题是，您无法在 ex（exists 和 exists! 的基础归纳）上进行模式匹配，以生成 sumbool 类型的值（@ 987654325@ notation)，它是一个 Type 而不是一个 Prop。“讨厌的错误消息”对于解决这个问题并没有太大帮助；请参阅 this bug report 以获取建议的修复。

为了避免这个问题，我认为你应该证明一个更强大的 Unique 版本，它在 Type (a sig) 而不是 Prop 中产生一些东西：

Definition Unique (xs : list A) := exists! x, In x xs /\ P x.
Definition UniqueT (xs : list A) := {x | unique (fun x => In x xs /\ P x) x}.

Theorem UniqueT_to_Unique : forall xs,
    UniqueT xs -> Unique xs.
Proof.
  unfold UniqueT, Unique; intros.
  destruct X as [x H].
  exists x; eauto.
Qed.

然后，您可以在 Type 中证明此定义的可判定性，并根据需要从那里证明您的原始陈述：

Definition UniqueT_dec : forall xs, UniqueT xs + (UniqueT xs -> False).

正如 Anton 的回答中所提到的，这个证明将需要 A 的可判定相等性，同样在 Type 中，即 forall (x y:A), {x=y} + {x<>y}。

【讨论】：

【解决方案2】：

让我只提供部分答案（评论太大了）。

如果我们采用允许多个副本的唯一性定义（如 Arthur 所提到的），那么 Unique_dec 意味着类型 A 的相等性的可判定性（如 @ejgallego 所提到的）。

假设我们有

Unique_dec
     : forall (A : Type) (P : A -> Prop),
       (forall x : A, {P x} + {~ P x}) ->
       forall xs : list A, {Unique P xs} + {~ Unique P xs}

我们可以展示以下内容：

Lemma dec_eq A (a b : A) : a = b \/ a <> b.
Proof.
  pose proof (Unique_dec (fun (_ : A) => True) (fun _ => left I) [a;b]) as U.
  unfold Unique in U; destruct U as [u | nu].
  - destruct u as (x & [I _] & U).
    destruct I as [<- | [<- | contra]];
      [specialize (U b) | specialize (U a) |]; firstorder.
  - right; intros ->; apply nu; firstorder.
Qed.

【讨论】：