How to rewrite over Rle inside a term with Rmult in Coq?

Question

With respect to the relation Rle (<=), I can rewrite inside Rplus (+) and Rminus (-), since both positions of both binary operators have fixed variance:

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.

Unfortunately, Rmult (*) does not have this property: the variance depends on whether the other multiplicand is positive or negative. Is it possible to define a conditional morphism, so that Coq performs the rewriting step and simply adds the non-negativity of the multiplicand as a proof obligation? Thanks.

Bornite

You can always try the coq-club mailing list, you might get lucky :) – This

Answer 1

I think that defining what you want should be possible but likely not trivial.

However you may be interested in a different approach using the algebraic hierarchy of math-comp, see:

Lemma ler_pmul2l x : 0 < x → {mono *%R x : x y / x ≤ y}.

and related lemmas ( http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html ). In ssreflect <= is a boolean relation so vanilla rewriting is possible as a <= b really means a <= b = true.

Eliezer