A suitably polymorphic definition of commutation in Coq

user_2415103 0
Viewed 71

Right now I have a definition of commute in Coq as:

Definition circ {X Y Z:Type} (f : Y -> Z) (g : X -> Y) : X -> Z := fun z => f (g z).
Infix "@@" := circ (at level 60, right associativity).
Definition funcEq {X Y:Type} (f g : X -> Y) := forall x:X, f x = g x.
Infix "==" := funcEq (at level 60, right associativity).

Definition commute {X:Type} (f : X -> X) (g : X -> X) : Prop := (f @@ g) == (g @@ f).

and can thus state and prove a theorem such as forall (X : Type) (f : X -> X), commute (fmap f) reverse for functions fmap f and reverse on lists. But I want a more generalized definition of commutation, to account for arbitrary functions f—one capable of expressing the truth that forall (X Y : Type) (xs : [X]) (f : X -> Y), reverse (fmap f xs) = fmap f (reverse xs). Is there a reasonably elegant way of doing this?

coq polymorphism
1 Answers

As mentioned in the title of your question, the example you want to capture relies on the fact that reverse is a polymorphic function so that it can be applied to lists containing values of any type.

As a first step towards your goal, you can require that g has the same property leading to the following definition

Definition natural {X Y : Type} (f : X -> Y) (g : forall {Z : Type}, Z -> Z)
 : Prop := (f @@ g) == (g @@ f).

If you want to handle more general cases such as reverse that maps polymorphically lists, you should look into the notion of naturality between functors.

Definition circ {X Y Z:Type} (f : Y -> Z) (g : X -> Y) : X -> Z := fun z => f (g z).
Infix "@@" := circ (at level 55, right associativity).
Definition funcEq {X Y:Type} (f g : X -> Y) := forall x:X, f x = g x.
Infix "==" := funcEq (at level 60, right associativity).

Section Naturality.
  Context (F G : Type -> Type)
          (fmapF : forall {A B : Type}, (A -> B) -> F A -> F B)
          (fmapG : forall {A B : Type}, (A -> B) -> G A -> G B).

  Arguments fmapF {_ _} _ _.
  Arguments fmapG {_ _} _ _.

  Context {X Y : Type} (f : X -> Y) .

  Definition naturality (g : forall {Z : Type}, F Z -> G Z) : Prop :=
    g @@ fmapF f == fmapG f @@ g.
End Naturality.
user_78074380
Related