关于关系 Rle (<=)，我可以在 Rplus (+) 和 Rminus (-) 内部重写，因为两个二元运算符的两个位置都有固定的方差:
Require Import Setoid Relation_Definitions Reals.
Open Scope R.
Add Parametric Relation : R Rle
reflexivity proved by Rle_refl
transitivity proved by Rle_trans
as Rle_setoid_relation.
Add Parametric Morphism : Rplus with
signature Rle ++> Rle ++> Rle as Rplus_Rle_mor.
intros ; apply Rplus_le_compat ; assumption.
Qed.
Add Parametric Morphism : Rminus with
signature Rle ++> Rle --> Rle as Rminus_Rle_mor.
intros ; unfold Rminus ;
apply Rplus_le_compat;
[assumption | apply Ropp_le_contravar ; assumption].
Qed.
Goal forall (x1 x2 y1 y2 : R),
x1 <= x2 -> y1 <= y2 ->
x1 - y2 <= x2 - y1.
Proof.
intros x1 x2 y1 y2 x1_le_x2 y1_le_y2;
rewrite x1_le_x2; rewrite y1_le_y2;
reflexivity.
Qed.
不幸的是，Rmult (*) 没有这个属性:方差取决于另一个被乘数是正数还是负数。是否可以定义条件态射，以便 Coq 执行重写步骤并简单地添加被乘数的非负性作为证明义务？谢谢。
最佳答案
我认为定义你想要的应该是可能的，但可能不是微不足道的。
但是，您可能对使用 math-comp 的代数层次结构的不同方法感兴趣，请参阅:
Lemma ler_pmul2l x : 0 < x → {mono *%R x : x y / x ≤ y}.
和相关的引理 ( http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html )。在 ssreflect
<=是一个 bool 关系，所以普通重写是可能的，如 a <= b真正的意思是a <= b = true .
关于relation - 如何在 Coq 中使用 Rmult 在一个术语中重写 Rle？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/27929242/