The Coq mailing list

[Lars Rasmusson <lars.rasmusson AT ri.se>]

Many thanks to both of you!  It is really helpful!

Cheers,
/Lars


> On 5 Mar 2017, at 14:56 , Dominique Larchey-Wendling 
> <dominique.larchey-wendling AT loria.fr>
>  wrote:
> 
> 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
>>> 
>> 
>> 
> <php_from_agda.v>