coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Class_apply and instances level

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Class_apply and instances level
Date: Mon, 16 Sep 2019 14:40:28 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f170.google.com
Ironport-phdr: 9a23:87XH8hFd6ctJX85FAt53Bp1GYnF86YWxBRYc798ds5kLTJ78o8SwAkXT6L1XgUPTWs2DsrQY0rGQ6vqrADVZqdbZ6TZeKcYKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZsJ6or1xfFvHREd/lLyW91OFmfmwrw6tqq8JNs7ihcpegt+9JcXan/Yq81UaFWADM6Pm4v+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAOUBM+hWrIfzukUAogelCAa2GO/i0CVFimPq0aA41ekqDAHI3BYnH9ILqHnZss/6NKAPWu6uzanIyzrCb/JM1jf754jDbxcsru2WUrJ3aMrRyE8vFgzEjlqKr4zlMCiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhIrRho8N1FzI6SF0zJw2KNC4UkJ3fN+pHZlKuy2HNYZ6XsUvSHxytikg0L0Jo5u7cTAKyJs5wx7fbOSKc42S7RLiUOadODB4hHN4dL6miRa+7EqtxvHmWsm711ZKqSVFkt3SuXwXyxPT7c2HRuN8/kenxzmPyxje5v9YLU0wj6bWKJ4szqQtmpcSs0nPBDL6lUfqgKOOc0Ur4Omo6+DpYrX8oZ+cMpd5hR3kPaQpg8y/AOI4MwcPX2eB/+S826bu/UL8QLpQj/02lrPVv4zdJcQevqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsGAWzi9/mDsV834URETaEC6iAMaXCsFaO6cogJuCNYMkevzOreKtt3OLnkXJswQxVRqKux5ZCMCnlTMQjGF2QZD/XuvlEEWoOuVBgHunjiVnHVj8KInjrAPp66TY8B4arS4zEQ9L12e3T7GKABpRTI1t+JBWJGHbseZ+DXq5VOi2XK85l1DcDUOr4EtNz5VSVrAb/joFfAK/M4CRB7MDs0dF046vYkhRgrTE=

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

[Coq-Club] Class_apply and instances level, Cao Qinxiang, 09/16/2019
- Re: [Coq-Club] Class_apply and instances level, Dan Frumin, 09/16/2019
  - Re: [Coq-Club] Class_apply and instances level, Cao Qinxiang, 09/17/2019