coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] pigeon hole principal
- Date: Fri, 16 Jan 2015 09:09:02 -0800
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
- [Coq-Club] pigeon hole principal, Jiten Pathy, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Frédéric Blanqui, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Ben, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Jiten Pathy, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, gallais, 01/16/2015
- Re: [Coq-Club] pigeon hole principal, Daniel Schepler, 01/16/2015
Archive powered by MHonArc 2.6.18.