The Coq mailing list

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

Indeed the advice of Gaetan is very good. Another way 
to say it:

When you need to show inversion lemmas for inductively defined 
predicates, consider *inverting the rules at once* and then
instantiate on the particular form you need. Doing so, you end
up using a simple destruct (pattern matching) which succeed
when all parameters are variables. It usually fails when
parameters and compound terms (like x::xs).

I send you a variant of what Gaetan did with dependent
inversion lemmas.

Dominique

----- Mail original -----
> De: "Gaetan Gilbert" 
> <gaetan.gilbert AT ens-lyon.fr>
> À: 
> coq-club AT inria.fr
> Envoyé: Dimanche 5 Mars 2017 11:59:10
> Objet: Re: [Coq-Club] Proving without decidable equality or excluded middle.
> 
> 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
> >
> 
>

Attachment: php_from_agda.v
Description: Binary data