Come riscrivere su Rle all'interno di un termine con Rmult in Coq?

Question

Per quanto riguarda la relazione RLE (< =), posso riscrivere all'interno Rplus (+) e Rminus (-), varianza poiché entrambe le posizioni di entrambi gli operatori binari sono fissati:

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. 

Sfortunatamente, Rmult (*) non ha questa proprietà: la varianza dipende dal fatto che l'altro multiplo sia positivo o negativo. È possibile definire un morfismo condizionale, in modo che Coq esegua la fase di riscrittura e aggiunga semplicemente la non negatività del multiplicand come obbligo di prova? Grazie.

Answer 1

Penso che la definizione di ciò che si desidera sia possibile ma probabilmente non banale.

Tuttavia si può essere interessati a un approccio diverso utilizzando la gerarchia algebrica di matematica-comp, vedi:

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

e relativo lemmi (http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html). In ssreflect <= è una relazione booleana per cui è possibile riscrivere la vaniglia come a <= b significa davvero a <= b = true.