The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello,

I am having trouble getting the desired unfolding behavior of 
operational type classes with recursive instances using the simpl 
tactic. Let me explain this by the following example.

Consider the operational type class for a functor:

  Class FMap (M : Type -> Type) :=
    fmap: forall {A B}, (A -> B) -> (M A -> M B).

An instance for lists can be defined as follows:

  Instance list_fmap: FMap list := fun A B f =>
    fix go (l : list A) : list B :=
    match l with
    | nil => nil
    | x :: l => f x :: go l
    end.

When using this type class for proofs on lists, it does not work well 
because simpl does not unfold occurrences of fmap at all. Luckily, this 
can be fixed using the Arguments command to force to unfold simpl when 
the last argument is a constructor.

  Arguments fmap {_ _ _ _} _ !_ /.

But still, simpl's behavior is not quite what I would like to see:

  Eval simpl in (fun l => fmap S (10 :: l)).

  (* fun l : list nat => 11 :: list_fmap nat nat S l *)

What we see here is that the recursive call is not folded back to the 
projection of the operational type class. Instead, the instance 
declaration itself appears. The following is what I want to see:

   fun l : list nat => 11 :: fmap S l

A dirty fix is to change the definition of list_fmap such that the 
recursive call uses the constructor of the class.

  Instance list_fmap_alt: FMap list :=
    fix go A B f (l : list A) : list B :=
    match l with
    | nil => nil
    | x :: l => f x :: @fmap _ go _ _ f l
    end.

This fixes the problem, and the result of simpl uses the projection fmap 
for recursive calls.

Unfortunately, now the mapped function f is an argument of the fixpoint, 
and therefore mutual recursion is no longer possible. For example:

  Inductive tree A :=
    | leaf : A -> tree A
    | branch : list (tree A) -> tree A.
  Arguments leaf {_} _.
  Arguments branch {_} _.

  Instance tree_fmap: FMap tree :=
    fix go A B f (t : tree A) : tree B :=
    match t with
    | leaf x => leaf (f x)
    | branch ts => branch (fmap (@fmap _ go _ _ f) ts)
    end.

will fail when the instance list_fmap_alt is declared, whereas it used 
to work when list_fmap was declared.

I have tried the following solutions:

* Use an autorewrite database instead of simpl. This has two problems: 
autorewrite does not rewrite under binders, and autorewrite is much 
slower than simpl.

* Put the mapped function as an argument of the functor type class

    Class FMap (M : Type -> Type) {A B} (f : A -> B) :=
      fmap: (M A -> M B).

  This way, simpl works as expected, and mutual recursion is allowed as 
well. However, this is incredibly ugly, as this is not the definition of 
a functor. Everywhere where a functor is needed, I have to write the 
type class constraint as {map : forall A B (f : A -> B), FMap M f}.


Does anyone have an idea how to work around this idea? Or would it be 
possible to change simpl in such a way that it not only refolds 
fixpoints (what it is doing right now), but also refolds operational 
type classes?

Best,

Robbert