The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

I expected something like

>Definition IN_IND : same as your type.

>intros;dependent inversion pr.

to do it but apparently it can't.

I put one way to do it in the attached file. The intuition is that if we 
want to prove something from the structure of (pr : IN foo bar) it's 
easier if bar is a variable, so make an auxiliary lemma where it is a 
variable and which proves the same thing on the value we're interested in.

Gaëtan Gilbert

On 04/03/2017 23:08, Lars Rasmusson wrote:
> 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

Require Import List. (* for x :: xs notation *)

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 {_ _ _}.

Definition in_full_destruct:
  forall {x xs}
         {P : forall x, IN x xs -> Prop}
         (Phere : match xs return (forall x, IN x xs -> Prop) -> Prop with
                  | x::xs => fun P => P x here
                  | nil => fun _ => False end P)
         (Pthere : match xs return (forall x, IN x xs -> Prop) -> Prop with
                   | x::xs => fun P => forall y (pr : IN y xs), P y (there pr)
                   | nil => fun _ => False end P)
         (pr : IN x xs), P x pr.
Proof.
  intros.
  destruct pr;auto.
Qed.


Definition in_cons_destruct:
  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 x y ys P Phere Pthere.
  apply in_full_destruct;auto.
Qed.