The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 19 févr. 2013, at 06:44, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> Hi,
> Is there a way to make [Existing Class] behave like [Class]?  For example, 
> in the following code, if I have [Existing Class IsCat], then [rewrite 
> Associativity] generates an extra goal [IsCat C]; but if I define [IsCat] 
> to be a [Class] to start off with, then this goal does not show up.
> 
> Set Implicit Arguments.
> 
> Record Cat :=
>   { 
>     Object :> Type;
>     Morphism : Object -> Object -> Type;
>     Compose : forall {s d d'}, Morphism d d' -> Morphism s d -> Morphism s 
> d'
>   }.
> 
> Record IsCat (C : Cat) :=
>   { 
>     Associativity : forall o1 o2 o3 o4
>                            (m1 : Morphism C o1 o2)
>                            (m2 : Morphism C o2 o3)
>                            (m3 : Morphism C o3 o4),
>                       Compose C (Compose C m3 m2) m1 = Compose C m3 
> (Compose C m2 m1)
>   }.
> 
> Existing Class IsCat.
> 
> Section foo.
>   Variable C : Cat.
>   Context `(IsCat C).
>   Lemma foo o1 o2 o3 o4
>         (m1 : Morphism C o1 o2)
>         (m2 : Morphism C o2 o3)
>         (m3 : Morphism C o3 o4)
>   : Compose C (Compose C m3 m2) m1 = Compose C (Compose C m3 m2) m1.
>     rewrite Associativity.
> 

Hi Jason,

  This is because the IsCat record is not declared implicit for Associativity.
Using this setting of implicts works:
Arguments Associativity {C} {IsCat} {o1 o2 o3 o4} m1 m2 m3 : rename.

-- Matthieu