The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/29/2012 11:10 AM, Robbert Krebbers wrote:
> 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.

I also tried using an autorewrite database to refold type class 
instances. This did not work well either.


Require Import List.

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

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.

Definition list_fmap_fold A B f :
  @list_fmap A B f = @fmap list (@list_fmap) A B f := eq_refl.
Hint Rewrite list_fmap_fold : fold_classes.

Lemma list_fmap_compose {A B C}
    (f : A -> B) (g : B -> C) (l : list A) :
  fmap (fun x => g (f x)) l = fmap g (fmap f l).
Proof.
  induction l; [easy |].
  simpl.

(* The goal is:
   g (f a) :: list_fmap A C (fun x : A => g (f x)) l =
   g (f a) :: list_fmap B C g (list_fmap A B f l) *)

  autorewrite with fold_classes.

(* The goal is:
  g (f a) :: fmap (fun x : A => g (f x)) l =
  g (f a) :: list_fmap B C g (list_fmap A B f l)
So, only the first occurrence has been rewritten.
*)

  rewrite list_fmap_fold.
(*
  Error: Tactic generated a subgoal identical to the original goal.

  Apparently, rewrite tries to rewrite the first occurrence of 
list_fmap again, but fails. Note that the first occurrence of list_fmap 
is only partial applied, so list_fmap_fold should not even match. *)