Lemma -> Let in HB.builders (#1295)

* Lemma -> Let in HB.builders

* fixes #1296

CHANGELOG_UNRELEASED.md

@@ -29,6 +29,13 @@
   + `measurable_normr` -> `normr_measurable`
   + `measurable_fine` -> `fine_measurable`
   + `measurable_natmul` -> `natmul_measurable`
+- in `topology.v`:
+  + in mixin `Nbhs_isUniform_mixin`:
+    * `entourage_refl_subproof` -> `entourage_diagonal_subproof`
+  + in factory `Nbhs_isUniform`:
+    * `entourage_refl` -> `entourage_diagonal`
+  + in factory `isUniform`:
+    * `entourage_refl` -> `entourage_diagonal`
 
 ### Generalized
 
@@ -50,6 +57,15 @@
   + notation `measurable_fun_opp` (was deprecated since 0.6.3)
   + notation `measurable_fun_normr` (was deprecated since 0.6.3)
   + notation `measurable_fun_fine` (was deprecated since 0.6.3)
+- in `topology.v`:
+  + turned into Let's (inside `HB.builders`):
+    * lemmas `nbhsE_subproof`, `openE_subproof`
+    * lemmas `nbhs_pfilter_subproof`, `nbhsE_subproof`, `openE_subproof`
+    * lemmas `open_fromT`, `open_fromI`, `open_from_bigU`
+    * lemmas `finI_from_cover`, `finI_from_join`
+    * lemmas `nbhs_filter`, `nbhs_singleton`, `nbhs_nbhs`
+    * lemmas `ball_le`, `entourage_filter_subproof`, `ball_sym_subproof`,
+      `ball_triangle_subproof`, `entourageE_subproof`
 
 ### Infrastructure
 

theories/topology.v

@@ -1974,7 +1974,7 @@ HB.builders Context T of Nbhs_isNbhsTopological T.
 
 Definition open_of_nbhs := [set A : set T | A `<=` nbhs^~ A].
 
-Lemma nbhsE_subproof (p : T) :
+Let nbhsE_subproof (p : T) :
   nbhs p = [set A | exists B, [/\ open_of_nbhs B, B p & B `<=` A] ].
 Proof.
 rewrite predeqE => A; split=> [p_A|]; last first.
@@ -1984,7 +1984,7 @@ exists (nbhs^~ A); split=> //; first by move=> ?; apply: nbhs_nbhs.
 by move=> q /nbhs_singleton.
 Qed.
 
-Lemma openE_subproof : open_of_nbhs = [set A : set T | A `<=` nbhs^~ A].
+Let openE_subproof : open_of_nbhs = [set A : set T | A `<=` nbhs^~ A].
 Proof. by []. Qed.
 
 HB.instance Definition _ := Nbhs_isTopological.Build T
@@ -2009,7 +2009,7 @@ HB.builders Context T of Pointed_isOpenTopological T.
 
 HB.instance Definition _ := hasNbhs.Build T (nbhs_of_open op).
 
-Lemma nbhs_pfilter_subproof (p : T) : ProperFilter (nbhs p).
+Let nbhs_pfilter_subproof (p : T) : ProperFilter (nbhs p).
 Proof.
 apply: Build_ProperFilter.
   by move=> A [B [_ Bp sBA]]; exists p; apply: sBA.
@@ -2021,11 +2021,11 @@ move=> A B sAB [C [Cop p_C sCA]].
 by exists C; split=> //; apply: subset_trans sAB.
 Qed.
 
-Lemma nbhsE_subproof (p : T) :
+Let nbhsE_subproof (p : T) :
   nbhs p = [set A | exists B, [/\ op B, B p & B `<=` A] ].
 Proof. by []. Qed.
 
-Lemma openE_subproof : op = [set A : set T | A `<=` nbhs^~ A].
+Let openE_subproof : op = [set A : set T | A `<=` nbhs^~ A].
 Proof.
 rewrite predeqE => A; split=> [Aop p Ap|Aop].
   by exists A; split=> //; split.
@@ -2055,10 +2055,10 @@ HB.builders Context T of Pointed_isBaseTopological T.
 
 Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
 
-Lemma open_fromT : open_from setT.
+Let open_fromT : open_from setT.
 Proof. exists D => //; exact: b_cover. Qed.
 
-Lemma open_fromI (A B : set T) : open_from A -> open_from B ->
+Let open_fromI (A B : set T) : open_from A -> open_from B ->
   open_from (A `&` B).
 Proof.
 move=> [DA sDAD AeUbA] [DB sDBD BeUbB].
@@ -2081,7 +2081,7 @@ rewrite predeqE => t; split=> [[_ [s ABs <-] bDtst]|ABt].
 by exists (get (Dt t)); [exists t| have /ABU/getPex [? []]:= ABt].
 Qed.
 
-Lemma open_from_bigU (I0 : Type) (f : I0 -> set T) :
+Let open_from_bigU (I0 : Type) (f : I0 -> set T) :
   (forall i, open_from (f i)) -> open_from (\bigcup_i f i).
 Proof.
 set fop := fun j => [set Dj | Dj `<=` D /\ f j = \bigcup_(i in Dj) b i].
@@ -2218,13 +2218,13 @@ HB.builders Context T of Pointed_isSubBaseTopological T.
 
 Local Notation finI_from := (finI_from D b).
 
-Lemma finI_from_cover : \bigcup_(A in finI_from) A = setT.
+Let finI_from_cover : \bigcup_(A in finI_from) A = setT.
 Proof.
 rewrite predeqE => t; split=> // _; exists setT => //.
 by exists fset0 => //; rewrite predeqE.
 Qed.
 
-Lemma finI_from_join A B t : finI_from A -> finI_from B -> A t -> B t ->
+Let finI_from_join A B t : finI_from A -> finI_from B -> A t -> B t ->
   exists k, [/\ finI_from k, k t & k `<=` A `&` B].
 Proof.
 move=> [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt.
@@ -4013,7 +4013,7 @@ Proof. by []. Qed.
 HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
-  entourage_refl_subproof : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
+  entourage_diagonal_subproof : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
   entourage_inv_subproof : forall A, entourage A -> entourage (A^-1)%classic;
   entourage_split_ex_subproof :
     forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
@@ -4027,7 +4027,7 @@ HB.structure Definition Uniform :=
 HB.factory Record Nbhs_isUniform M of Nbhs M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
-  entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
+  entourage_diagonal : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
   entourage_inv : forall A, entourage A -> entourage (A^-1)%classic;
   entourage_split_ex :
     forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
@@ -4036,23 +4036,23 @@ HB.factory Record Nbhs_isUniform M of Nbhs M := {
 
 HB.builders Context M of Nbhs_isUniform M.
 
-Lemma nbhs_filter (p : M) : ProperFilter (nbhs p).
+Let nbhs_filter (p : M) : ProperFilter (nbhs p).
 Proof.
 rewrite nbhsE nbhs_E; apply: filter_from_proper; last first.
-  by move=> A entA; exists p; apply/mem_set; apply: entourage_refl entA _ _.
+  by move=> A entA; exists p; apply/mem_set; apply: entourage_diagonal entA _ _.
 apply: filter_from_filter.
   by exists setT; exact: @filterT entourage_filter.
 move=> A B entA entB; exists (A `&` B); last by rewrite xsectionI.
 exact: (@filterI _ _ entourage_filter).
 Qed.
 
-Lemma nbhs_singleton (p : M) A : nbhs p A -> A p.
+Let nbhs_singleton (p : M) A : nbhs p A -> A p.
 Proof.
 rewrite nbhsE nbhs_E  => - [B entB sBpA].
-by apply/sBpA/mem_set; apply: entourage_refl entB _ _.
+by apply/sBpA/mem_set; exact: entourage_diagonal entB _ _.
 Qed.
 
-Lemma nbhs_nbhs (p : M) A : nbhs p A -> nbhs p (nbhs^~ A).
+Let nbhs_nbhs (p : M) A : nbhs p A -> nbhs p (nbhs^~ A).
 Proof.
 rewrite nbhsE nbhs_E => - [B entB sBpA].
 have /entourage_split_ex[C entC sC2B] := entB.
@@ -4064,23 +4064,26 @@ HB.instance Definition _ := Nbhs_isNbhsTopological.Build M
   nbhs_filter nbhs_singleton nbhs_nbhs.
 
 HB.instance Definition _ := Nbhs_isUniform_mixin.Build M
-  entourage_filter entourage_refl entourage_inv entourage_split_ex nbhsE.
+  entourage_filter entourage_diagonal entourage_inv entourage_split_ex nbhsE.
 
 HB.end.
 
 HB.factory Record isUniform M of Pointed M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
-  entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
+  entourage_diagonal : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
   entourage_inv : forall A, entourage A -> entourage (A^-1)%classic;
   entourage_split_ex :
     forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
 }.
 
 HB.builders Context M of isUniform M.
-  HB.instance Definition _ := @hasNbhs.Build M (nbhs_ entourage).
-  HB.instance Definition _ := @Nbhs_isUniform.Build M entourage
-    entourage_filter entourage_refl entourage_inv entourage_split_ex erefl.
+
+HB.instance Definition _ := @hasNbhs.Build M (nbhs_ entourage).
+
+HB.instance Definition _ := @Nbhs_isUniform.Build M entourage
+  entourage_filter entourage_diagonal entourage_inv entourage_split_ex erefl.
+
 HB.end.
 
 Lemma nbhs_entourageE {M : uniformType} : nbhs_ (@entourage M) = nbhs.
@@ -4119,14 +4122,13 @@ Qed.
 Section uniformType1.
 Context {M : uniformType}.
 
-Lemma entourage_refl (A : set (M * M)) x :
-  entourage A -> A (x, x).
-Proof. by move=> entA; apply: entourage_refl_subproof entA _ _. Qed.
+Lemma entourage_refl (A : set (M * M)) x : entourage A -> A (x, x).
+Proof. by move=> entA; exact: entourage_diagonal_subproof entA _ _. Qed.
 
 Global Instance entourage_pfilter : ProperFilter (@entourage M).
 Proof.
 apply Build_ProperFilter; last exact: entourage_filter.
-by move=> A entA; exists (point, point); apply: entourage_refl.
+by move=> A entA; exists (point, point); exact: entourage_refl.
 Qed.
 
 Lemma entourageT : entourage [set: M * M].
@@ -4326,7 +4328,7 @@ move=> [B [entB1 entB2] sBA] xy /eqP.
 rewrite [_.1]surjective_pairing [xy.2]surjective_pairing xpair_eqE.
 move=> /andP [/eqP xy1e /eqP xy2e].
 have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1), (xy.1.2, xy.2.2)).
