coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "John Wiegley" <johnw AT newartisans.com>
To: scott constable <sdconsta AT syr.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prove associativity of composition of relations
Date: Wed, 11 May 2016 10:48:27 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f170.google.com
Ironport-phdr: 9a23:bYbWMRMc4T6HY+pYiH0l6mtUPXoX/o7sNwtQ0KIMzox0KPT7rarrMEGX3/hxlliBBdydsKIVzbOH+Pm6ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTmkbnjsMSJPU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGBCE4WcAGm4RlAFUCgLB4VmuRZv6tS3hquNVwziAe8D6UOZndy6l6vIhahjojm84NjM29GzGwIQkjqVbpg2JoRFgypTIYZqcMuE4daTYK4BJDVFdV9pcAnQSSri3aJECWq9YZb5V
Organization: New Artisans LLC

>>>>> scott constable
>>>>> <sdconsta AT syr.edu>
>>>>> writes:

> Lemma compose_assoc : R3 @ R2 @ R1 = (R3 @ R2) @ R1.
> Proof. ???
> Admitted.

Require Import FunctionalExtensionality.

Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.

Lemma compose_assoc : R3 @ R2 @ R1 = (R3 @ R2) @ R1.
Proof.
extensionality x.
extensionality y.
apply prop_extensionality; split; intros;
inversion H; subst.
inversion H0; subst.
eapply comp_intro.
exact H2.
eapply comp_intro.
exact H3.
exact H1.
inversion H; subst.
inversion H1; subst.
eapply comp_intro.
eapply comp_intro.
exact H0.
exact H4.
exact H5.
Qed.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

Re: [Coq-Club] Prove associativity of composition of relations, (continued)