The Coq mailing list

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

Hi,

 

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 is the example.

 

=============================================

Require Import FunctionalExtensionality.
Set Implicit Arguments.

 

Record Cat_data : Type := mkcat_data
{ obj :> Type;
  mor : forall a b : obj, Type;
  id : forall a:obj, mor a a;
  comp : forall a b c: obj, mor a b -> mor b c -> mor a c
}.

 

Record Functor_data (C1 C2 : Cat_data) : Type := mkfunctor_data
{ map_o :>  C1 ->  C2;
  map_m : forall (a b : obj  C1), mor C1 a b -> mor C2 (map_o a) (map_o b)
}.

 

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.

=============================================

 

We want to prove the above goal using FunctionalExtensionality.

But, simple rewriting does not work because the fourth argument of mkfunctor_data depends on its third argument.

I proved it in the following way using Heq.

 

=============================================

Proof.

Require Import Heq.

intros.
replace (fun a b f => mm a b f) with mm
  by (repeat (apply @functional_extensionality_dep; intro); auto).
set (mo_eta := fun a => mo a) in *.
HreflI mm at 2. revert mm.
change mo_eta with (fun a => mo a). clear mo_eta.
hrewrite <- (eta_expansion mo).
intros. Hclear. reflexivity.
Qed.
=============================================

 

Best,

Chung-Kil Hur