The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Your intuition about = (Coq.Init.Logic.eq) is/was too rosy. 
For 2 closed terms, say a and b, the only time you can prove a=b is when the strong normal forms of a and b are SYNTACTICALLY the same.

When you instantiate your lemma with P Q R := eq nat, the LHS and RHS are closed terms in strong normal form, and they are NOT syntactically the same.
Hence your lemma is not provable.

-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Wed, May 11, 2016 at 1:07 PM, scott constable <sdconsta AT syr.edu> wrote:

>

> >

> Correction: "I think it should be possible to prove associativity of my definition of composition"...
>
> On Wed, May 11, 2016 at 1:06 PM, scott constable <sdconsta AT syr.edu> wrote:

>

> >>

>> Thanks for the quick response Frédéric, but I already have a large project which relies heavily on my definition of composition, and the CoLoR library uses a different definition of composition. Hence I would have to rework a lot of my project to fit the CoLoR definition. I think it should be possible to prove associativity of my definition of relation in Coq, and I would like to know how to do so.
>>
>> ~Scott
>>
>> On Wed, May 11, 2016 at 1:00 PM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

>

> >>>

>>> Hello. You will find useful developments on relations in CoLoR.Util.RelUtil.v (coq-color on opam). See http://color.inria.fr/doc/CoLoR.Util.Relation.RelUtil.html for the definitions and theorems without the proofs. Best regards, Frédéric.
>>>
>>>
>>> Le 11/05/2016 18:51, scott constable a écrit :

>

> >>>>

>>>> Hi All,
>>>>
>>>> I have the following definition of composition:
>>>>
>>>> Inductive Compose : T → V → Prop :=
>>>> | comp_intro : ∀ x y z, R1 x y → R2 y z → Compose x z.
>>>>
>>>> Notation "P ∘ R" := (Compose R P) (at level 55, right associativity).
>>>>
>>>> And I am hopelessly lost as to how to prove this theorem:
>>>>
>>>> Lemma compose_assoc : ∀ (R : U → V → Prop) (Q : V → T → Prop)
>>>>                           (P : T → W → Prop), P ∘ Q ∘ R = (P ∘ Q) ∘ R.
>>>>
>>>> Any help would be extremely appreciated!
>>>>
>>>> Thanks in advance,
>>>>
>>>> ~Scott Constable
>>>
>>>
>>
>