0

我正在从 Naturals 自下而上构建整数，并尝试直接应用态射重写，而不是将其添加为 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？

4

2 回答 2

1

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

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

你有

cnat_add_morphism x x : x¦x -> forall y y', y¦y' -> x ± y ¦ x ± y'

所以你需要提供证明，x¦x但你x¦x自己提供。您实际上需要在系统中添加自反性证明。就像是

Parameter CRefl : forall (x : CNat), x¦x.

然后你可以证明你的引理。

Example cnat_add_inc : 
  forall (x y c : CNat), 
    x¦y -> 
    x ± c ¦ y ± c.
Proof.
  intros x y c CH.
  apply cnat_add_morphism.
  - assumption.
  - apply CRefl.
Qed.
于 2020-03-26T13:47:32.420 回答
1

这里有几个问题。

首先，错误意味着您试图给出cnat_add_morphism一个命题而不是对该命题的证明。在 Coq 中，证明是它们所证明的命题类型的对象。例如，forall x : CNat, x¦x是一种类型，您必须构建该类型的对象以保证该类型为真。这就像你有一个函数f : nat -> nat并且你写了f nat，你会得到以下错误：

The term "nat" has type "Set" while it is expected to have type "nat".

您收到的错误完全相同。因此，您需要提供“x ¦ x”类型的对象，即保证命题x ¦ x为真的证明。所以你可以使用ceq_reflexivity公理。该术语(ceq_reflexivity x)具有类型x¦x，您可以使用它来代替x¦x.

(cnat_add_morphism x x (ceq_reflexivity x))

其次，您需要应用引理而不是重写它并使用假设而不是x¦x（仅使用 x 和 y 而不是 x）。

apply (cnat_add_morphism x y CH c c (ceq_reflexivity c)).
于 2020-03-26T13:50:05.983 回答