Làm thế nào để viết lại Rle bên trong một thuật ngữ với Rmult trong Coq?

Question

liên quan đến mối quan hệ Với RLE (< =), tôi có thể viết lại bên RPLUS (+) và Rminus (-), sai vì cả hai vị trí của cả hai nhà khai thác nhị phân đã cố định:

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. 

Thật không may, Rmult (*) không có khách sạn này: phương sai phụ thuộc vào việc nhơn khác là tích cực hay tiêu cực. Có thể xác định một hình thái có điều kiện, để Coq thực hiện bước viết lại và chỉ cần thêm sự không tiêu cực của phép nhân và làm nghĩa vụ chứng minh? Cảm ơn.

Answer 1

Tôi nghĩ rằng việc xác định những gì bạn muốn là có thể nhưng có thể không tầm thường.

Tuy nhiên bạn có thể quan tâm đến một cách tiếp cận khác nhau bằng cách sử dụng hệ thống cấp bậc đại số của toán học-comp, xem:

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

và bổ đề liên quan (http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html). Trong ssreflect <= là một mối quan hệ boolean để vani viết lại có thể như a <= b thực sự có nghĩa a <= b = true.