Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prove associativity of composition of relations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prove associativity of composition of relations


Chronological Thread 
  • From: Cyprien Mangin <cyprien.mangin AT m4x.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Prove associativity of composition of relations
  • Date: Wed, 11 May 2016 19:32:39 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=Neutral smtp.pra=cyprien.mangin AT m4x.org; spf=Pass smtp.mailfrom=SRS0=wd/9=RE=m4x.org=cyprien.mangin AT bounces.m4x.org; spf=Pass smtp.helo=postmaster AT mx1.polytechnique.org
  • Ironport-phdr: 9a23:W76H8hPeQLUyJXguL5Ul6mtUPXoX/o7sNwtQ0KIMzox0KPj5rarrMEGX3/hxlliBBdydsKIVzbOI+Pm4ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTmkbnssMSLPU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y43Q30MkxdOSy3M6h77WN+luTrirOtw3m+fNMv5TLYcXGiyqaBxR0m72288Kzcl/TSP2YRLh6VBrUf5qg==

Hello,

You will need some kind of extensionality to prove exactly your lemma. What you can prove is the following:

∀ (R : U → V → Prop) (Q : V → T → Prop) (P : T → W → Prop) x y, (P ∘ Q ∘ R) x y  ↔ ((P ∘ Q) ∘ R) x y.

--
Cyprien

On Wed, May 11, 2016 at 7: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







Archive powered by MHonArc 2.6.18.

Top of Page