Coq에서 Rmult를 사용하여 용어 내에서 Rle을 덮어 쓰는 방법은 무엇입니까? 관계에 대하여

Question

는 RLE (< =), I 내부 재기록 가능 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

당신이 원하는 것을 정의하는 것이 가능해야하지만 사소한 일은 아니라고 생각합니다. 당신이 수학 빌려 대수 계층 구조를 사용하여 다른 접근 방식에 관심이있을 수 그러나

, 참조 :

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

및 관련 보조 정리 (http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html). ssreflect에서는 이 실제로는 a <= b = true을 의미하므로 바닐라 재 작성이 가능한 부울 관계입니다.