The Coq mailing list

["Chung Kil Hur" <ckh25 AT cam.ac.uk>]

Hi Adam,

Oh, I was stupid. I only tried eta reduction rather than eta expansion.
Thanks for the proof.

----- Original Message ----- 
From: "Adam Chlipala" 
<adam AT chlipala.net>
To: "Chung Kil Hur" 
<ckh25 AT cam.ac.uk>
Cc: 
<coq-club AT inria.fr>
Sent: Thursday, February 04, 2010 1:27 PM
Subject: Re: [Coq-Club] An interesting example using Heq


> Chung Kil Hur wrote:
>> I received an example from Benedikt Ahrens and he asked whether I can
>> simplify his proof using Heq.
>> That example was interesting to me because I didn't have this kind of
>> example in mind when I developed Heq, but Heq helped.
>> I wonder whether there is a direct simple proof, or Heq is
>> particularly useful in this case.
> 
> Here's a pretty simple direct proof.
> 
> 
> Hint Resolve @functional_extensionality_dep.
> Hint Extern 1 (_ = _) => progress f_equal.
> 
> Goal forall C1 C2 mo mm,
> mkfunctor_data C1 C2 (fun a => mo a) (fun a b f => mm a b f) =
> mkfunctor_data C1 C2 mo mm.
> intros until mo; rewrite (eta_expansion mo); auto.
> Qed.
>