The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Dear Dan,

Thank you very much!

Best,

Qinxiang

On Tue, Sep 17, 2019 at 2:37 AM Dan Frumin <dfrumin AT cs.ru.nl> wrote:

Dear Qinxiang Cao,

I don't know an answer to your first question, but as for the second one, I believe that the default priority for an instance is the number of its
arguments that are not (formally) dependant on the other arguments. So, in your case Foo1Prod has priority 2 (arguments A and B). foo1 on the other
hand has default priority of 1. That explains the Coq behavior in your snippet.

Best,
Dan

On 16-09-19 08:40, Cao Qinxiang wrote:
> Dear Coq clubbers,
>
> Here are two questions about coq type classes.
>
> 1. I find this line of code in standard library (Coq.Classes.RelationClasses):
>    Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
> But what does "class_apply" mean? What is the difference between "class_apply" and "apply"? I cannot find it in Coq's tactic index.
>
> 2. When declaring instances using "Existing Instance", I can provide a priority number. Smaller numbers have high priority. But what is the order
> between instances with a priority number and those without a priority number? The following examples seem to say: there is not such thing called
> default priority number.
>
>     Class Foo1 (A: Type): Type.
>     Class Foo2 (A: Type): Type.
>
>     Class Foo (A: Type): Type := {
>        foo1 : Foo1 A;
>        foo2 : Foo2 A
>     }.
>     Definition FooProd {A B: Type} {FooA: Foo A} {FooB: Foo B}: Foo (A*B).
>        constructor; constructor.
>     Qed.
>
>     Definition Foo1Prod {A B: Type} {FooA: Foo1 A} {FooB: Foo1 B}: Foo1 (A*B).
>        constructor.
>     Qed.
>
>     Set Printing All.
>
>     Module DefaultBeforeOne.
>
>     Local Existing Instance FooProd | 1.
>     Local Existing Instance Foo1Prod | 1.
>     Local Existing Instance foo1 .
>     Local Existing Instance foo2 .
>     Goal forall (A B: Type) (FooA: Foo A) (FooB: Foo B), Foo1 (A * B).
>     Proof.
>        intros.
>        eauto with typeclass_instances.
>     Qed.
>
>     Print Unnamed_thm.
>
>     End DefaultBeforeOne.
>
>     Module DefaultAfterTwo.
>
>     Local Existing Instance FooProd.
>     Local Existing Instance Foo1Prod.
>     Local Existing Instance foo1 | 2.
>     Local Existing Instance foo2 | 2.
>     Goal forall (A B: Type) (FooA: Foo A) (FooB: Foo B), Foo1 (A * B).
>     Proof.
>        intros.
>        eauto with typeclass_instances.
>     Qed.
>     Print Unnamed_thm.
>
>     End DefaultAfterTwo.
>
>     Module DefaultBeforeThree.
>
>     Local Existing Instance FooProd.
>     Local Existing Instance Foo1Prod.
>     Local Existing Instance foo1 | 3.
>     Local Existing Instance foo2 | 3.
>     Goal forall (A B: Type) (FooA: Foo A) (FooB: Foo B), Foo1 (A * B).
>     Proof.
>        intros.
>        eauto with typeclass_instances.
>     Qed.
>     Print Unnamed_thm.
>
>     End DefaultBeforeThree.
>
>
> Thank you very much!
>
> Best regards,
> Qinxiang Cao
> Shanghai Jiao Tong University, John Hopcroft Center
> Room 1110-2, SJTUSE Building
> 800 Dongchuan Road, Shanghai, China, 200240
>