From 0dd339f91dc8c34bcf902fc9df8e5400e29bdb31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 17 Nov 2024 23:26:58 +0900 Subject: [PATCH] linting --- CHANGELOG_UNRELEASED.md | 5 +- classical/boolp.v | 16 +- theories/homotopy_theory/wedge_sigT.v | 216 ++++++++++++-------------- theories/separation_axioms.v | 2 +- 4 files changed, 118 insertions(+), 121 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f9d3a218c..f3151abe6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,7 +88,7 @@ `wedge_compact`, `wedge_connected`. - in `boolp.`: - + lemma `existT_inj` + + lemma `existT_inj2` - in file `order_topology.v` + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and `max_fun_continuous`. @@ -109,6 +109,9 @@ `wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and `wedge_fun_joint_continuous`. +- in `boolp.v`: + + lemmas `existT_inj1`, `surjective_existT` + ### Changed - in file `normedtype.v`, diff --git a/classical/boolp.v b/classical/boolp.v index 5f63c4e63..f1ece5aa2 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -88,13 +88,21 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a. by apply: cid; case: PQA => x; exists x. Qed. -Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) : - existT P p x = existT P p y -> x = y. +Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) : + existT P x Px = existT P y Py -> x = y. +Proof. by case. Qed. + +Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) : + existT P x Px1 = existT P x Px2 -> Px1 = Px2. Proof. -apply: Eqdep_dec.inj_pair2_eq_dec => a b. -by have [|/eqP] := eqVneq a b; [left|right]. +apply: Eqdep_dec.inj_pair2_eq_dec => y z. +by have [|/eqP] := eqVneq y z; [left|right]. Qed. +Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}): + existT [eta P] (projT1 p) (projT2 p) = p. +Proof. by case: p. Qed. + Record mextensionality := { _ : forall (P Q : Prop), (P <-> Q) -> (P = Q); _ : forall {T U : Type} (f g : T -> U), diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 5b113e234..d39fddba0 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. -From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra fsbigop. -From mathcomp Require Import reals signed topology separation_axioms function_spaces. -Require Import EqdepFacts. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import separation_axioms function_spaces. (**md**************************************************************************) (* # wedge sum for sigT *) @@ -25,9 +24,8 @@ Require Import EqdepFacts. (* wedge_prod == the mapping from the wedge as a quotient of sums to *) (* the wedge as a subspace of the product topology. *) (* It's an embedding when the index is finite. *) -(* *) -(* *) (* ``` *) +(* *) (* The type `wedge p0` is endowed with the structures of: *) (* - topology via `quotient_topology` *) (* - quotient *) @@ -116,14 +114,14 @@ have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). rewrite eqEsubset; split => x /=. by move=> Ux; exists i => //; exists x. case=> j _ /= [] y Uy /eqmodP /predU1P[R|]. - have E : j = i by move: R; exact: eq_sigT_fst. - by rewrite -E in x R *; rewrite -(existT_inj R). + have E : j = i by move: R; apply: existT_inj1. + by rewrite -E in x R *; rewrite -(existT_inj2 R). case/andP => /eqP/= + /eqP -> => yj. by rewrite yj (wedge_liftE x y) in Uy. congr open; rewrite eqEsubset; split => /= z. by case=> i _ /= [x] Ux <-. move=> Uz; exists (projT1 (repr z)) => //=. -by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK. +by exists (projT2 (repr z)); rewrite /wedge_lift /= surjective_existT reprK. Qed. Lemma wedge_point_nbhs i0 : @@ -143,7 +141,7 @@ exists W; split. - apply/wedge_openP => i; rewrite /W; have [+ Vpj _] := projT2 (V_ i). congr (_ _); rewrite eqEsubset; split => z; first by move=> Viz; exists i. case => j _ /= [] w /= svw /eqmodP /predU1P[[E]|]. - by rewrite E in w svw * => R; rewrite -(existT_inj R). + by rewrite E in w svw * => R; rewrite -(existT_inj2 R). by case/andP => /eqP /= _ /eqP ->. - by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). - by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. @@ -167,7 +165,7 @@ Qed. Lemma wedgeTE : \bigcup_i (@wedge_lift i) @` setT = [set: wedge]. Proof. rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. -by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta. +by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= surjective_existT. Qed. Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> @@ -194,65 +192,62 @@ move=> i ? /=; apply: connected_continuous_connected => //. exact/continuous_subspaceT/wedge_lift_continuous. Qed. -Definition wedge_fun {Z : Type} (f : forall i, X i -> Z) : wedge -> Z := +Definition wedge_fun {Z : Type} (f : forall i, X i -> Z) : wedge -> Z := sigT_fun f \o repr. Lemma wedge_fun_continuous {Z : topologicalType} (f : forall i, X i -> Z) : - (forall i, continuous (f i)) -> - (forall i j, f i (p0 i) = f j (p0 j)) -> + (forall i, continuous (f i)) -> (forall i j, f i (p0 i) = f j (p0 j)) -> continuous (wedge_fun f). Proof. move=> cf fE; apply: repr_comp_continuous; first exact: sigT_continuous. -move=> a b /eqP/eqmodP /orP [ /eqP -> // | /andP [/eqP +] /eqP +]. -by rewrite /sigT_fun /= => -> ->; exact/eqP/fE. +move=> a b /eqP/eqmodP /predU1P[-> //|/andP[/eqP + /eqP +]]. +by rewrite /sigT_fun /= => -> ->; exact/eqP. Qed. -Lemma wedge_lift_funE {Z : Type} (f : forall i, X i -> Z) i0 (a : X i0): +Lemma wedge_lift_funE {Z : Type} (f : forall i, X i -> Z) i0 (a : X i0): (forall i j, f i (p0 i) = f j (p0 j)) -> wedge_fun f (wedge_lift a) = f i0 a. -Proof. +Proof. move=> fE. rewrite /wedge_fun/= /sigT_fun /=; case: piP => z /= /eqmodP. -by case/orP => [/eqP <- // | /andP [/eqP /= ->] /eqP ->]; apply: fE. +by move/predU1P => [<- //|/andP[/= /eqP -> /eqP ->]]. Qed. Lemma wedge_fun_comp {Z1 Z2 : Type} (h : Z1 -> Z2) (f : forall i, X i -> Z1) : h \o wedge_fun f = wedge_fun (fun i => h \o f i). -Proof. by apply/funext => z. Qed. +Proof. exact/funext. Qed. (* The wedge maps into the product \bigcup_i [x | x j = p0 j when j != i] - + For the box topology, it's an embedding. But more practically, - since the box and product agree when `I` is finite, + since the box and product agree when `I` is finite, we get that the finite wedge embeds into the finite product. *) Section wedge_as_product. -Definition wedge_prod : wedge -> prod_topology X := - wedge_fun (fun i x => dfwith (p0) i x). + +Definition wedge_prod : wedge -> prod_topology X := wedge_fun (dfwith p0). Lemma wedge_prod_pointE (i j : I) : dfwith p0 i (p0 i) = dfwith p0 j (p0 j). Proof. apply: functional_extensionality_dep => k /=. -case: dfwithP; first case: dfwithP => //. -by move=> i1 iNi1; case: dfwithP => //. +by case: dfwithP => [|*]; case: dfwithP. Qed. Lemma wedge_prod_inj : injective wedge_prod. Proof. -have ? := wedge_prod_pointE. -move=> a b; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). -case Ea : (repr a)=> [i x]; case Eb : (repr b) => [j y]. -rewrite /wedge_prod /= ?wedge_lift_funE //. -move=> dfij; apply/eqmodP/orP. -case: (pselect (i = j)) => E. - destruct E; left; apply/eqP; congr(_ _). +have dfwithp0 := wedge_prod_pointE. +move=> a b; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). +move Ea : (repr a)=> [i x]; move Eb : (repr b) => [j y]. +rewrite /wedge_prod !wedge_lift_funE//= => dfij; apply/eqmodP/orP. +have [E|E /=] := eqVneq i j. + rewrite -{}E in x y Ea Eb dfij *; left; apply/eqP; congr existT. have : dfwith p0 i x i = dfwith p0 i y i by rewrite dfij. - by rewrite ?dfwithin. -right => /=; apply/andP; split; apply/eqP. - have : dfwith p0 i x i = dfwith p0 j y i by rewrite dfij. - by rewrite dfwithin => ->; rewrite dfwithout // eq_sym; apply/eqP. -have : dfwith p0 i x j = dfwith p0 j y j by rewrite dfij. -by rewrite dfwithin => <-; rewrite dfwithout //; apply/eqP. + by rewrite !dfwithin. +right; apply/andP; split; apply/eqP. +- have : dfwith p0 i x i = dfwith p0 j y i by rewrite dfij. + by rewrite dfwithin => ->; rewrite dfwithout // eq_sym. +- have : dfwith p0 i x j = dfwith p0 j y j by rewrite dfij. + by rewrite dfwithin => <-; rewrite dfwithout. Qed. Lemma wedge_prod_continuous : continuous wedge_prod. @@ -262,121 +257,112 @@ exact: dfwith_continuous. Qed. Lemma wedge_prod_open (x : wedge) (A : set wedge) : - finite_set [set: I] -> + finite_set [set: I] -> (forall i, closed [set p0 i]) -> - nbhs x A -> + nbhs x A -> @nbhs _ (subspace (range wedge_prod)) (wedge_prod x) (wedge_prod @` A). Proof. -move=> fsetI clI; case: wedge_nbhs_specP => //. - move=> i0 bcA. - pose B_ i : set (subspace (range wedge_prod)) := - proj i @^-1` (@wedge_lift i@^-1` A). - have /finite_fsetP [fI fIE] := fsetI. - have : (\bigcap_(i in [set` fI]) B_ i) `&` range wedge_prod `<=` wedge_prod @` A. - move=> ? [] /[swap] [][] z _ <- /= Bwz; exists z => //. - have Iz : [set` fI] (projT1 (repr z)) by rewrite -fIE //. - have := Bwz _ Iz; congr(A _); rewrite /wedge_lift /= -[RHS]reprK. +move=> fsetI clI; case: wedge_nbhs_specP => [//|i0 bcA|i z zNp0 /= wNz]. + pose B_ i : set (subspace (range wedge_prod)) := + proj i @^-1` (@wedge_lift i @^-1` A). + have /finite_fsetP[fI fIE] := fsetI. + have /filterS : (\bigcap_(i in [set` fI]) B_ i) `&` range wedge_prod + `<=` wedge_prod @` A. + move=> _ [] /[swap] [] [z _] <- /= Bwz; exists z => //. + have /Bwz : [set` fI] (projT1 (repr z)) by rewrite -fIE. + congr (A _); rewrite /wedge_lift /= -[RHS]reprK. apply/eqmodP/orP; left; rewrite /proj /=. - by rewrite /wedge_prod /= /wedge_fun /sigT_fun /= dfwithin -sigT_eta. - move/filterS; apply. - apply/nbhs_subspace_ex; first by exists (wedge_lift (p0 i0)). + by rewrite /wedge_prod/= /wedge_fun /sigT_fun/= dfwithin surjective_existT. + apply; apply/nbhs_subspace_ex; first by exists (wedge_lift (p0 i0)). exists (\bigcap_(i in [set` fI]) B_ i); last by rewrite -setIA setIid. - apply: filter_bigI => i _. - rewrite /B_; apply: proj_continuous. - (have Ii : [set: I] i by done); have /= := bcA _ Ii; congr(nbhs _ _). - rewrite /proj /wedge_prod. - rewrite wedge_lift_funE; last exact: wedge_prod_pointE. - by case: dfwithP. -move=> i z zNp0 /= wNz. -rewrite [x in nbhs x _]/wedge_prod /= wedge_lift_funE; first last. + apply: filter_bigI => i _; rewrite /B_; apply: proj_continuous. + have /bcA : [set: I] i by []. + congr (nbhs _ _). + rewrite /proj /wedge_prod wedge_lift_funE; first by case: dfwithP. + exact: wedge_prod_pointE. +rewrite [x in nbhs x _]/wedge_prod /= wedge_lift_funE; first last. exact: wedge_prod_pointE. -have : wedge_prod @` (A `&` (@wedge_lift i @` ~`[set p0 i])) `<=` wedge_prod @` A. +have : wedge_prod @` (A `&` (@wedge_lift i @` ~`[set p0 i])) + `<=` wedge_prod @` A. by move=> ? [] ? [] + /= [w] wpi => /[swap] <- Aw <-; exists (wedge_lift w). -move/filterS; apply; apply/nbhs_subspace_ex. +move/filterS; apply; apply/nbhs_subspace_ex. exists (wedge_lift z) => //. by rewrite /wedge_prod wedge_lift_funE //; exact: wedge_prod_pointE. -exists (proj i @^-1` (@wedge_lift i @^-1` (A `&` (@wedge_lift i @` ~`[set p0 i])))). +exists (proj i @^-1` (@wedge_lift i @^-1` + (A `&` (@wedge_lift i @` ~`[set p0 i])))). apply/ proj_continuous; rewrite /proj dfwithin preimage_setI; apply: filterI. exact: wNz. have /filterS := @preimage_image _ _ (@wedge_lift i) (~` [set p0 i]). - apply; apply: open_nbhs_nbhs; split; first exact: closed_openC. - by apply/eqP. -rewrite eqEsubset; split => // ?; case => /[swap] [][] r _ <- /=. - case => ? /[swap] /wedge_prod_inj -> [+ [e /[swap]]] => /[swap]. + by apply; apply: open_nbhs_nbhs; split; [exact: closed_openC|exact/eqP]. +rewrite eqEsubset; split => // prodX; case => /[swap] [][] r _ <- /=. + case => _ /[swap] /wedge_prod_inj -> [+ [e /[swap]]] => /[swap]. move=> <- Awe eNpi; rewrite /proj /wedge_prod /=. - rewrite wedge_lift_funE; last by exact: wedge_prod_pointE. - rewrite dfwithin; split => //; first by (split => //; exists e). + rewrite wedge_lift_funE; last exact: wedge_prod_pointE. + rewrite dfwithin; split => //; first by split => //; exists e. exists (wedge_lift e) => //. by rewrite wedge_lift_funE //; exact: wedge_prod_pointE. case=> /[swap] [][y] yNpi E Ay. -case : (pselect (i = (projT1 (repr r)))); first last. - move=> R; move: yNpi; apply: absurd. - move: E; rewrite /proj/wedge_prod /wedge_fun /=/sigT_fun /=. - rewrite dfwithout //; last by rewrite eq_sym; apply/eqP. - case/eqmodP/orP; last by case/andP => /= /eqP E. - move=> /eqP => E. - have := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ E; apply. - by move=> a b; case: (pselect (a = b)) => ?; [left | right]. -move=> riE; split; exists (wedge_lift y) => //. -- by split; [rewrite E | exists y]. -- congr (wedge_prod _); rewrite E. +have [riE|R] := eqVneq i (projT1 (repr r)); last first. + apply: absurd yNpi. + move: E; rewrite /proj/wedge_prod /wedge_fun /=/sigT_fun /=. + rewrite dfwithout //; last by rewrite eq_sym. + by case/eqmodP/orP => [/eqP E|/andP[/= /eqP//]]; exact: (existT_inj2 E). +split; exists (wedge_lift y); [by split; [rewrite E | exists y]| |by []|]. +- congr wedge_prod; rewrite E. rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. - by rewrite riE dfwithin /wedge_lift /= -sigT_eta reprK. -- congr(wedge_prod _); rewrite E . + by rewrite riE dfwithin /wedge_lift /= surjective_existT reprK. +- congr wedge_prod; rewrite E. rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. - by rewrite riE dfwithin /wedge_lift /= -sigT_eta reprK. + by rewrite riE dfwithin /wedge_lift /= surjective_existT reprK. Qed. + End wedge_as_product. -Lemma wedge_hausdorff : - (forall i, hausdorff_space (X i)) -> - hausdorff_space wedge. +Lemma wedge_hausdorff : + (forall i, hausdorff_space (X i)) -> hausdorff_space wedge. Proof. -move=> /hausdorff_product hf => x y clxy. -apply: wedge_prod_inj; apply: hf => U V /wedge_prod_continuous. -move=> nU /wedge_prod_continuous nV; have := clxy _ _ nU nV. -by case => z [/=] ? ?; exists (wedge_prod z). +move=> /hausdorff_product hf x y clxy. +apply/wedge_prod_inj/hf => U V /wedge_prod_continuous nU. +move=> /wedge_prod_continuous nV; have := clxy _ _ nU nV. +by case => z [/= ? ?]; exists (wedge_prod z). Qed. -Lemma wedge_fun_joint_continuous (T R: topologicalType) +Lemma wedge_fun_joint_continuous (T R : topologicalType) (k : forall (x : I), T -> X x -> R): - (finite_set [set: I]) -> + finite_set [set: I] -> (forall x, closed [set p0 x]) -> (forall t x y, k x t (p0 x) = k y t (p0 y)) -> (forall x, continuous (uncurry (k x))) -> - continuous (uncurry (fun t => wedge_fun (k^~ t))). + continuous (uncurry (fun t => wedge_fun (k^~ t))). Proof. move=> Ifin clp0 kE kcts /= [t u] U. -case : (wedge_nbhs_specP u) => //. - move=> i0; rewrite /= wedge_lift_funE // => Ukp0. - have pq_ : forall x, {PQ : set T * set (X x) | - [/\nbhs (p0 x) PQ.2, nbhs t PQ.1 & PQ.1 `*` PQ.2 `<=` uncurry (k x) @^-1` U]}. - move=> x; apply: cid. +case : (wedge_nbhs_specP u) => [//|i0 /=|]. + rewrite wedge_lift_funE // => Ukp0. + have pq_ x : {PQ : set T * set (X x) | [/\ nbhs (p0 x) PQ.2, + nbhs t PQ.1 & PQ.1 `*` PQ.2 `<=` uncurry (k x) @^-1` U]}. + apply: cid. move: Ukp0; rewrite (@kE t i0 x). - rewrite -[k x ]uncurryK /curry=> /kcts; case; case=> P Q /= [Pt Qp0 pqU]. - by exists (P,Q) => //. - have UPQ : nbhs (wedge_lift (p0 i0)) ( - \bigcup_x (@wedge_lift x) @` (snd (projT1 (pq_ x)))). + rewrite -[k x ]uncurryK /curry=> /kcts[[P Q] [Pt Qp0 pqU]]. + by exists (P, Q). + have UPQ : nbhs (wedge_lift (p0 i0)) + (\bigcup_x (@wedge_lift x) @` (projT1 (pq_ x)).2). rewrite wedge_point_nbhs => r _. - by case: (projT2 (pq_ r)) => /filterS + ? ?; apply => z /= ?; by exists r. + by case: (projT2 (pq_ r)) => /filterS + ? ?; apply => z /= ?; exists r. have /finite_fsetP [fI fIE] := Ifin. - have UPt : nbhs t (\bigcap_(r in [set` fI]) (fst (projT1 (pq_ r)))). + have UPt : nbhs t (\bigcap_(r in [set` fI]) (projT1 (pq_ r)).1). by apply: filter_bigI => x ?; case: (projT2 (pq_ x)). near_simpl => /=; near=> t1 t2 => /=. - have [] // := near UPQ t2 => x _ [w /=] ? <-. + have [//|x _ [w /=] ? <-]:= near UPQ t2. rewrite wedge_lift_funE //. case: (projT2 (pq_ x)) => ? Npt /(_ (t1, w)) => /=; apply; split => //. - by have := near UPt t1; apply; rewrite // -fIE. -move: u => _ x u uNp0 /=; rewrite wedge_lift_funE //=. -rewrite -[k x]uncurryK /curry => /kcts; rewrite nbhs_simpl /=. -case; case => /= P Q [Pt Qu] PQU. + by apply: (near UPt t1) => //; rewrite -fIE. +move=> x {}u uNp0 /=; rewrite wedge_lift_funE //= -[k x]uncurryK /curry. +move/kcts; rewrite nbhs_simpl /= => -[[P Q] [Pt Qu] PQU]. have wQu : nbhs (wedge_lift u) ((@wedge_lift x) @` Q). - rewrite -wedge_lift_nbhs //=; move/filterS: Qu; apply. - by move=> z; exists z. + by rewrite -wedge_lift_nbhs //=; apply: filterS Qu => z; exists z. near_simpl; near=> t1 t2 => /=. -have [] // := near wQu t2 => l ? <-; rewrite wedge_lift_funE //. -apply: (PQU (t1,l)); split => //. -exact: (near Pt t1). +have [//|l ? <-] := near wQu t2; rewrite wedge_lift_funE//. +by apply: (PQU (t1,l)); split => //; exact: (near Pt t1). Unshelve. all: by end_near. Qed. End wedge. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index afd1f4ad6..c136e2bfd 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1139,7 +1139,7 @@ rewrite {}ji {j} in x y cl *. congr existT; apply: hX => U V Ux Vy. have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. -by rewrite -(existT_inj lr). +by rewrite -(existT_inj2 lr). Qed. End sigT_separations.