在Coq中使用类型类的公理重用
在Coq中使用类型类的公理重用
提问于 2020-03-30 09:05:56
我试图使用类型类来实现代码重用，但在子类型类定理中应用父类型类公理时，我遇到了setoid错误。我用下面的相等和加法操作做了一个MRE：
Require Import Setoid.
(* Equality *)
Parameter CEq : forall A, A->A->Prop.
Arguments CEq [A] _ _.
Notation "x ¦ y" := (CEq x y) (at level 70, no associativity).
Axiom ceq_reflexivity: forall A, forall a:A, a¦a.
Axiom ceq_symmetry: forall A, forall a b:A, a¦b->b¦a.
Axiom ceq_transitivity: forall A, forall a b c:A, a¦b->b¦c->a¦c.
Add Parametric Relation A : (A) (@CEq A)
reflexivity proved by (@ceq_reflexivity A)
symmetry proved by (@ceq_symmetry A)
transitivity proved by (@ceq_transitivity A)
as ceq_rel.
(* Addition *)
Parameter CAdd: forall A, A->A->A.
Arguments CAdd [A] _ _.
Infix "±" := CAdd (at level 50, left associativity).下面是父类和子类：
(* Parent Typeclass *)
Class CDiscT (CDisc: Set) := {
O: forall CDisc, CDisc;
cdisc_add_neutral:forall CDisc, forall x:CDisc, x±(O CDisc)¦x;
}.
(* Natural Set & Child Typeclass *)
Parameter CNat: Set.
Class CNatT `{CDiscT CNat} := {}.这就是失败的定理：
(* Axiom inheritance test *)
Example test `{CNatT}: (O CNat)¦(O CNat)±(O CNat).
Proof.
rewrite <- cdisc_add_neutral. (* Error *)
reflexivity.
Qed.下面是错误：
Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
In environment:
H : CDiscT CNat
H0 : CNatT
?s : "subrelation (CEq (A:=Prop)) (Basics.flip Basics.impl)"为了能够在CNatT定理中使用CDiscT公理，这里缺少什么？有没有更好的方法来做这件事？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-30 10:05:43
这在一定程度上可能是因为您的示例过于简单，但是使用cdisc_add_neutral从右向左重写是有问题的，因为右侧的x可以匹配任何内容，并且可以具有任何类型。
你得到的错误是，Coq试图用它重写整个目标，但这将使用逻辑蕴含impl，这反过来要求您的关系CEq是impl的子关系。
您可以通过稍微专门化引理来避免这种情况：
rewrite <- (cdisc_add_neutral CNat) at 1.您需要at 1，因为现在匹配的子项是O CNat，但它在您的目标中出现了三次。默认情况下，rewrite会尝试重写所有这些实例，这需要这里缺少的Proper实例。(您可以通过手册中描述的Parametric Morphism机制获得这些内容)。
此外，您还可以从左到右重写：
rewrite cdisc_add_neutral页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60922736
复制相关文章
相似问题
腾讯云开发者
