add existT_inj, shorten

CHANGELOG_UNRELEASED.md

@@ -78,6 +78,9 @@
     `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`,
     `wedge_compact`, `wedge_connected`.
 
+- in `boolp.`:
+  + lemma `existT_inj`
+
 ### Changed
 
 - in file `normedtype.v`,

classical/boolp.v

@@ -88,6 +88,13 @@ 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.
+Proof.
+apply: Eqdep_dec.inj_pair2_eq_dec => a b.
+by have [|/eqP] := eqVneq a b; [left|right].
+Qed.
+
 Record mextensionality := {
   _ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
   _ : forall {T U : Type} (f g : T -> U),

theories/homotopy_theory/homotopy.v

@@ -1,2 +1,2 @@
-
-From mathcomp Require Export wedge_sigT.
+(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Export wedge_sigT.

theories/homotopy_theory/wedge_sigT.v

@@ -1,3 +1,4 @@
+(* 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.
@@ -11,14 +12,14 @@ Require Import EqdepFacts.
 (* at a single point. It's classicaly used in the proof that every free group *)
 (* is a fundamental group of some space. We also will use it as part of our   *)
 (* construction of paths and path concatenation.                              *)
-(*                                                                            *)
+(* ```                                                                        *)
 (*    wedge_rel p0 x y == x and y are equal, or they are (p0 i) and           *)
-(*                        (p0 j) for some i and j.                            *)
+(*                        (p0 j) for some i and j                             *)
 (*            wedge p0 == the quotient of {i : X i} along `wedge_rel p0`      *)
 (*            wedgei i == the lifting of elements of (X i) into the wedge     *)
 (*           pwedge p0 == the wedge of ptopologicalTypes at their designated  *)
 (*                        point                                               *)
-(*                                                                            *)
+(* ```                                                                        *)
 (* The type `wedge p0` is endowed with the structures of:                     *)
 (* - topology via `quotient_topology`                                         *)
 (* - quotient                                                                 *)
@@ -40,117 +41,107 @@ Local Open Scope quotient_scope.
 
 Section wedge.
 Context {I : choiceType} (X : I -> topologicalType) (p0 : forall i, X i).
+Implicit Types i : I.
 
-Let wedge_rel' (a b : {i & X i}) := 
+Let wedge_rel' (a b : {i & X i}) :=
   (a == b) || ((projT2 a == p0 _) && (projT2 b == p0 _)).
 
 Local Lemma wedge_rel_refl : reflexive wedge_rel'.
 Proof. by move=> ?; rewrite /wedge_rel' eqxx. Qed.
 
 Local Lemma wedge_rel_sym : symmetric wedge_rel'.
-Proof. move=> a b.
-suff : (is_true (wedge_rel' a b) <-> is_true (wedge_rel' b a)).
-  case: (wedge_rel' a b) => //; case: (wedge_rel' b a) => // [].
-    by case=> ->.
-  by case=> _ ->.
-by split; rewrite /wedge_rel'=> /orP [/eqP -> // /[!eqxx] //|] /andP [] /eqP ->;
-  move=> /eqP ->; rewrite ?eqxx /= orbT.
+Proof.
+by move=> a b; apply/is_true_inj/propext; rewrite /wedge_rel'; split;
+  rewrite (eq_sym b) andbC.
 Qed.
 
 Local Lemma wedge_rel_trans : transitive wedge_rel'.
-Proof. 
-move=> a b c /orP [/eqP -> //|] + /orP [ /eqP <- // |].
-rewrite /wedge_rel'; case/andP=> /eqP -> /eqP <- /andP [] /eqP _ ->.
-by apply/orP; right; rewrite eqxx.
+Proof.
+move=> a b c /predU1P[-> //|] + /predU1P[<- //|]; rewrite /wedge_rel'.
+by move=> /andP[/eqP -> /eqP <-] /andP[_ /eqP <-]; rewrite !eqxx orbC.
 Qed.
 
 Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans.
 Global Opaque wedge_rel.
 
 Definition wedge := {eq_quot wedge_rel}.
-Definition wedgei (i : I) : X i -> wedge := \pi_wedge \o (existT X i).
+Definition wedgei (i : I) : X i -> wedge := \pi_wedge \o existT X i.
 
 HB.instance Definition _ := Topological.copy wedge (quotient_topology wedge).
 HB.instance Definition _ := Quotient.on wedge.
 Global Opaque wedge.
 
-Lemma wedgei_continuous (i : I) : continuous (@wedgei i).
+Lemma wedgei_continuous i : continuous (@wedgei i).
 Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed.
 
-HB.instance Definition _ (i : I) := @isContinuous.Build _ _ 
-  (@wedgei i) (@wedgei_continuous i).
+HB.instance Definition _ i :=
+  @isContinuous.Build _ _ (@wedgei i) (@wedgei_continuous i).
 
-Lemma wedgei_nbhs (i : I) (x : X i) : 
+Lemma wedgei_nbhs i (x : X i) :
   closed [set p0 i] -> x != p0 _ -> (@wedgei i) @ x = nbhs (@wedgei _ x).
 Proof.
 move=> clx0 xNx0; rewrite eqEsubset; split => U; first last.
-  by move=> ?; apply: wedgei_continuous.
-rewrite ?nbhsE /=; case => V [oV Vx VU].
-exists ((@wedgei  i) @` (V `&` ~`[set p0 i])); first last.
-  by move=> ? /= [l] [Vl lx] <-; apply: VU.
-split; last by exists x => //; split => //=; apply/eqP.
+  by move=> ?; exact: wedgei_continuous.
+rewrite ?nbhsE /= => -[V [oV Vx VU]].
+exists (@wedgei i @` (V `&` ~` [set p0 i])); first last.
+  by move=> ? /= [l] [Vl lx] <-; exact: VU.
+split; last by exists x => //; split => //=; exact/eqP.
 rewrite /open /= /quotient_open /wedgei /=.
-suff -> : \pi_wedge @^-1` ((@wedgei i) @` (V `&` ~`[set p0 i])) = 
-          (existT X i) @` (V `&` ~`[set p0 i]).
+suff -> : \pi_wedge @^-1` (@wedgei i @` (V `&` ~`[set p0 i])) =
+          existT X i @` (V `&` ~` [set p0 i]).
   by apply: existT_open_map; apply: openI => //; exact: closed_openC.
 rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l.
-case/eqmodP/orP => [/eqP <- |]; first by exists l.
-by move=> /= /andP [/eqP]; move: lNx0 => /[swap] ->.  
+by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l.
 Qed.
 
 Lemma wedge_openP (U : set wedge) :
-  open U <-> (forall i, open (@wedgei i @^-1` U)).
+  open U <-> forall i, open (@wedgei i @^-1` U).
 Proof.
-split.
-  move=> oU i; apply: open_comp => // ? _.
-  by apply: continuous_comp => //; exact: pi_continuous.
-move=> oiU.
-have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U) )).
-  apply/sigT_openP => i; move: (oiU i); congr(open _). 
+split=> [oU i|oiU].
+  by apply: open_comp => // x _; exact: wedgei_continuous.
+have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U))).
+  apply/sigT_openP => i; move: (oiU i); congr open.
   rewrite eqEsubset; split => x /=.
