The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks!

However, I have a goal where I can do

      Create HintDb foobar discriminated.

      Hint Rewrite @FIdentityOf : foobar.

      Fail rewrite_db foobar. (* The command has indeed failed with message:

=> Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *)

      setoid_rewrite @FIdentityOf. (* succeeds *)

The definition of [FIdentityOf] is 

FIdentityOf = 

fun (objC : Type) (C : ComputationalCategory objC)

  (H : IsSpecializedCategory C) (objD : Type)

  (D : ComputationalCategory objD) (H0 : IsSpecializedCategory D)

  (F : ComputationalFunctor C D)

  (IsSpecializedFunctor0 : IsSpecializedFunctor F) =>

let (_, FIdentityOf) := IsSpecializedFunctor0 in FIdentityOf

     : forall (objC : Type) (C : ComputationalCategory objC)

         (H : IsSpecializedCategory C) (objD : Type)

         (D : ComputationalCategory objD) (H0 : IsSpecializedCategory D)

         (F : ComputationalFunctor C D),

       IsSpecializedFunctor F ->

       forall x : C, MorphismOf F (Identity x) = Identity (F x)

Arguments objC, C, H, objD, D, H0 are implicit

Argument IsSpecializedFunctor is implicit and maximally inserted

Argument scopes are [type_scope category_scope _ type_scope category_scope _

  functor_scope _ object_scope]

The goal is

1 subgoals, subgoal 1 (ID 2696)

  

  objC : Type

  C : SpecializedCategory objC

  objD : Type

  D : SpecializedCategory objD

  objE : Type

  E : SpecializedCategory objE

  G : SpecializedFunctor D E

  F : SpecializedFunctor C D

  x : C

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

   MorphismOf G (Identity (F x)) = Identity (G (F x))

I can try to construct a small example reproducing the error, if you don't have any idea what's going on here.

Thanks,

Jason

On Fri, Mar 22, 2013 at 6:43 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi Jason,

Le 22 mars 2013 à 05:32, Jason Gross <jasongross9 AT gmail.com> a écrit :

>
> Hint Rewrite @FIdentityOf using eauto with typeclass_instances : functor.

>   Fail rewrite @FIdentityOf by auto with typeclass_instances. (* should not fail *)
>   erewrite @FIdentityOf by auto with typeclass_instances.

The problem is that, even before launching type class resolution, [rewrite] expects
the metavariables for H and H0 to be instantiated, that's why it fails. If instead it
used existential variables (like [setoid_rewrite FIdentityOf] does) it wouldn't fail.
There is an (undocumented) tactic [rewrite_db hintdb] which does setoid rewrite
using the rewrite hint database hintdb, but it doesn't take care of the side
condition tactic (yet). You could still use it like this:

Require Import Setoid.
Ltac rewrite_cat := rewrite_db functor; try typeclasses eauto.

And use rewrite_cat instead of your autorewrite.
-- Matthieu