From 27d73e309c7115165a958bbebddd27d0650b246c Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 23 Sep 2026 15:55:50 +0200 Subject: [PATCH 1/4] Add function to restrict a real to the intervale [0 , 1] --- classical/unstable.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/classical/unstable.v b/classical/unstable.v index 7e3c2827f8..a00c61015e 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -55,6 +55,33 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. +Section Clamp. +Context {R : realFieldType}. + +Definition clamp (x : R) := + Num.max (Num.min x 1) 0. + +Lemma ge0_clamp x : 0 <= clamp x. +Proof. by rewrite le_max lexx orbT. Qed. + +Lemma le1_clamp x : clamp x <= 1. +Proof. by rewrite ge_max ge_min lexx ler01 orbT. Qed. + +Definition cp01_clamp := (ge0_clamp, le1_clamp). + +Lemma clamp_in01 x : 0 <= x <= 1 -> clamp x = x. +Proof. by case/andP=> ge0_x le1_x; rewrite /clamp min_l ?max_l. Qed. + +Lemma clamp_id x : clamp (clamp x) = clamp x. +Proof. by rewrite clamp_in01 // !cp01_clamp. Qed. + +Lemma clamp0 : clamp 0 = 0. +Proof. by rewrite clamp_in01 // lexx ler01. Qed. + +Lemma clamp1 : clamp 1 = 1. +Proof. by rewrite clamp_in01 // lexx ler01. Qed. +End Clamp. + Module Order. Import Order. Definition default_display : disp_t. From f5fe6e6cc90e18aff81d090413bd7c8b9446c03d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Sep 2026 00:46:39 +0900 Subject: [PATCH 2/4] tentative gen --- classical/unstable.v | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index a00c61015e..5eea5e28e9 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -56,30 +56,31 @@ Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. Section Clamp. -Context {R : realFieldType}. +Context {R : realDomainType} (min max : R). +Hypothesis minmax : min <= max. -Definition clamp (x : R) := - Num.max (Num.min x 1) 0. +Definition clamp (x : R) := Num.max (Num.min x max) min. -Lemma ge0_clamp x : 0 <= clamp x. +Lemma clamp_gemin x : min <= clamp x. Proof. by rewrite le_max lexx orbT. Qed. -Lemma le1_clamp x : clamp x <= 1. -Proof. by rewrite ge_max ge_min lexx ler01 orbT. Qed. +Lemma clamp_lemax x : clamp x <= max. +Proof. by rewrite ge_max ge_min lexx minmax orbT. Qed. -Definition cp01_clamp := (ge0_clamp, le1_clamp). +Definition clamp_gele := (clamp_gemin, clamp_lemax). -Lemma clamp_in01 x : 0 <= x <= 1 -> clamp x = x. -Proof. by case/andP=> ge0_x le1_x; rewrite /clamp min_l ?max_l. Qed. +Lemma minmax_clamp x : min <= x <= max -> clamp x = x. +Proof. by case/andP => minx xmax; rewrite /clamp min_l ?max_l. Qed. Lemma clamp_id x : clamp (clamp x) = clamp x. -Proof. by rewrite clamp_in01 // !cp01_clamp. Qed. +Proof. by rewrite minmax_clamp// !clamp_gele. Qed. -Lemma clamp0 : clamp 0 = 0. -Proof. by rewrite clamp_in01 // lexx ler01. Qed. +Lemma clamp_min : clamp min = min. +Proof. by rewrite minmax_clamp// lexx minmax. Qed. + +Lemma clamp_max : clamp max = max. +Proof. by rewrite minmax_clamp// lexx minmax. Qed. -Lemma clamp1 : clamp 1 = 1. -Proof. by rewrite clamp_in01 // lexx ler01. Qed. End Clamp. Module Order. From 00d755c5918624213c60341b36bdc24b16b7bf5a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Oct 2026 14:21:03 +0900 Subject: [PATCH 3/4] changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d90a8985a4..84f327da8d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,6 +14,11 @@ - in `uniform_structure.v`: + lemma `unif_continuous_continuous` +- in `unstable.v`: + + definitions `clamp`, `clamp_gele` + + lemmas `clamp_gemin`, `clamp_lemax`, `minmax_clamp`, + `clamp_id`, `clamp_min`, `clamp_max` + ### Changed - in `esum.v`: From e1ca00c6e739026a06236de16949fbd82b39c9fc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Oct 2026 14:22:38 +0900 Subject: [PATCH 4/4] doc --- classical/unstable.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/classical/unstable.v b/classical/unstable.v index 5eea5e28e9..3b00d8cfc2 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -14,6 +14,7 @@ From mathcomp Require Import vector archimedean interval matrix. (* and mention it in the changelog. *) (* *) (* ``` *) +(* clamp x := max (min x max) min *) (* swap x := (x.2, x.1) *) (* map_pair f x := (f x.1, f x.2) *) (* nondecreasing_fun f == the function f is non-decreasing *) @@ -47,7 +48,6 @@ From mathcomp Require Import vector archimedean interval matrix. Attributes warn(note="The unstable.v file should only be used inside analysis.", cats="internal-analysis"). -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive.