The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Lars,

To prove the PHP *without using decidability of equality*, I suggest
you to prove the following generalization which does not get you
stuck in the inductive proof (see below).

That proof DOES NOT REQUIRE you to manipulate proof terms 
as your code seems to imply (IN_IND) ... I am going to look into
how to prove IN_IND but you need to generalize IN_fwd to give
you identities between proof terms as well I think ... 
Something like

Lemma IN_fwd (x y : X) (xs : list X) (H : IN x (y::xs)) :
       (exists (E : x = y), eq_rect _ (fun u => IN u (y::xs)) H _ E = @here y 
xs)
    \/ (exists H' : IN x xs, H = @there _ _ _ H').

Which is not going to be as easy as inversion ...

(* ------ *)

Anyway, here is the principle of the alternative proof I suggest

You show that for two lists (l m : list X), if 

a/ incl l m: l is included in m (forall x, In x l -> In x m)
b/ length m <= length l (notice this is <= and not <)

then 

either 

1/ lhd l : l is a duplicated element (exists a u v w, l = u++a::v++a::w) 

or

2/ l ~p m : l is a permutation of m (Permutation l m)

Theorem PHP_gen X (l m : list X) : incl l m -> length m <= length l -> lhd l 
\/ l ~p m.

I suggest defining "has a duplicated element" inductively as

Inductive lhd : list X -> Prop :=
  | in_lhd0 : forall x l, In x l -> lhd (x::l)
  | in_lhd1 : forall x l, lhd l -> lhd (x::l)

orelse you simply show the induction principle for the
definition you give of the lhd predicate.

Then the PHP follows trivially

Theorem PHP X (l m : list X) : incl l m -> length m < length l -> lhd l.

because l ~p m implies length l = length m which contradicts length m < 
length l

Good luck,

Dominique

----- Mail original -----
> De: "Lars Rasmusson" 
> <lars.rasmusson AT ri.se>
> À: 
> coq-club AT inria.fr
> Envoyé: Samedi 4 Mars 2017 23:08:00
> Objet: [Coq-Club] Proving without decidable equality or excluded middle.
> 
> The Agda proof [1] by G. Allais of the Pigeonhole does not use decidability
> or excluded
> middle. It defines a membership predicate and an induction lemma.
> 
> data _∈_ {X : Set} (x : X) : (xs : List X) → Set where
>   here! : {xs : List X} → x ∈ x ∷ xs
>   there : {xs : List X} {y : X} (pr : x ∈ xs) → x ∈ y ∷ xs
> 
> x∈y∷ys : {X : Set} {x y : X} {ys : List X} {P : (x : X) (pr : x ∈ y ∷ ys) →
> Set}
>          (phere! : P y here!) (pthere : (x : X) (pr : x ∈ ys) → P x (there
>          pr))
>          (pr : x ∈ y ∷ ys) → P x pr
> x∈y∷ys phere! pthere here!      = phere!
> x∈y∷ys phere! pthere (there pr) = pthere _ pr
> 
> 
> On the last two lines, the proof of the induction lemma considers the two
> cases
> where pr was constructed using either the 'here!' constructor  or the 
> 'there'
> constructor.
> How would one do that in Coq?  Inversion doesn't help here [2]...
> 
> 
>   Variable (X : Type).
>   Implicit Type (x : X).
> 
>   Inductive IN x : list X -> Prop :=
>   | here  xs   : IN x (x :: xs)
>   | there xs y : IN x xs -> IN x (y :: xs).
> 
>   Arguments here {_ _}.
>   Arguments there {_ _ _}.
> 
>    Lemma IN_fwd: forall {x y xs}, IN x (y::xs) -> (x=y \/ IN x xs).
>     now inversion 1; tauto.
>   Qed.
>  
>   Definition IN_IND:
>     forall {x y ys}
>       {P : forall x, IN x (y::ys) -> Prop}
>       (Phere : P y here)
>       (Pthere : forall x (pr: IN x ys),  P x (there pr))
>       (pr : IN x (y::ys)), P x pr.
>   Proof.
>     intros.
>     destruct (IN_fwd pr).
>     subst.
>     
> (* in the x=y case  we have
> 
>   ...
>   Phere : P y here
>   pr : IN y (y :: ys)
>   ============================
>   P y pr
> 
> *)
>   
>     inversion pr.
> 
> (* still no information that pr was created by 'here!' or 'there' *)
> 
>  How would one write the Agda proof in Coq? How can one compare proof
> objects (functions) based on which constructor they were built from  
> (without
> EM,functional extensionality, JM_eq or other additional axioms)?
> 
> 
> Thanks!
> /Lars
> 
> 
> 
> [1] 
> https://github.com/gallais/potpourri/blob/master/agda/poc/PigeonHole.agda
> [2] https://x80.org/collacoq/agikoxayom.coq
> 
>