-  by rewrite xy1e xy2e; split=> /=; apply: entourage_refl.
+  by rewrite xy1e xy2e; split=> /=; exact: entourage_refl.
 move=> [zt Azt /eqP]; rewrite !xpair_eqE.
 by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP<-.
 Qed.
@@ -4397,7 +4399,7 @@ Qed.
 Lemma mx_ent_refl A : mx_ent A -> [set MN | MN.1 = MN.2] `<=` A.
 Proof.
 move=> [B entB sBA] MN MN1e2; apply: sBA => i j.
-by rewrite MN1e2; apply: entourage_refl.
+by rewrite MN1e2; exact: entourage_refl.
 Qed.
 
 Lemma mx_ent_inv A : mx_ent A -> mx_ent (A^-1)%classic.
@@ -4738,7 +4740,7 @@ HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
 
 HB.builders Context R M of Nbhs_isPseudoMetric R M.
 
-Lemma ball_le x : {homo ball x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
+Let ball_le x : {homo ball x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
 Proof.
 move=> e1 e2 le12 y xe1_y.
 move: le12; rewrite le_eqVlt => /orP [/eqP <- //|].
@@ -4748,27 +4750,27 @@ suff : ball x (PosNum lt12)%:num x by [].
 exact: ball_center.
 Qed.
 
-Lemma entourage_filter_subproof : Filter ent.
+Let entourage_filter_subproof : Filter ent.
 Proof.
 rewrite entourageE; apply: filter_from_filter; first by exists 1 => /=.
 move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=.
 by rewrite subsetI; split=> ?; apply: ball_le;
    rewrite num_le// ge_min lexx ?orbT.
 Qed.
 
-Lemma ball_sym_subproof A : ent A -> [set xy | xy.1 = xy.2] `<=` A.
+Let ball_sym_subproof A : ent A -> [set xy | xy.1 = xy.2] `<=` A.
 Proof.
 rewrite entourageE; move=> [e egt0 sbeA] xy xey.
 apply: sbeA; rewrite /= xey; exact: ball_center.
 Qed.
 
-Lemma ball_triangle_subproof A : ent A -> ent (A^-1)%classic.
+Let ball_triangle_subproof A : ent A -> ent (A^-1)%classic.
 Proof.
 rewrite entourageE => - [e egt0 sbeA].
 by exists e => // xy xye; apply: sbeA; apply: ball_sym.
 Qed.
 
-Lemma entourageE_subproof A : ent A -> exists2 B, ent B & B \; B `<=` A.
+Let entourageE_subproof A : ent A -> exists2 B, ent B & B \; B `<=` A.
 Proof.
 rewrite entourageE; move=> [_/posnumP[e] sbeA].
 exists [set xy | ball xy.1 (e%:num / 2) xy.2].
@@ -5750,7 +5752,7 @@ by exists 0%N.
 Qed.
 
 Local Lemma n_step_ball_center x e : 0 < e -> n_step_ball 0 x e x.
-Proof. by move=> epos; split => //; apply: entourage_refl. Qed.
+Proof. by move=> epos; split => //; exact: entourage_refl. Qed.
 
 Local Lemma step_ball_center x e : 0 < e -> step_ball x e x.
 Proof. by move=> epos; exists 0%N; apply: n_step_ball_center. Qed.
@@ -6368,8 +6370,9 @@ move=> [x y] /=; case; first (by move=> ->; split=> /=; left).
 by move=> [Ax [Ay [Pxy Qxy]]]; split=> /=; right.
 Qed.
 
-Let subspace_uniform_entourage_refl : forall X : set (subspace A * subspace A),
-  subspace_ent X -> [set xy | xy.1 = xy.2] `<=` X.
+Let subspace_uniform_entourage_diagonal :
+  forall X : set (subspace A * subspace A),
+    subspace_ent X -> [set xy | xy.1 = xy.2] `<=` X.
 Proof.
 by move=> ? + [x y]/= ->; case=> V entV; apply; left.
 Qed.
@@ -6426,7 +6429,7 @@ case: (@nbhs_subspaceP X A x); rewrite propeqE; split => //=.
 Unshelve. all: by end_near. Qed.
 
 HB.instance Definition _ := Nbhs_isUniform_mixin.Build (subspace A)
-  Filter_subspace_ent subspace_uniform_entourage_refl
+  Filter_subspace_ent subspace_uniform_entourage_diagonal
   subspace_uniform_entourage_inv subspace_uniform_entourage_split_ex
   subspace_uniform_nbhsE.