The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Just a remark: propositional extensionality is a truncated (to –1) version of univalence (from Homotopy Type Theory).

T.

From: <coq-club-request AT inria.fr> on behalf of scott constable <sdconsta AT syr.edu>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 11 May 2016 at 19:05
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Prove associativity of composition of relations

Ah, I think that propositional extensionality is the missing piece that I was looking for. Here is the complete solution:

Require Import FunctionalExtensionality.

Set Implicit Arguments.

Section Rels.

  Variables T U V : Type.
  Variable R1 : T -> U -> Prop.
  Variable R2 : U -> V -> Prop.

  Inductive Compose : T -> V -> Prop :=
  | comp_intro : forall x y z, R1 x y -> R2 y z -> Compose x z.

End Rels.

Notation "R2 @ R1" := (Compose R1 R2) (at level 55, right associativity).

Axiom prop_ext : forall (P Q : Prop), (P <-> Q) -> P = Q.

Section RelLemmas.

  Variables T U V W : Type.
  Variable R1 : T -> U -> Prop.
  Variable R2 : U -> V -> Prop.
  Variable R3 : V -> W -> Prop.

  Lemma compose_assoc : R3 @ R2 @ R1 = (R3 @ R2) @ R1.
  Proof.
    extensionality x; extensionality y.
    apply prop_ext; split; intro H;
      repeat match goal with
      | [ H : (_ @ _) _ _ |- _ ] => inversion_clear H; subst
      end; eauto using Compose.
  Qed.

End RelLemmas.

Thanks so much everyone!

~Scott Constable


On Wed, May 11, 2016 at 1:47 PM, Cyprien Mangin <cyprien.mangin AT m4x.org> wrote:
>
> You need a form of predicate extensionality:
>
> forall (T U : Type) (P Q : T -> U -> Prop), (forall x y, P x y <-> Q x y) -> P = Q
>
> As remarked in https://coq.inria.fr/cocorico/CoqAndAxioms, this is entailed by propositional extensionality + functional extensionality.
>
> On Wed, May 11, 2016 at 7:36 PM, scott constable <sdconsta AT syr.edu> wrote:
>>
>> 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.
>>>
>>> --
>>> 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
>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.