From a19fcf72d53dc4e0f00a83407b574b92fff5f833 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 22 Oct 2025 14:27:27 +0900 Subject: [PATCH] generalize onem Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 4 ++++ classical/unstable.v | 50 ++++++++++++++++++++++------------------- 2 files changed, 31 insertions(+), 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 81d8772ba5..4519951d89 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -347,6 +347,10 @@ - in `probabilitity.v`: + lemma `exponential_pdf_ge0` (hypothesis generalized) +- in `unstable.v`: + + generalized from `numDomainType` to `pzRingType`: + + definition `onem`, lemmas `onme0`, `onem1`, `add_onemK`, `onemD`, `onemMr`, `onemM` + ### Deprecated ### Removed diff --git a/classical/unstable.v b/classical/unstable.v index 9b57974e44..ada5b95f4f 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -232,21 +232,38 @@ elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0. by rewrite (leq_trans (leq_card_setU _ _))// leq_add. Qed. -Section onem. -Variable R : numDomainType. -Implicit Types r : R. +Definition onem {R : pzRingType} (r : R) : R := 1 - r. +Notation "`1- r" := (onem r) : ring_scope. -Definition onem r := 1 - r. -Local Notation "`1- r" := (onem r). +Section onem_ring. +Context {R : pzRingType}. +Implicit Type r : R. -Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed. +Lemma onem0 : `1-0 = 1 :> R. Proof. by rewrite /onem subr0. Qed. -Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed. +Lemma onem1 : `1-1 = 0 :> R. Proof. by rewrite /onem subrr. Qed. Lemma onemK r : `1-(`1-r) = r. Proof. exact: subKr. Qed. -Lemma add_onemK r : r + `1- r = 1. -Proof. by rewrite /onem addrC subrK. Qed. +Lemma add_onemK r : r + `1- r = 1. Proof. by rewrite /onem addrC subrK. Qed. + +Lemma onemD r s : `1-(r + s) = `1-r - s. +Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. + +Lemma onemMr r s : s * `1-r = s - s * r. +Proof. by rewrite /onem mulrBr mulr1. Qed. + +Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. +Proof. +rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. +by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. +Qed. + +End onem_ring. + +Section onem_order. +Variable R : numDomainType. +Implicit Types r : R. Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. @@ -265,20 +282,7 @@ Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. -Lemma onemD r s : `1-(r + s) = `1-r - s. -Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. - -Lemma onemMr r s : s * `1-r = s - s * r. -Proof. by rewrite /onem mulrBr mulr1. Qed. - -Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. -Proof. -rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. -by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. -Qed. - -End onem. -Notation "`1- r" := (onem r) : ring_scope. +End onem_order. Lemma onemV (F : numFieldType) (x : F) : x != 0 -> `1-(x^-1) = (x - 1) / x. Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.