The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

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
>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>