以Coq解释类型的术语

Question

我正在自下而上地从Naturals构建Integers，并尝试直接应用态射重写，而不是将其添加为setoid态射，因为在我的情况下这样做很困难而且很不自然，但是一个测试用例由于以下错误而失败：

The term "x = x" has type "Prop" while it is expected to have type "x = x".

以下MRE也会抛出该异常：

Require Import Setoid.

(* Custom natural Set *)
Parameter CNat : Set.

(* Addition *) 
Parameter CAdd : CNat -> CNat -> CNat. 
Infix "±" := CAdd (at level 50, left associativity).

(* Addition Morphism *)
Axiom cnat_add_morphism : 
  forall (x x' : CNat), x = x' ->
  forall (y y' : CNat), y = y' -> 
    x ± y = x' ± y'.

(* Test Example *)
Example cnat_add_inc : 
  forall (x y c : CNat), x = y -> x±c = y±c.
Proof.
  intros x y c CH.
  rewrite (@cnat_add_morphism x x (x=x) c c (c=c)). (* #Error *)

是否有可能告诉cnat_add_morphism（在我的代码中是一个定理，而不是一个公理）将x¦x和c¦c术语解释为一种使态射正常工作的类型，或者将其解释为能够应用手动形态学重写而不是将其添加为setoid？

Answer 1

您遇到的第一个问题是您要重写的术语类型不正确：

cnat_add_morphism x x (x¦x) c c (c¦c)

Answer 2

这里有几个问题。