List uniqueness predicate decidability

1
votes

I'd like to define a predicate for list uniqueness and its decidability function in Coq. My first try was:

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.

Here I just have specified that predicate Unique xs will hold if there's just one value x in list xs such that P x holds. Now, comes the problem. When I've tried to define its Unique decidability: 

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

I've got the following nasty error message:

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

I've googled this message and seen several similar problems in different contexts. At least to me, it seems that such problem is related to some restrictions on Coq pattern matching, right?

Now that the problem is settled, my questions:

1) All I want is to define a decidability for a uniqueness test based on a decidable predicate. In the standard library, there are similar tests for existencial and universal quantifiers. Both can be defined as inductive predicates. Is there a way to define "exists unique" as an inductive predicate on lists?

2) It is possible to define such predicate in order to it match the standard logic meaning of exists unique? Like exists! x, P x = exists x, P x /\ forall y, P y -> x = y?

2
coq
I think you will also need to require decidablity of equality in order to capture the ! bit of your predicate. In practice, I prefer to avoid In and use the seq library from math-comp, where Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true. – ejgallego
Note that there are two sensible definitions of a uniqueness predicate on lists. Besides the one you gave, there is a stronger variant that requires that x occur in exactly one position of the list xs. – Arthur Azevedo De Amorim
You could define the stronger version from Arthur's comment inductively by something like: 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). – Daniel Schepler
And for the weaker version you gave, maybe change the base case to something like: forall x xs, P x -> Forall (fun y => P y -> y = x) xs -> Unique (x :: xs). – Daniel Schepler
I don't understand what does the stronger version capture. In my head, I only see a unique uniq definition [for decidable eqtypes that is] – ejgallego

2 Answers

3
votes

What you're running into is that you can't pattern match on ex (the underlying inductive for both exists and exists!) in order to produce a value of type sumbool (the type for the {_} + {_} notation), which is a Type and not a Prop. The "nasty error message" isn't terribly helpful in figuring this out; see this bug report for a proposed fix.

To avoid this issue, I think you should prove a stronger version of Unique that produces something in Type (a sig) rather than 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.

You can then prove decidability for this definition in Type, and from there prove your original statement if you want:

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

As mentioned in Anton's answer, this proof will require decidable equality for A, also in Type, namely forall (x y:A), {x=y} + {x<>y}.

1
votes

Let me provide only a partial answer (it's too large for a comment).

If we go with this definition of uniqueness which admits multiple copies (as mentioned by Arthur), then Unique_dec implies decidability of equality for type A (as mentioned by @ejgallego).

Assuming we have 

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}

We can show the following:

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.