coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: scott constable <sdconsta AT syr.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Prove associativity of composition of relations
- Date: Wed, 11 May 2016 13:36:39 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
- Ironport-phdr: 9a23:ZtwDPRSBIntr0ZpkOPrE/S1wE9psv+yvbD5Q0YIujvd0So/mwa64ZxON2/xhgRfzUJnB7Loc0qyN4/GmADJLuM7f+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVOlsD3WLjKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxwFDBBTZpBr9WIztuyH+u6IpwyWROsvtUbkcQiW4qapnVUm72288Kzcl/TSP2YRLh6VBrUf5qg==
Hi Cyprien,
I realize that I can prove an IFF, but what I really need for my theorems is a Leibniz equality. I tried functional extensionality without any success. I'm not sure what other types of extensionality would be applicable.
~Scott
On Wed, May 11, 2016 at 1:32 PM, Cyprien Mangin <cyprien.mangin AT m4x.org> wrote:
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.--CyprienOn 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.~ScottOn 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
- [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Frédéric Blanqui, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Fabian Kunze, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Cyprien Mangin, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Cyprien Mangin, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Thorsten Altenkirch, 05/12/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Cyprien Mangin, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Fabian Kunze, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, John Wiegley, 05/12/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Abhishek Anand, 05/12/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, scott constable, 05/11/2016
- Re: [Coq-Club] Prove associativity of composition of relations, Frédéric Blanqui, 05/11/2016
Archive powered by MHonArc 2.6.18.