`split` fails with `Error: Refiner was given an argument "@SpecializedFunctor (* Set NaturalTransformation.283 Top.112 Top.113 *) (CardinalityRepresentative O) (NatCategory (* NaturalTransformation.283 *) O) objC C" of type "Type (* max(Set, Nat

[JasonGross]

This is in the following environment. I'll try to get a cleaner one soon, but I figured that the error message and environment might be enough to point you to the error

  objC : Type (* Top.112 *)
  C : SpecializedCategory (* Top.112 Top.113 *) objC
  ============================
   and
     (@eq
        (@SpecializedFunctor (* Set Functor.290 Set Functor.290 *)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O)))
        (@ComposeFunctors (* Set Functor.290 Set Functor.290 Set
           Functor.290 *) (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O)) ExponentialLaw0Functor
           (* Set Functor.290 Functor.290 NaturalTransformation.283 *)
           ExponentialLaw0Functor_Inverse (* Functor.290 Set Functor.290
           NaturalTransformation.283 Set Set Top.244 *))
        (@IdentityFunctor (* Set Functor.290 *)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))))
     (@eq
        (@SpecializedFunctor (* Set Functor.290 Set Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C))
        (@ComposeFunctors (* Set Functor.290 Set Functor.290 Set
           Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           ExponentialLaw0Functor_Inverse (* Functor.290 Set Functor.290
           NaturalTransformation.283 Set Set Top.259 *)
           ExponentialLaw0Functor (* Set Functor.290 Functor.290
           NaturalTransformation.283 *))
        (@IdentityFunctor (* Set Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)

[JasonGross]

There's something odd going on here. When I have something as a goal, it fails:

    Set Printing All.
    Goal (@eq
     (@SpecializedFunctor (CardinalityRepresentative (S O))
        (NatCategory (S O)) (CardinalityRepresentative (S O))
        (NatCategory (S O)))
     (@ComposeFunctors (CardinalityRepresentative (S O))
        (NatCategory (S O))
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)
        (@FunctorCategory (CardinalityRepresentative O)
           (NatCategory O) objC C) (CardinalityRepresentative (S O))
        (NatCategory (S O)) ExponentialLaw0Functor
        ExponentialLaw0Functor_Inverse)
     (@IdentityFunctor (CardinalityRepresentative (S O)) (NatCategory (S O)))).
    generalize ExponentialLaw0Functor. (* Toplevel input, characters 0-33:
Error: Illegal application (Type Error):
The term "SpecializedFunctor" of type
 "forall (objC : Type) (_ : SpecializedCategory objC)
    (objD : Set) (_ : SpecializedCategory objD), Type"
cannot be applied to the terms
 "@SpecializedFunctor (CardinalityRepresentative O) (NatCategory O) objC C"
   : "Type"
 "@FunctorCategory (CardinalityRepresentative O) (NatCategory O) objC C"
   : "SpecializedCategory
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)"
 "CardinalityRepresentative (S O)" : "Set"
 "NatCategory (S O)"
   : "SpecializedCategory (CardinalityRepresentative (S O))"
The 1st term has type "Type" which should be coercible to
"Type". *)

But if instead I do

    Set Printing All.
    Goal True.
    assert (@eq
     (@SpecializedFunctor (CardinalityRepresentative (S O))
        (NatCategory (S O)) (CardinalityRepresentative (S O))
        (NatCategory (S O)))
     (@ComposeFunctors (CardinalityRepresentative (S O))
        (NatCategory (S O))
        (@SpecializedFunctor (CardinalityRepresentative O)
           (NatCategory O) objC C)
        (@FunctorCategory (CardinalityRepresentative O)
           (NatCategory O) objC C) (CardinalityRepresentative (S O))
        (NatCategory (S O)) ExponentialLaw0Functor
        ExponentialLaw0Functor_Inverse)
     (@IdentityFunctor (CardinalityRepresentative (S O)) (NatCategory (S O)))).
    generalize ExponentialLaw0Functor.

it goes through fine. (This is in the file ExponentialLaws.v at https://JasonGross@bitbucket.org/JasonGross/catdb.) I'm still trying to get it small enough to post the source here.

[JasonGross]

Ok, here's a self-contained version. I'm really surprised that intro can fail with Illegal application (Type Error) I'll try to trim this down sometime soon, but, if I don't get to it, I hope it's enough to work off of:

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.

Set Implicit Arguments.

Generalizable All Variables.

Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
  Object :> _ := obj;
  Morphism' : obj -> obj -> Type;

  Identity' : forall o, Morphism' o o;
  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d';

  Associativity' : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' (Compose' m3 m2) m1 = Compose' m3 (Compose' m2 m1);
  (* ask for [eq_sym (Associativity' ...)], so that C^{op}^{op} is convertible with C *)
  Associativity'_sym : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
    Compose' m3 (Compose' m2 m1) = Compose' (Compose' m3 m2) m1;
  LeftIdentity' : forall a b (f : Morphism' a b), Compose' (Identity' b) f = f;
  RightIdentity' : forall a b (f : Morphism' a b), Compose' f (Identity' a) = f
}.

Bind Scope category_scope with SpecializedCategory.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism'.

Arguments Object {obj%type} C%category : rename.
Arguments Identity' {obj%type} C%category o%object : rename.
Arguments Compose' {obj%type} C%category s%object d%object d'%object m1%morphism m2%morphism : rename.

(* create a hint db for all category theory things *)
Create HintDb category discriminated.
(* create a hint db for morphisms in categories *)
Create HintDb morphism discriminated.

Section SpecializedCategoryInterface.
  Polymorphic Definition Build_SpecializedCategory (obj : Type)
    (Morphism' : obj -> obj -> Type)
    (Identity' : forall o : obj, Morphism' o o)
    (Compose' : forall s d d' : obj, Morphism' d d' -> Morphism' s d -> Morphism' s d')
    (Associativity' : forall (o1 o2 o3 o4 : obj) (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),
      Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
    (LeftIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a b b (Identity' b) f = f)
    (RightIdentity' : forall (a b : obj) (f : Morphism' a b), Compose' a a b f (Identity' a) = f) :
    @SpecializedCategory obj
    := @Build_SpecializedCategory' obj
    Morphism'
    Identity' Compose'
    Associativity'
    (fun _ _ _ _ _ _ _ => eq_sym (Associativity' _ _ _ _ _ _ _))
    LeftIdentity'
    RightIdentity'.

  Context `(C : @SpecializedCategory obj).

  Polymorphic Definition Morphism : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').

  Bind Scope morphism_scope with Morphism.

  Polymorphic Definition Identity : forall o : C, Morphism o o := Eval cbv beta delta [Identity'] in C.(Identity').
  Polymorphic Definition Compose : forall {s d d' : C} (m : Morphism d d') (m0 : Morphism s d), Morphism s d' := Eval cbv beta delta [Compose'] in C.(Compose').
  Polymorphic Definition Associativity : forall (o1 o2 o3 o4 : C) (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),
    Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1)
    := C.(Associativity').
  Polymorphic Definition LeftIdentity : forall (a b : C) (f : Morphism a b),
    Compose (Identity b) f = f
    := C.(LeftIdentity').
  Polymorphic Definition RightIdentity : forall (a b : C) (f : Morphism a b),
    Compose f (Identity a) = f
    := C.(RightIdentity').
End SpecializedCategoryInterface.

Bind Scope morphism_scope with Morphism.

Arguments Object {obj} C : rename, simpl never.
Arguments Morphism {obj} C s d : rename, simpl nomatch.
Arguments Compose {obj} [C s d d'] m m0 : simpl nomatch.
Arguments Identity {obj} [C] o : simpl nomatch.

Global Opaque Associativity LeftIdentity RightIdentity.

Hint Resolve @LeftIdentity @RightIdentity @Associativity : category.
Hint Rewrite @LeftIdentity @RightIdentity : category.

Section SpecializedFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Record SpecializedFunctor := {
    ObjectOf' : objC -> objD;
    MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
    FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
      MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
    FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
  }.
End SpecializedFunctor.

Bind Scope functor_scope with SpecializedFunctor.

Create HintDb functor discriminated.

Section FunctorInterface.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Variable F : SpecializedFunctor C D.

  Polymorphic Definition ObjectOf : C -> D := Eval cbv beta delta [ObjectOf'] in F.(ObjectOf'). (* [forall], so we can name it in [Arguments] *)
  Polymorphic Definition MorphismOf : forall {s d : C} (m : C.(Morphism) s d), D.(Morphism) (ObjectOf s) (ObjectOf d)
    := Eval cbv beta delta [MorphismOf'] in F.(MorphismOf').
  Polymorphic Definition FCompositionOf : forall (s d d' : C) (m1 : C.(Morphism) s d) (m2 : C.(Morphism) d d'),
    MorphismOf (Compose m2 m1) = Compose (MorphismOf m2) (MorphismOf m1)
    := F.(FCompositionOf').
  Polymorphic Definition FIdentityOf : forall (o : C), MorphismOf (Identity o) = Identity (ObjectOf o)
    := F.(FIdentityOf').
End FunctorInterface.

Global Coercion ObjectOf : SpecializedFunctor >-> Funclass.

Hint Resolve @FCompositionOf @FIdentityOf @FCompositionOf' @FIdentityOf' : functor.
Hint Rewrite @FIdentityOf @FIdentityOf' : functor.

Section FunctorComposition.
  Context `(B : @SpecializedCategory objB).
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).

  Hint Rewrite @FCompositionOf : functor.

  Polymorphic Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E.
    refine {| ObjectOf' := (fun c => G (F c));
      MorphismOf' := (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m))
    |};
    abstract (
        intros; autorewrite with functor; reflexivity
      ).
  Defined.
End FunctorComposition.

Definition Cat0 : SpecializedCategory Empty_set.
  refine {|
      Morphism' := fun s d : Empty_set => s = d;
      Identity' := fun o : Empty_set => eq_refl;
      Compose' := fun (s d d' : Empty_set) (H : d = d') (H0 : s = d) =>
                    eq_trans H0 H |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.

Lemma foo objC (C : @SpecializedCategory objC) (C0 : SpecializedCategory (SpecializedFunctor Cat0 C)) (x : SpecializedFunctor Cat0 Cat0) : forall (y : SpecializedFunctor C0 Cat0) z, (ComposeFunctors y z = x).
  intro.

It has something to do with the intros; autorewrite with functor; reflexivity line; if I change that to admit, it all goes through. (Same thing if I do the rewriting manually.)

[JasonGross]

Here's a slightly more trimmed version:

Set Implicit Arguments.

Polymorphic Record Category (obj : Type) :=
  {
    Morphism : obj -> obj -> Type;
    Identity : forall o, Morphism o o
  }.

Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) :=
  {
    ObjectOf :> objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
    FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o)
  }.

Create HintDb functor discriminated.

Hint Rewrite @FIdentityOf : functor.

Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
refine {| ObjectOf := (fun c => G (F c));
          MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m))
       |};
  intros; autorewrite with functor; reflexivity.
Defined.

Definition Cat0 : Category Empty_set.
  refine {|
      Morphism := fun s d : Empty_set => s = d;
      Identity := fun o : Empty_set => eq_refl
    |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.

Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x).
  intro.

[mattam82]

Indeed, autorewrite was doing something wrong: if it could rewrite twice with the same polymorphic lemma it would just use a single instance of the universes for both, hence equating all levels of the categories/functors involved in your definition of composition. I'll commit the fix ASAP. It's pretty bad that Lemma doesn't tell you it can't typecheck the term and you have to do an intro to see that, I'll look into it.

[JasonGross]

Does one of Hint Extern 0 => rewrite .... or auto with ... do something similar? I'm getting behavior that looks like this using auto with .... If need-be, I can trim and post the relevant code.

[mattam82]

It could be. I think a Hint with a rewrite in it is fine. OTOH you better make your auto hints Polymorphic if you want them to be :)

[JasonGross]

What about Polymorphic Hint Resolve? The following code fails on econstrutor/refine:

Set Implicit Arguments.

Polymorphic Record Category (obj : Type) :=
  {
    Morphism : obj -> obj -> Type;

    Identity : forall o, Morphism o o;
    Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2;

    LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
  }.

Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
  {
    ObjectOf : objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
  }.

Create HintDb morphism discriminated.

Polymorphic Hint Resolve @LeftIdentity : morphism.

Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
  refine {|
      Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
      Identity := (fun o => (Identity _ (fst o), Identity _ (snd o)));
      Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1)))
    |};
  intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *)
Defined.

Polymorphic Definition Cat0 : Category Empty_set.
  refine {|
      Morphism := fun s d : Empty_set => s = d;
      Identity := fun o : Empty_set => eq_refl;
      Compose := fun s d d2 m0 m1 => eq_trans m1 m0
    |};
  admit.
Defined.

Set Printing All.
Set Printing Universes.
Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71:
Error: Refiner was given an argument
 "prod (* Top.2289 Top.2289 *) objC Empty_set" of type
"Type (* Top.2289 *)" instead of "Set". *)
econstructor. (* Toplevel input, characters 0-12:
Error: No applicable tactic.
*)

This is with commit ecb030d0dba7e784d66427d9bff14713c8ca4cbd.

[mattam82]

Ha, I overlooked to update (e)auto's code to handle polymorphic hints, only typeclasses were benefiting from the change...

[mattam82]

I forgot to add, polymorphic hints can only be made out of global references. Here typing "Resolve LeftIdentity" without the @ will parse LeftIdentity as a global reference and not typecheck it with implicit arguments and all. The latest HoTT/coq will raise an error if one tries to make a polymorphic hint out of something else than a global.

[JasonGross]

This forbids polymorphic hints of theorems with implicit maximally inserted terms. This is annoying, for example, when I want to define theorems in a Section where I used Context to give me variables. Removing the @s gives me, e.g., Error: Cannot infer the implicit parameter obj of LeftIdentity. if I make obj an implicit maximally inserted term.

[JasonGross]

Would it be a problem to make Hints ignore rules about maximally inserted parameters?

[mattam82]

No it should not, when interpreted as a global reference it ignores about implicits. So it's probably a bug or you're using a different version (?).

-- Matthieu

Le 23 janv. 2013 à 12:06, Jason Gross notifications@github.com a écrit :

This forbids polymorphic hints of theorems with implicit maximally inserted terms. This is annoying, for example, when I want to define theorems in a Section where I used Context to give me variables. Removing the @s gives me, e.g., Error: Cannot infer the implicit parameter obj of LeftIdentity. if I make obj an implicit maximally inserted term.

— Reply to this email directly or view it on GitHub.

[JasonGross]

Ah, it only errors on Hint Rewrite (see below). Can polymorphic rewrite hints use non-global references? (If so, it seems odd that Hint Rewrite and Hint Resolve behave differently in this fashion.)

Polymorphic Lemma foo {obj : Type} : 1 = 1.
trivial.
Qed.

Polymorphic Hint Resolve foo. (* success *)
Polymorphic Hint Rewrite @foo. (* Success *)
Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)

[mattam82]

Ha, I thought I did adapt it in the trunk already... apparently not.

[JasonGross]

Is this a straightforward thing to fix/adapt?

[mattam82]

On my TODO list for today.

[JasonGross]

If you want to point me at the right bit of code (or even just the right file) to modify, I can try to figure out what has to be done, and write a patch for this. (I've never hacked on Coq before, though, so you might get around to doing this yourself before I figure out how to.)

[mattam82]

This no longer applies.

[JasonGross]

This is broken again in polyproj (intro gives Illegal Application). Also Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *) is broken.