-    by move=> Ux; exists i => //; exists x => //.
-  case=> j _ /= [] y Uy /eqmodP /orP [/eqP R|].
-    have E : j = i by move: R; apply: eq_sigT_fst.
-    move: x R; rewrite -E => x R; move: Uy; congr(U (_ _)); move: R.
-    apply: Eqdep_dec.inj_pair2_eq_dec.
-    by move => p q; case: (pselect (p = q)) => ?; [left | right].
-  case/andP=> /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr(_ _).
-  by apply/eqmodP; apply/orP; right; rewrite ?eqxx.
-congr(open _); rewrite eqEsubset; split => /= z.
+    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.
+    rewrite -E in x R *; move: Uy; congr (U (_ _)).
+    exact: existT_inj R.
+  case/andP => /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr (_ _).
+  by apply/eqmodP/orP; right; rewrite !eqxx.
+congr open; rewrite eqEsubset; split => /= z.
   by case=> i _ /= [x] Ux <-.
-move=> Uz; exists (projT1 (repr z)) => //=. 
+move=> Uz; exists (projT1 (repr z)) => //=.
 by exists (projT2 (repr z)); rewrite /wedgei /= -?sigT_eta ?reprK.
 Qed.
 
-Lemma wedge_pointE i j : existT _ i (p0 i)  = existT _ j (p0 j)  %[mod wedge].
+Lemma wedge_pointE i j : existT _ i (p0 i)  = existT _ j (p0 j) %[mod wedge].
 Proof. by apply/eqmodP; apply/orP; right; rewrite ?eqxx. Qed.
 
-Lemma wedge_point_nbhs i0 : 
-  nbhs (wedgei (p0 i0)) = \bigcap_i ((@wedgei i) @ p0 i).
+Lemma wedge_point_nbhs i0 :
+  nbhs (wedgei (p0 i0)) = \bigcap_i (@wedgei i @ p0 i).
 Proof.
 rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl.
   case=> V [/= oV Vp] VU j _; apply: wedgei_continuous.
-  move/filterS: VU; apply => //; first exact: (@nbhs_filter wedge).
-  apply: open_nbhs_nbhs; split => //; move: Vp; congr( _ _).
+  apply: (filterS VU); first exact: (@nbhs_filter wedge).
+  apply: open_nbhs_nbhs; split => //; move: Vp; congr (_ _).
   by rewrite /wedgei /=; exact: wedge_pointE.
