The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, January 16, 2015 12:39:43 AM gallais wrote:
> If you are willing to have membership / repeat predicates living
> in Type (it is needed to write the `remove` function) then there
> is a fairly simple constructive solution:
> https://github.com/gallais/potpourri/blob/master/agda/poc/PigeonHole.agda
> 
> Now, it should not be too hard to move from a Prop-based formulation
> to a Type-based one if you can decide equality of elements: you can
> recover a membership predicate in Type by searching the list for an
> element (decidable equality!) with the guarantee to find one (Prop-
> based membership predicate!).

Since the end result is a Prop anyway, it shouldn't really matter whether you 
have decidable equality.  Projecting from a Type to its corresponding Prop 
acts like a monad - for example:

Inductive In {A:Type} (x:A) : list A -> Prop :=
| In_now : forall l, In x (cons x l)
| In_later : forall y l, In x l ->
  In x (cons y l).

Inductive InT {A:Type} (x:A) : list A -> Type :=
| InT_now : forall l, InT x (cons x l)
| InT_later : forall y l, InT x l ->
  InT x (cons y l).

Lemma In_InT_monad : forall {A:Type} (x:A)
  (l:list A) (Q:Prop),
  (InT x l -> Q) -> (In x l -> Q).
Proof.
intros. revert H. induction H0.
+ intro H; apply H. constructor.
+ intros. apply IHIn. intros. apply H.
  constructor. trivial.
Qed.

Inductive HasDup {A:Type} : list A -> Prop :=
| HasDup_now : forall x l, In x l -> HasDup (cons x l)
| HasDup_later : forall x l, HasDup l -> HasDup (cons x l).

Inductive HasDupT {A:Type} : list A -> Type :=
| HasDupT_now : forall x l, InT x l -> HasDupT (cons x l)
| HasDupT_later : forall x l, HasDupT l -> HasDupT (cons x l).

Lemma HasDup_HasDupT_monad : forall {A:Type} (l:list A) (P:Prop),
  (HasDupT l -> P) -> (HasDup l -> P).
Proof.
intros. revert H. induction H0.
+ intros. refine (In_InT_monad _ _ _ _ H). intros. 
  apply H0. constructor 1; trivial.
+ intros. apply IHHasDup. intros. apply H.
  constructor 2; trivial.
Qed.

(Or, you could probably also prove these by proving e.g.
In x l <-> inhabited (InT x l) and then destructing the inhabited.)
-- 
Daniel Schepler