如何使用Coq中的Rmult重写Rle中的Rle？

Question

关于关系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执行重写步骤并简单地将被乘数的非负性作为证明义务？谢谢.

Answer 1

我认为定义你想要的东西应该是可能的，但可能不是微不足道的。

\n\n

但是，您可能对使用 math-comp 的代数层次结构的不同方法感兴趣，请参阅：

\n\n

Lemma ler_pmul2l x : 0 < x \xe2\x86\x92 {mono *%R x : x y / x \xe2\x89\xa4 y}.\n

\n\n

和相关引理（http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html）。在 ssreflect 中<=是一个布尔关系，因此可以按照a <= b实际含义进行普通重写a <= b = true。

\n