The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

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