一意性述語の可否判定リスト

Question

リストの一意性とその決定性機能の述語を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. 

が、私はちょうどP xが成り立つxsように、リスト内の一つだけ値xがあるかどう述語Unique xsが保持することを指定しています。今、問題が起こります。私は、次の厄介なエラーメッセージを持っている

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]]. 
    ... 

：私はこのメッセージをGoogleで検索し、別のコンテキスト内のいくつかの同様の問題を見てきました

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

私はそのUnique決定可能性を定義しようとしたとき。少なくとも私には、このような問題はCoqパターンマッチングに関するいくつかの制限に関連しているようです。

さて、問題は解決していることを、私の質問は：

1）私が欲しいのは、決定可能述語に基づいて一意性テストのための決定可能性を定義することです。標準ライブラリでは、存在量と普遍的な量指定子についても同様のテストが行​​われます。両方とも帰納的述語として定義できます。リストに帰納的述語として "一意に存在する"を定義する方法はありますか？

2）このような述語を定義することは、存在する固有の標準論理の意味に一致するように可能ですか？ありがとうございます！ x、P x =存在するx、P x /¥for y、P y - > x = y？

Answer 1

あなたに実行している何があなたがex上のパターンマッチ（両方existsための基本となる誘導できないことですおよびexists!）を使用して、タイプであり、Propではないタイプの値であるsumbool（{_} + {_}表記のタイプ）を生成します。提案された修正についてはthis bug reportを参照してください。この問題を回避するために

、私はあなたではなくプロップよりもタイプで何かを作り出すユニークなのより強力なバージョン（sig）を証明する必要があると思う：

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. 

あなたは、その後タイプで、この定義のための決定可能性を証明することができ、あなたがしたい場合は、あなたの元の文を証明し、そこから：

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

アントンの答えで述べたように、この証明は、またタイプで、すなわちforall (x y:A), {x=y} + {x<>y}をAための決定可能平等が必要になります。

Answer 2

部分的な回答のみを提供してください（コメントには大きすぎます）。

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.