Merge pull request #1238 from affeldt-aist/fixes_20240605

Fixes 20240605

CHANGELOG_UNRELEASED.md

@@ -188,6 +188,9 @@
   + canonical `rev_mulmx`
   + structure `revop`
 
+- in `reals.v`
+  + lemma `inf_lower_bound` (use `inf_lb` instead)
+
 ### Infrastructure
 
 ### Misc

classical/classical_sets.v

@@ -144,16 +144,20 @@ From mathcomp Require Import mathcomp_extra boolp.
 (*                                P must be a set on a pointedType.           *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ## squash/unsquash                                                         *)
 (* ```                                                                        *)
-(*                      $| T | == T : Type is inhabited                       *)
-(*                    squash x == proof of $| T | (with x : T)                *)
-(*                  unsquash s == extract a witness from s : $| T |           *)
+(*                      $| T | == the type `T : Type` is inhabited            *)
+(*                                $| T | has type `Prop`.                     *)
+(*                                $| T | is a notation for `squashed T`.      *)
+(*                    squash x == object of type $| T | (with x : T)          *)
+(*                  unsquash s == extract an inhabitant of type `T`           *)
+(*                                (with s : $| T |)                           *)
 (* ```                                                                        *)
-(*                                                                            *)
-(* ## Tactic                                                                  *)
+(* Tactic:                                                                    *)
 (*   - squash x:                                                              *)
 (*     solves a goal $| T | by instantiating with x or [the T of x]           *)
 (*                                                                            *)
+(* ## Pairwise-disjoint sets                                                  *)
 (* ```                                                                        *)
 (*                trivIset D F == the sets F i, where i ranges over           *)
 (*                                D : set I, are pairwise-disjoint            *)

classical/functions.v

@@ -17,12 +17,12 @@ Add Search Blacklist "_mixin_".
 (*          set_fun A B f == f : aT -> rT is a function with domain           *)
 (*                           A : set aT and codomain B : set rT               *)
 (*         set_surj A B f == f is surjective                                  *)
-(*          set inj A B f == f is injective                                   *)
+(*          set_inj A B f == f is injective                                   *)
 (*          set_bij A B f == f is bijective                                   *)
 (*                                                                            *)
 (*          {fun A >-> B} == type of functions f : aT -> rT from A : set aT   *)
-(*                           to B : set rT.                                   *)
-(*                           funS f  is a proof of  set_fun A B f             *)
+(*                           to B : set rT                                    *)
+(*                           `funS f` is a proof of `set_fun A B f`.          *)
 (*       {oinv aT >-> rT} == type of functions with a partial inverse         *)
 (*      {oinvfun A >-> B} == combination of {fun A >-> B} and                 *)
 (*                           {oinv aT >-> rT}                                 *)
@@ -48,10 +48,14 @@ Add Search Blacklist "_mixin_".
 (* ```                                                                        *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*              funin A f == alias for f : aT -> rT, with A : set aT          *)
-(*             [fun f in A] == the function f from the set A to the set f @` A*)
-(*            'split_ d f == partial injection from aT : Type to rt : Type;   *)
-(*                           f : aT -> rT, d : rT -> aT                       *)
+(*           [fun f in A] == the function f from the set A to the set f @` A  *)
+(*                           with f : aT -> rT and A : set aT                 *)
+(*                           This is a notation for funin A f, which is an HB *)
+(*                           alias.                                           *)
+(*            'split_ d f == partial injection from aT : Type to rT : Type,   *)
+(*                           f : aT -> rT, and d : rT -> aT                   *)
+(*                           This is a notation for split_ d f which is an HB *)
+(*                           alias.                                           *)
 (*                  split := 'split_(fun=> point)                             *)
 (*             @to_setT T == function that associates to x : T a dependent    *)
 (*                           pair of x with a proof that x belongs to setT    *)
@@ -80,7 +84,9 @@ Add Search Blacklist "_mixin_".
 (*                           A and B are intended to be the ranges of f and g *)
 (*           'pinv_ d A f == inverse of the function [fun f in A] over        *)
 (*                           f @` A, function d outside of f @` A             *)
-(*                  pinv := notation for 'pinv_(fun=> point)                  *)
+(*                           This is a notation for pinv_ which is defined as *)
+(*                           the inverse of a partial injection ('split_).    *)
+(*                   pinv := 'pinv_(fun=> point)                              *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Function restriction                                                    *)

theories/realfun.v

@@ -286,12 +286,11 @@ Lemma nonincreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O ->
 Proof.
 move=> ab lef ubf; set M := sup _.
 have supf : has_sup [set f x | x in [set` Interval (BRight a) b]].
-  split => //; case: b ab {lef ubf M} => [[|] t ta|[]] /=.
+  split => //; case: b ab {lef ubf M} => [[|] t ta|[]] //=.
   - exists (f ((a + t) / 2)), ((a + t) / 2) => //=.
     by rewrite in_itv/= !midf_lt.
   - exists (f ((a + t) / 2)), ((a + t) / 2) => //=.
     by rewrite in_itv/= midf_lt// midf_le// ltW.
-  - by exists (f (a + 1)), (a + 1).
   - by exists (f (a + 1)), (a + 1) => //=; rewrite in_itv/= ltrDl andbT.
 apply/cvgrPdist_le => _/posnumP[e].
 have {supf} [p [ap pb]] :

theories/reals.v

@@ -375,12 +375,6 @@ Variables (R : realType).
 Implicit Types E : set R.
 Implicit Types x : R.
 
-Lemma inf_lower_bound E : has_inf E -> lbound E (inf E).
-Proof.
-move=> /has_inf_supN /sup_upper_bound /ubP inflb; apply/lbP => x.
-by rewrite memNE => /inflb; rewrite lerNl.
-Qed.
-
 Lemma inf_adherent E (eps : R) : 0 < eps ->
   has_inf E -> exists2 e, E e & e < inf E + eps.
 Proof.
@@ -735,7 +729,7 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l :
 Proof.
 set P := [set y | _]; move=> hs; rewrite -subr_gt0.
 move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
-by exists x=> //; move/lbP : (inf_lower_bound hs) => -> //; exists x.
+by exists x => //; rewrite (inf_lb hs.2)//; exists x.
 Qed.
 
 End Sup.