我已经从实数公理证明了许多定理，现在我想将自然定律定义为实数的子集，并重用所有已证明的定理。怎么做到呢？这是将使用适当的coq设计实践进行编译的人工MRE：
01 (* CReal Definitions *)
02 Parameter CReal: Set.
03 Parameter creal_add : CReal -> CReal -> CReal.
04 Axiom creal_comm: forall x y:CReal, creal_add x y = creal_add y x.
05
06 (* CNat Definitions *)
07 Parameter CNat: Set.
08 Theorem cnat_comm: forall x y:CNat, creal_add x y = creal_add y x.
09 Proof. exact creal_comm. Qed. (* Should be OK after subclassing *)
现在，它抱怨O是CReal而不是CNat，因此，如果x被多态解释为CReal，能够再次与其他CReals进行比较，然后以漂亮而又不复杂的方式将CReal定理和公理应用到它们上，那就太好了。
编辑：
为了更清楚我想要的，这是在正确的子类化之后不应编译的代码：
11 (* CNat Positive *)
12 Parameter O : CReal.
13 Parameter cnat_succ : CNat -> CNat.
14 Axiom cnat_positive: forall (x : CNat), ~cnat_succ x=O.
15
16 (* CReal Wrong Theorem *)
17 Theorem creal_positive: forall x:CReal, ~cnat_succ x=O. (*Crash*)
18 Proof. exact cnat_positive. Qed. (*Also Crash*)
之所以第17行和第18行崩溃的原因是，17在CReal上使用cnat_succ，但是cnat_succ仅为子类CNat定义，而在18中使用了CNat公理，超类CReal应该看不到它。因此，超类公理和定理应该对子类可见并且适用于子类，但反之则不然。
您必须证明您的CNat是同构的，带有CReal的一个子集，并且CNat操作已关闭。
这里有个例子，您可以根据自己的喜好进行扩展。我使用用于实数的lra策略证明了一个简单的引理。
我使用强制，因此不必在所有位置手动插入注入函数f和g。它们在那里，但是用隐形墨水。如果要查看它们，请执行Set Printing Coercions.。
Require Import Reals.
Open Scope R.
Parameter (N:Type)(f:N->R) (g:R->N).
Parameter iso1: forall x, f (g x) = x.
Parameter iso2: forall x, g (f x) = x.
Coercion f : N>->R.
Coercion g : R>->N.
Parameter (n0 n1 : N) (nplus nmult : N->N->N) .
Parameter nzero : n0 = 0.
Parameter none : n1 = 1.
Parameter nplus_ok : forall a b:N, nplus a b = a+b.
Parameter nmult_ok : forall a b:N, nmult a b = a*b.
Set Printing Coercions.
Print nplus_ok.
(* nplus_ok : forall a b : N, nplus a b = g (f a + f b) *)
Unset Printing Coercions.
(* useful tactic to rewrite N to R *)
Ltac NtoR :=
rewrite ?nplus_ok, ?nmult_ok, ?nzero, ?none, ?iso1;
try apply f_equal.
Require Import Psatz.
Goal forall (a b c:N),
(nplus a (nplus b c)) + nmult 1 (a+n1+c) = nplus (2*nplus c a) (nplus (n0+1) b).
intros.
NtoR.
lra.
Qed.
最后我找到了使用Typeclasses的解决方案：
01 (* Import Setoid for smart rewriting *)
02 Require Import Setoid.
03
04
05 (* -------------------------------------------------- *)
06 (* CNat Class *)
07
08
09 (* CNat Definition *)
10 Class CNat A := {
11 O: A;
12 succ: A->A;
13 add: A->A->A;
14 add_comm: forall x y:A, add x y = add y x
15 }.
16
17 (* O Commutativity Lemma *)
18 Lemma O_SO `{CNat}: add O (succ O) = add (succ O) O.
19 Proof.
20 apply add_comm. (* Class axiom *)
21 Qed.
22
23
24 (* -------------------------------------------------- *)
25 (* CInt Class *)
26
27
28 (* CInt Definition *)
29 Class CInt A `{CNat A} := {
30 inv: A->A;
31 add_inv: forall x:A, add x (inv x) = O
32 }.
33
34 (* Some notation for convenience *)
35 Notation "´ x" := (succ x) (at level 25, right associativity).
36 Infix "±" := add (at level 50, left associativity).
37 Notation "¯ x" := (inv x) (at level 35, right associativity).
38
39 (* O Additive Inverse Lemma *)
40 Lemma invO_O `{CInt}: (´O±O) ± ¯(O ±´O) = (´O±´´O) ± ¯(´´O ±´O).
41 Proof.
42 rewrite O_SO. (* Superclass Lemma *)
43 setoid_rewrite add_comm at 5. (* Superclass Axiom *)
44 setoid_rewrite add_inv. (* Class Axiom *)
45 reflexivity.
46 Qed.
可以看出，超类的公理和定理（Lemmas是定理）可以由子类使用。符号和setoid智能重写也可以用来以精美形式，类型安全和可扩展的方式演示定理。