Merge branch 'qp-lemmas' into 'master'

Add Qp lemmas

See merge request iris/stdpp!187

CHANGELOG.md

@@ -7,6 +7,15 @@ API-breaking change is listed.
   and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
 - Add `max` and `min` operations for `Qp`.
 - Add additional lemmas for `Qp`.
+- Remove the lemma `Qp_not_plus_q_ge_1` in favor of `Qp_not_plus_ge`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i '
+s/\bQp_not_plus_q_ge_1\b/Qp_not_plus_ge/g
+' $(find theories -name "*.v")
+```
 
 ## std++ 1.4.0 (released 2020-07-15)
 

theories/numbers.v

@@ -831,11 +831,11 @@ Proof.
     + by rewrite Qp_div_2.
 Qed.
 
-Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc.
+Lemma Qp_not_plus_ge (q p : Qp) : ¬ (q + p)%Qp ≤ q.
 Proof.
-  intros Hle.
-  apply (Qcplus_le_mono_l q 0 1) in Hle.
-  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
+  rewrite <- (Qcplus_0_r q).
+  intros Hle%(Qcplus_le_mono_l p 0 q)%Qcle_ngt.
+  apply Hle, Qp_prf.
 Qed.
 
 Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
@@ -856,6 +856,9 @@ Proof.
                              |by apply Qcplus_le_mono_r].
 Qed.
 
+Lemma Qp_plus_id_free q p : q + p = q → False.
+Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq.  Qed.
+
 Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
 Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed.
 
@@ -878,14 +881,14 @@ Qed.
 Lemma Qp_max_spec_le (q p : Qp) : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
 Proof. destruct (Qp_max_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed.
 
-Instance Qc_max_assoc : Assoc (=) Qp_max.
+Instance Qp_max_assoc : Assoc (=) Qp_max.
 Proof.
   intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o));
     eauto using decide_True, Qcle_trans.
   rewrite decide_False by done.
   by rewrite decide_False by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge).
 Qed.
-Instance Qc_max_comm : Comm (=) Qp_max.
+Instance Qp_max_comm : Comm (=) Qp_max.
 Proof.
   intros q p. apply Qp_eq.
   destruct (Qp_max_spec_le q p) as [[?->]|[?->]], (Qp_max_spec_le p q) as [[?->]|[?->]];
@@ -895,11 +898,11 @@ Qed.
 Lemma Qp_max_id q : q `max` q = q.
 Proof. by destruct (Qp_max_spec q q) as [[_->]|[_->]]. Qed.
 
-Lemma Qc_le_max_l (q p : Qp) : q ≤ q `max` p.
+Lemma Qp_le_max_l (q p : Qp) : q ≤ q `max` p.
 Proof. unfold Qp_max. by destruct (decide (q ≤ p)). Qed.
 
-Lemma Qc_le_max_r (q p : Qp) : p ≤ q `max` p.
-Proof. rewrite (comm _ q). apply Qc_le_max_l. Qed.
+Lemma Qp_le_max_r (q p : Qp) : p ≤ q `max` p.
+Proof. rewrite (comm _ q). apply Qp_le_max_l. Qed.
 
 Lemma Qp_max_plus (q p : Qp) : q `max` p ≤ q + p.
 Proof.
@@ -926,14 +929,14 @@ Qed.
 Lemma Qp_min_spec_le (q p : Qp) : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
 Proof. destruct (Qp_min_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed.
 
-Instance Qc_min_assoc : Assoc (=) Qp_min.
+Instance Qp_min_assoc : Assoc (=) Qp_min.
 Proof.
   intros q p o. unfold Qp_min.
   destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
   - rewrite decide_True by done. by rewrite decide_True by (eapply Qcle_trans; done).
   - by rewrite (decide_False _ _) by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge).
 Qed.
-Instance Qc_min_comm : Comm (=) Qp_min.
+Instance Qp_min_comm : Comm (=) Qp_min.
 Proof.
   intros q p. apply Qp_eq.
   destruct (Qp_min_spec_le q p) as [[?->]|[?->]], (Qp_min_spec_le p q) as [[? ->]|[? ->]];