时间戳

首页 > 解决方案 > 在 Coq 中使用 Typeclasses 重用 Axiom

coq - 在 Coq 中使用 Typeclasses 重用 Axiom

问题描述

我正在尝试使用类型类进行代码重用，但是在子类型类定理中应用父类型类公理时遇到了 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 公理，这里缺少什么？有一个更好的方法吗？

标签： coq

解决方案

这可能部分是因为您的示例过于简化，但是从右到左重写cdisc_add_neutral是有问题的，因为右侧x匹配任何内容并且可以具有任何类型。

你得到的错误是 Coq 试图用它重写整个目标，但这会使用逻辑暗示impl，这反过来又要求你的关系CEq是 的子关系impl。

您可以通过稍微专门化引理来避免这种情况：

  rewrite <- (cdisc_add_neutral CNat) at 1.

您需要 ，at 1因为现在匹配的子项是O CNat，但它在您的目标中出现了 3 次。rewrite默认情况下会尝试重写所有这些，这需要Proper此处缺少的实例。（您可以通过Parametric Morphism手册中描述的机制获得这些）。

此外，您可以从左到右重写：

rewrite cdisc_add_neutral

推荐阅读