Wie überschreibt man Rle innerhalb eines Terms mit Rmult in Coq?

Question

Im Hinblick auf die Beziehung Rle (< =), kann ich umschreiben innen Rplus (+) und Rminus (-), da beide Positionen der beiden binären Operatoren haben feste Varianz:

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. 

Leider Rmult (*) hat diese Eigenschaft nicht: die Varianz hängt davon ab, ob der andere Multiplikand positiv oder negativ ist. Ist es möglich, einen bedingten Morphismus zu definieren, so dass Coq den Schritt des Umschreibens ausführt und einfach die Nicht-Negativität des Multiplikanden als Beweispflicht hinzufügt? Vielen Dank.

Answer 1

Ich denke, dass die Definition, was Sie wollen, sollte möglich sein, aber wahrscheinlich nicht trivial.

auch immer Sie in einem anderen Ansatz interessiert sein kann, die algebraischen Hierarchie der Mathe-comp finden Sie unter:

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

und damit verbundene Lemmata (http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html). In ssreflect <= ist eine boolesche Relation, so dass Vanilla Rewriting möglich ist, da a <= b wirklich a <= b = true bedeutet.