使用大于定理中的等价定理

Question

我在自然数的上下文中具有以下等于，小于和加法的运算定义：

Require Import Setoid.

(* CNat Set *)
Parameter (CNat:Set) (O i:CNat).

(* CEq Equivalence *)
Parameter CEq: CNat->CNat->Prop.
Infix "¦" := CEq (at level 70, no associativity).
Axiom ceq_refl: forall x:CNat, x¦x.
Axiom ceq_sym: forall x y:CNat, x¦y->y¦x.
Axiom ceq_trans: forall x y z:CNat, x¦y->y¦z->x¦z.
Add Relation CNat CEq
  reflexivity proved by ceq_refl
  symmetry proved by ceq_sym
  transitivity proved by ceq_trans
  as ceq_rel.

(* CLe StrictOrder *)
Parameter CLe: CNat->CNat->Prop.
Infix "«" := CLe (at level 70).
Axiom cle_irrefl: forall x:CNat, ~x«x.
Axiom cle_trans: forall x y z:CNat, x«y->y«z->x«z.
Add Relation CNat CLe
  transitivity proved by cle_trans
  as cle_rel.

(* CAdd Operation *)
Parameter CAdd : CNat->CNat->CNat.
Infix "±" := CAdd (at level 50, left associativity).
Add Morphism CAdd with signature CEq ==> CEq ==> CEq 
  as ceq_add_mor. Admitted.

然后我定义中性加法和自然归纳法，并尝试在检验定理中使用它们：

(* CNat Axioms *)
Axiom cnat_add_neutral: forall x:CNat, x±O¦x.
Axiom cnat_induction: forall P: CNat->Prop, P O ->
    (forall x:CNat, P x->P (x±i)) -> forall x:CNat, P x.

(* CNat Test Theorem *)
Example cle_neutral_test: forall x:CNat, O«x -> O«x±O.
Proof.
  intros x CH.
  rewrite cant_add_neutral. (* Error *)
  apply CH.
Qed.

出现以下错误：

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
In environment:
x : CNat
CH : O « x
do_subrelation := Morphisms.do_subrelation : Morphisms.apply_subrelation

?p : "Morphisms.Proper (CEq ==> Basics.flip Basics.impl) (CLe O)"

在使此测试生效之前，我应该产生什么样的先前定义或演示？

Answer 1

（（使用更多标准符号，希望您仍然清楚。CEq为==，CLe为<（可能应命名为CLt））

首先，在深入研究重写之前，请确保您在逻辑上有足够的事实来证明该定理。

您想证明x < y，并且您知道y == z。为此，您需要以下引理将目标更改为x < z：

y == z -> x < z -> x < y

目前不在事实列表中。

提出适合通用重写的事实的一种方法是作为Morphism的CLe声明：

Add Morphism CLe with signature CEq ==> CEq ==> iff
  as ceq_cle_mor. Admitted.

签名CEq ==> CEq ==> iff表示：

forall x x',
  x == x' ->
  forall y y',
  y == y' ->
  (x < y) <-> (x' < y')

哪个人可以很容易地检查出上述缺失事实的概括。添加了它，并修复了cnat_add_neutral引理中的错字（在问题的初始版本中，现在已编辑），证明会通过。

Add Morphism CLe with signature CEq ==> CEq ==> iff
  as ceq_cle_mor. Admitted.

(* CNat Test Theorem *)
Example cle_neutral_test: forall x:CNat, O«x -> O«x±O.
Proof.
  intros x CH.
  rewrite cnat_add_neutral. (* Error *)
  apply CH.
Qed.