coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] fun <-> forall

From: Burak Ekici <ekcburak AT hotmail.com>
To: Clément Pit-Claudel <cpitclaudel AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] fun <-> forall
Date: Thu, 26 Oct 2017 15:11:10 +0000
Accept-language: tr-TR, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ekcburak AT hotmail.com; spf=Pass smtp.mailfrom=ekcburak AT hotmail.com; spf=Pass smtp.helo=postmaster AT EUR03-VE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:7B3+iB33wR4vQ/uxsmDT+DRfVm0co7zxezQtwd8ZsegSLvad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3WbmHC57CYTFxPjLkI1Y72tQs+Bx/iwgsu2epjeZRkAvDuhJJh2JQi6oAGZ4sIOgJdpLq8sxhbNinRNcuVSg2hvIATX11z34d7195p++QxRvegg/ohOS++yK68/VPlTCCksG2Ez/szi8xfZG1ih/HwZB08LiBNLSyXG7Rr7FsP8sSDwq/B02wGaOtHzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfce+Ur5qg==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi Clément,

Thanks a lot! That's exactly what I was looking for...

Best,

―

Burak.

On 26-10-2017 18:08, Clément Pit-Claudel wrote:
> On 2017-10-26 10:25, Burak Ekici wrote:
>> However, could not make it work whatever I did...
> Does the following work for you?
>
> pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl
> H1c) as H';
> cbv beta in H'.
>
> Here's a complete example:
>
> Axiom catC: Type.
> Axiom obj: Type -> Type.
> Axiom arrow: forall (catC: Type), obj catC -> obj catC -> Type.
> Axiom fmap : forall {C: Type} (a b: obj C), arrow C b a -> Type.
> Axiom foo : forall {C a b}, arrow C b a -> arrow C b a.
>
> Goal ((fun (a b : obj catC) (f : arrow catC b a) => fmap a b (foo f)) =
> (fun (a b : obj catC) (f : arrow catC b a) => fmap a b f) -> True).
> Proof.
> intros.
> pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl
> H) as H';
> cbv beta in H'.
>

[Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
  - Re: [Coq-Club] fun <-> forall, Robbert Krebbers, 10/26/2017
    - Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
      - Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        Message not available
        Re: [Coq-Club] fun <-> forall, Samuel Gruetter, 10/28/2017
        [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
        Re: [Coq-Club] Macro for Ltac, Pierre Courtieu, 10/30/2017
        Re: [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/30/2017
        
        Re: [Coq-Club] fun <-> forall, Jason Gross, 10/31/2017
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/31/2017
        
        Re: [Coq-Club] fun <-> forall, Cyril Cohen, 10/31/2017
    - Re: [Coq-Club] fun <-> forall, Anton Trunov, 10/26/2017