-move=> Uj; have V_ : forall i, {V : set (X i) |  
-    [/\ open V, V (p0 i) & V `<=` (@wedgei i) @^-1` U]}.
-  (move=> j; have Ij : [set: I] j by done); apply: cid.
-  by move: (Uj _ Ij); rewrite nbhsE /=; case=> B [? ? ?]; exists B.
+move=> Uj; have V_ : forall i, {V : set (X i) |
+    [/\ open V, V (p0 i) & V `<=` @wedgei i @^-1` U]}.
+  move=> j; apply: cid; have /Uj : [set: I] j by [].
+  by rewrite nbhsE /= => -[B [? ? ?]]; exists B.
 pose W := \bigcup_i (@wedgei i) @` (projT1 (V_ i)).
 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 /orP [/eqP [E]| ].
-    move: w svw; rewrite E => w svw R.
-    have <- // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ R.
-    by move=> a b; case: (pselect (a = b)) => ?; [left | right].
-  by case/andP=> /eqP /= _ /eqP ->.
+  case => j _ /= [] w /= svw /eqmodP /predU1P[[E]| ].
+    by rewrite E in w svw * => R; rewrite -(existT_inj R).
+  by case/andP => /eqP /= _ /eqP ->.
 - by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0).
-- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); apply.
+- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact.
 Qed.
 
-Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := 
+Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type :=
   | WedgeIsPoint i0 :
       wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i ((@wedgei i) @ p0 i))
   | WedgeNotPoint (i : I) (x : X i) of (x != p0 i):
@@ -159,41 +150,40 @@ Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type :=
 Lemma wedge_nbhs_specP (z : wedge) : (forall i, closed [set p0 i]) ->
   wedge_nbhs_spec z z (nbhs z).
 Proof.
-move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z).
-move=> i x; case: (pselect (x = p0 i)).
-  move=> ->; rewrite wedge_point_nbhs => /=; apply: WedgeIsPoint. 
-by move/eqP => xpi; rewrite /= -wedgei_nbhs //; apply: WedgeNotPoint.
+move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z) => i x.
+have [->|xpi] := eqVneq x (p0 i).
+  by rewrite wedge_point_nbhs => /=; exact: WedgeIsPoint.
+by rewrite /= -wedgei_nbhs //; exact: WedgeNotPoint.
 Qed.
 
 Lemma wedgeTE : \bigcup_i (@wedgei i) @` setT = [set: wedge].
-Proof. 
-rewrite -subTset=> z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //.
-by exists (projT2 (repr z)); rewrite // reprK /wedgei /= -sigT_eta reprK.
+Proof.
+rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //.
+by exists (projT2 (repr z)) => //; rewrite reprK /wedgei /= -sigT_eta reprK.
 Qed.
 
-Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> 
+Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) ->
   compact [set: wedge].
 Proof.
-move=> fsetI cptX.
-rewrite -wedgeTE -fsbig_setU //; apply: big_ind.
+move=> fsetI cptX; rewrite -wedgeTE -fsbig_setU //; apply: big_ind.
 - exact: compact0.
 - by move=> ? ? ? ?; exact: compactU.
 move=> i _; apply: continuous_compact; last exact: cptX.
-by apply: continuous_subspaceT; exact: wedgei_continuous.
+exact/continuous_subspaceT/wedgei_continuous.
 Qed.
 
-Lemma wedge_connected : (forall i, connected [set: X i]) -> 
+Lemma wedge_connected : (forall i, connected [set: X i]) ->
   connected [set: wedge].
 Proof.
-move=> ctdX; rewrite -wedgeTE. 
-case: (pselect ([set: I] !=set0)); first last.
-  move=> I0; have := @connected0 (wedge); congr (_ _). 
-  by rewrite eqEsubset; split => ? // [] x ?; move: I0; apply: absurd; exists x.
-case=> i0 Ii0; apply: bigcup_connected.
+move=> ctdX; rewrite -wedgeTE.
+have [I0|/set0P[i0 Ii0]] := eqVneq [set: I] set0.
+  rewrite [X in connected X](_ : _ = set0); first exact: connected0.
+  by rewrite I0 bigcup_set0.
+apply: bigcup_connected.
   exists (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //.
-  by rewrite /wedgei /=; apply/eqmodP; apply/orP; right; rewrite ?eqxx.
+  by apply/eqmodP/orP; right; rewrite !eqxx.
 move=> i ? /=; apply: connected_continuous_connected => //.
-by exact/continuous_subspaceT/wedgei_continuous.
+exact/continuous_subspaceT/wedgei_continuous.
 Qed.
 
 End wedge.

theories/separation_axioms.v

@@ -1114,12 +1114,11 @@ Lemma perfectTP_ex {T} : perfect_set [set: T] <->
   forall (U : set T), open U -> U !=set0 ->
   exists x y, [/\ U x, U y & x != y] .
 Proof.
-apply: iff_trans; first exact: perfectTP; split.
+apply: (iff_trans perfectTP); split.
   move=> nx1 U oU [] x Ux; exists x.
   have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1.
-  apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset.
-  (split => //; last by move=> ? ->); move=> y Uy; have  /not_and3P := Uyx y.
-  by case => // /negP; rewrite negbK => /eqP ->.
+  apply: contra_notP => /not_existsP/contrapT=> Uyx; rewrite eqEsubset.
+  by split => [y Uy|? ->//]; have /not_and3P[//|//|/negP/negPn/eqP] := Uyx y.
 move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
 by move=> y [] ? [->] -> /eqP.
 Qed.
@@ -1140,8 +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 => //.
-rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr.
-by move=> a b; exact: pselect.
+by rewrite -(existT_inj lr).
 Qed.
 
 End sigT_separations.