From e3d278f82e9d54b9d1a3459cc0eefd861ffb116b Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 2 Oct 2020 11:02:07 +0200 Subject: [PATCH 1/3] Add Qp lemmas --- theories/numbers.v | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 451da9f8..ded9ee43 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -831,13 +831,16 @@ 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_not_plus_q_ge_1 (q: Qp) : ¬ (1 + q)%Qp ≤ 1%Qp. +Proof. apply Qp_not_plus_ge. Qed. + Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc. Proof. apply Qclt_le_weak, Qp_prf. Qed. @@ -856,6 +859,9 @@ Proof. |by apply Qcplus_le_mono_r]. Qed. +Lemma Qp_plus_id_free q p : q + p = q → False. +Proof. intro Heq. eapply (Qp_not_plus_ge q p). rewrite Heq. done. 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 +884,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 +901,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 +932,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 [[? ->]|[? ->]]; -- GitLab From 94a98b3fbf35fe6c821019e99afbbff9a4bee544 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 2 Oct 2020 11:20:40 +0200 Subject: [PATCH 2/3] Change eapply to apply --- theories/numbers.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/numbers.v b/theories/numbers.v index ded9ee43..9c1c0ab5 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -860,7 +860,7 @@ Proof. Qed. Lemma Qp_plus_id_free q p : q + p = q → False. -Proof. intro Heq. eapply (Qp_not_plus_ge q p). rewrite Heq. done. Qed. +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. -- GitLab From 028eb93c107b3f103c577e28a4e4b2c2544229f6 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 2 Oct 2020 13:00:54 +0200 Subject: [PATCH 3/3] Remove Qp_not_plus_q_ge_1 --- CHANGELOG.md | 9 +++++++++ theories/numbers.v | 3 --- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e5362c59..8152693b 100644 --- a/CHANGELOG.md +++ b/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) diff --git a/theories/numbers.v b/theories/numbers.v index 9c1c0ab5..3976a72b 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -838,9 +838,6 @@ Proof. apply Hle, Qp_prf. Qed. -Lemma Qp_not_plus_q_ge_1 (q: Qp) : ¬ (1 + q)%Qp ≤ 1%Qp. -Proof. apply Qp_not_plus_ge. Qed. - Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc. Proof. apply Qclt_le_weak, Qp_prf. Qed. -- GitLab