From c74949cfe1c804431fb8fd833be880c36a1fd633 Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Tue, 6 Aug 2024 17:05:50 +0200
Subject: [PATCH] Declare `DirectedSets.DS_set` as coercion

The coercion from `DirectedSets` to `Sortclass` makes some code easier
to write.
---
 theories/Topology/Compactness.v     | 14 +++++------
 theories/Topology/Completeness.v    |  2 +-
 theories/Topology/FiltersAndNets.v  |  6 ++---
 theories/Topology/MetricSpaces.v    |  8 +++----
 theories/Topology/Nets.v            | 36 ++++++++++++++---------------
 theories/Topology/ProductTopology.v |  8 +++----
 theories/Topology/RTopology.v       | 12 +++++-----
 theories/Topology/WeakTopology.v    | 12 +++++-----
 theories/ZornsLemma/DirectedSets.v  | 36 ++++++++++++++---------------
 9 files changed, 67 insertions(+), 67 deletions(-)

diff --git a/theories/Topology/Compactness.v b/theories/Topology/Compactness.v
index 53f1ffe2..f5164cea 100644
--- a/theories/Topology/Compactness.v
+++ b/theories/Topology/Compactness.v
@@ -299,7 +299,7 @@ Qed.
 
 Lemma compact_impl_net_cluster_point:
   forall X:TopologicalSpace, compact X ->
-    forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) ->
+    forall (I:DirectedSet) (x:Net I X), inhabited I ->
     exists x0:X, net_cluster_point x x0.
 Proof.
 intros.
@@ -311,7 +311,7 @@ apply H1.
 Qed.
 
 Lemma net_cluster_point_impl_compact: forall X:TopologicalSpace,
-  (forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) ->
+  (forall (I:DirectedSet) (x:Net I X), inhabited I ->
     exists x0:X, net_cluster_point x x0) ->
   compact X.
 Proof.
@@ -357,13 +357,13 @@ apply Extensionality_Ensembles; split; red; intros.
   apply closure_inflationary. assumption.
 }
 destruct (net_limits_determine_topology _ _ H2) as [I0 [y []]].
-pose (yS (i:DS_set I0) := exist (fun x:X => In S x) (y i) (H3 i)).
+pose (yS (i:I0) := exist (fun x:X => In S x) (y i) (H3 i)).
 assert (inhabited (SubspaceTopology S)).
 { destruct H1.
   constructor.
   now exists x0.
 }
-assert (inhabited (DS_set I0)) as HinhI0.
+assert (inhabited I0) as HinhI0.
 { red in H4.
   destruct (H4 Full_set) as [i0]; auto with topology.
   constructor.
@@ -380,14 +380,14 @@ apply net_cluster_point_impl_subnet_converges in H6.
 }
 destruct H6 as [J [y' [HySy' Hy']]].
 destruct HySy' as [h [Hh0 [Hh1 Hhy']]].
-assert (net_limit (fun j:DS_set J => y (h j)) x0).
+assert (net_limit (fun j:J => y (h j)) x0).
 { apply continuous_func_preserves_net_limits with
   (f:=subspace_inc S) (Y:=X) in Hy'.
   - cbn in Hy'.
     eapply net_limit_compat; eauto.
     intros ?; cbn. rewrite Hhy'. reflexivity.
   - apply continuous_func_continuous_everywhere, subspace_inc_continuous. }
-assert (net_limit (fun j:DS_set J => y (h j)) x).
+assert (net_limit (fun j:J => y (h j)) x).
 { apply subnet_limit with I0 y; trivial.
   exists h. now constructor. }
 assert (x = x0).
@@ -443,7 +443,7 @@ intros.
 apply net_cluster_point_impl_compact.
 intros.
 destruct (compact_impl_net_cluster_point _ H
-  _ (fun i:DS_set I => subspace_inc _ (x i))) as [x0]; trivial.
+  _ (fun i:I => subspace_inc _ (x i))) as [x0]; trivial.
 assert (In S x0).
 { rewrite <- (closure_fixes_closed S); trivial.
   eapply net_cluster_point_in_closure;
diff --git a/theories/Topology/Completeness.v b/theories/Topology/Completeness.v
index 79c69a00..c90c2f04 100644
--- a/theories/Topology/Completeness.v
+++ b/theories/Topology/Completeness.v
@@ -14,7 +14,7 @@ Definition cauchy (x:nat->X) : Prop :=
 Definition complete : Prop :=
   forall x:nat -> X, cauchy x ->
     exists x0 : X, forall eps:R,
-      eps > 0 -> for large i:DS_set nat_DS,
+      eps > 0 -> for large i:nat_DS,
       d x0 (x i) < eps.
 
 Lemma cauchy_impl_bounded (x : nat -> X) :
diff --git a/theories/Topology/FiltersAndNets.v b/theories/Topology/FiltersAndNets.v
index b309dde2..0be96ff8 100644
--- a/theories/Topology/FiltersAndNets.v
+++ b/theories/Topology/FiltersAndNets.v
@@ -7,10 +7,10 @@ Section net_tail_filter.
 Variable X:TopologicalSpace.
 Variable J:DirectedSet.
 Variable x:Net J X.
-Hypothesis J_nonempty: inhabited (DS_set J).
+Hypothesis J_nonempty: inhabited J.
 
-Definition net_tail (j:DS_set J) :=
-  Im [ i:DS_set J | DS_ord j i ] x.
+Definition net_tail (j:J) :=
+  Im [ i:J | DS_ord j i ] x.
 
 Definition tail_filter_basis : Family (point_set X) :=
   Im Full_set net_tail.
diff --git a/theories/Topology/MetricSpaces.v b/theories/Topology/MetricSpaces.v
index b400f588..21f0bcd6 100644
--- a/theories/Topology/MetricSpaces.v
+++ b/theories/Topology/MetricSpaces.v
@@ -287,7 +287,7 @@ Qed.
 Lemma metric_space_net_limit: forall (X:TopologicalSpace)
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
-  (forall eps:R, eps > 0 -> for large i:DS_set I, d x0 (x i) < eps) ->
+  (forall eps:R, eps > 0 -> for large i:I, d x0 (x i) < eps) ->
   net_limit x x0.
 Proof.
 intros.
@@ -306,7 +306,7 @@ Lemma metric_space_net_limit_converse: forall (X:TopologicalSpace)
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
     net_limit x x0 -> forall eps:R, eps > 0 ->
-                         for large i:DS_set I, d x0 (x i) < eps.
+                         for large i:I, d x0 (x i) < eps.
 Proof.
 intros.
 pose (U:=open_ball d x0 eps).
@@ -324,7 +324,7 @@ Lemma metric_space_net_cluster_point: forall (X:TopologicalSpace)
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
   (forall eps:R, eps > 0 ->
-     exists arbitrarily large i:DS_set I, d x0 (x i) < eps) ->
+     exists arbitrarily large i:I, d x0 (x i) < eps) ->
   net_cluster_point x x0.
 Proof.
 intros.
@@ -344,7 +344,7 @@ Lemma metric_space_net_cluster_point_converse: forall (X:TopologicalSpace)
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
     net_cluster_point x x0 -> forall eps:R, eps > 0 ->
-                exists arbitrarily large i:DS_set I, d x0 (x i) < eps.
+                exists arbitrarily large i:I, d x0 (x i) < eps.
 Proof.
 intros.
 pose (U:=open_ball d x0 eps).
diff --git a/theories/Topology/Nets.v b/theories/Topology/Nets.v
index e5b529b4..be04eaf8 100644
--- a/theories/Topology/Nets.v
+++ b/theories/Topology/Nets.v
@@ -4,18 +4,18 @@ From Topology Require Export TopologicalSpaces InteriorsClosures Continuity.
 Set Asymmetric Patterns.
 
 Definition Net (I : DirectedSet) (X : Type) : Type :=
-  DS_set I -> X.
+  I -> X.
 
 Definition Subnet {I : DirectedSet} {X : Type}
   (x : Net I X) {J : DirectedSet} (y : Net J X) : Prop :=
-  exists (h : DS_set J -> DS_set I),
+  exists (h : J -> I),
     (* [h] is monotonous *)
-    (forall j1 j2 : DS_set J,
+    (forall j1 j2 : J,
         DS_ord j1 j2 -> DS_ord (h j1) (h j2)) /\
-    (exists arbitrarily large i : DS_set I,
-      exists j : DS_set J, h j = i) /\
+    (exists arbitrarily large i : I,
+      exists j : J, h j = i) /\
     (* [y] is [x ∘ h] *)
-    (forall j : DS_set J,
+    (forall j : J,
         y j = x (h j)).
 
 Lemma Subnet_refl {I : DirectedSet} {X : Type} (x : Net I X) :
@@ -54,14 +54,14 @@ Variable X:TopologicalSpace.
 
 Definition net_limit (x:Net I X) (x0:X) : Prop :=
   forall U:Ensemble X, open U -> In U x0 ->
-  for large i:DS_set I, In U (x i).
+  for large i:I, In U (x i).
 
 Definition net_cluster_point (x:Net I X) (x0:X) : Prop :=
   forall U:Ensemble X, open U -> In U x0 ->
-  exists arbitrarily large i:DS_set I, In U (x i).
+  exists arbitrarily large i:I, In U (x i).
 
 Lemma net_limit_compat (x1 x2 : Net I X) (x : X) :
-  (forall i : DS_set I, x1 i = x2 i) ->
+  (forall i : I, x1 i = x2 i) ->
   net_limit x1 x -> net_limit x2 x.
 Proof.
   intros Hxx Hx1.
@@ -87,7 +87,7 @@ Qed.
 
 Lemma net_limit_in_closure: forall (S:Ensemble X)
   (x:Net I X) (x0:X),
-  (exists arbitrarily large i:DS_set I, In S (x i)) ->
+  (exists arbitrarily large i:I, In S (x i)) ->
   net_limit x x0 -> In (closure S) x0.
 Proof.
 intros.
@@ -105,7 +105,7 @@ Qed.
 
 Lemma net_cluster_point_in_closure: forall (S:Ensemble X)
   (x:Net I X) (x0:X),
-  (for large i:DS_set I, In S (x i)) ->
+  (for large i:I, In S (x i)) ->
   net_cluster_point x x0 -> In (closure S) x0.
 Proof.
 intros.
@@ -192,7 +192,7 @@ Lemma net_limits_determine_topology:
   forall {X:TopologicalSpace} (S:Ensemble X)
   (x0:X), In (closure S) x0 ->
   exists I:DirectedSet, exists x:Net I X,
-  (forall i:DS_set I, In S (x i)) /\ net_limit x x0.
+  (forall i:I, In S (x i)) /\ net_limit x x0.
 Proof.
 intros.
 assert (forall U:Ensemble X, open U -> In U x0 ->
@@ -273,7 +273,7 @@ Variable f:X -> Y.
 Lemma continuous_func_preserves_net_limits:
   forall {I:DirectedSet} (x:Net I X) (x0:X),
     net_limit x x0 -> continuous_at f x0 ->
-    net_limit (fun i:DS_set I => f (x i)) (f x0).
+    net_limit (fun i:I => f (x i)) (f x0).
 Proof.
 intros.
 red. intros V ? ?.
@@ -283,7 +283,7 @@ assert (neighborhood V (f x0)).
 destruct (H0 V H3) as [U [? ?]].
 destruct H4.
 pose proof (H U H4 H6).
-apply eventually_impl_base with (fun i:DS_set I => In U (x i));
+apply eventually_impl_base with (fun i:I => In U (x i));
   trivial.
 intros.
 assert (In (inverse_image f V) (x i)) by auto with sets.
@@ -293,7 +293,7 @@ Qed.
 Lemma func_preserving_net_limits_is_continuous:
   forall x0:X,
   (forall (I:DirectedSet) (x:Net I X),
-    net_limit x x0 -> net_limit (fun i:DS_set I => f (x i)) (f x0))
+    net_limit x x0 -> net_limit (fun i:I => f (x i)) (f x0))
   -> continuous_at f x0.
 Proof.
 intros.
@@ -355,10 +355,10 @@ Section cluster_point_subnet.
 
 Variable x0:X.
 Hypothesis x0_cluster_point: net_cluster_point x x0.
-Hypothesis I_nonempty: inhabited (DS_set I).
+Hypothesis I_nonempty: inhabited I.
 
 Record cluster_point_subnet_DS_set : Type := {
-  cps_i:DS_set I;
+  cps_i:I;
   cps_U:Ensemble X;
   cps_U_open_neigh: open_neighborhood cps_U x0;
   cps_xi_in_U: In cps_U (x cps_i)
@@ -427,7 +427,7 @@ Defined.
 
 Definition cluster_point_subnet : Net
   cluster_point_subnet_DS X :=
-  fun (iU:DS_set cluster_point_subnet_DS) =>
+  fun (iU : cluster_point_subnet_DS) =>
   x (cps_i iU).
 
 Lemma cluster_point_subnet_is_subnet:
diff --git a/theories/Topology/ProductTopology.v b/theories/Topology/ProductTopology.v
index 8da0528f..5357acb0 100644
--- a/theories/Topology/ProductTopology.v
+++ b/theories/Topology/ProductTopology.v
@@ -24,8 +24,8 @@ Qed.
 
 Lemma product_net_limit: forall (I:DirectedSet)
   (x:Net I ProductTopology) (x0:ProductTopology),
-  inhabited (DS_set I) ->
-  (forall a:A, net_limit (fun i:DS_set I => x i a) (x0 a)) ->
+  inhabited I ->
+  (forall a:A, net_limit (fun i:I => x i a) (x0 a)) ->
   net_limit x x0.
 Proof.
 intros.
@@ -215,8 +215,8 @@ apply net_limit_in_projections_impl_net_limit_in_weak_topology.
       now destruct (x0 i).
   + unfold product_space_proj.
     simpl.
-    replace (fun i:DS_set I => prod2_conv2 (x0 i) twoT_2) with
-      (fun i:DS_set I => snd (x0 i)).
+    replace (fun i:I => prod2_conv2 (x0 i) twoT_2) with
+      (fun i:I => snd (x0 i)).
     * now apply net_limit_in_weak_topology_impl_net_limit_in_projections
         with (a:=twoT_2) in H.
     * extensionality i.
diff --git a/theories/Topology/RTopology.v b/theories/Topology/RTopology.v
index 9c032903..b58dfa74 100644
--- a/theories/Topology/RTopology.v
+++ b/theories/Topology/RTopology.v
@@ -173,12 +173,12 @@ exists R_metric.
 Qed.
 
 Lemma bounded_real_net_has_cluster_point: forall (I:DirectedSet)
-  (x:Net I RTop) (a b:R), (forall i:DS_set I, a <= x i <= b) ->
+  (x:Net I RTop) (a b:R), (forall i:I, a <= x i <= b) ->
   exists x0:RTop, net_cluster_point x x0.
 Proof.
 (* idea: the liminf is a cluster point *)
 intros.
-destruct (classic (inhabited (DS_set I))) as [Hinh|Hempty].
+destruct (classic (inhabited I)) as [Hinh|Hempty].
 2: {
   exists a.
   red. intros.
@@ -186,8 +186,8 @@ destruct (classic (inhabited (DS_set I))) as [Hinh|Hempty].
   contradiction Hempty.
   now exists.
 }
-assert (forall i:DS_set I, { y:R | is_glb
-                           (Im [ j:DS_set I | DS_ord i j ] x) y }).
+assert (forall i:I, { y:R | is_glb
+                         (Im [ j:I | DS_ord i j ] x) y }).
 { intro.
   apply inf.
   - exists a.
@@ -221,7 +221,7 @@ assert ({ x0:R | is_lub (Im Full_set (fun i => proj1_sig (X i))) x0 }).
 }
 destruct H0 as [x0].
 exists x0.
-assert (forall i j:DS_set I,
+assert (forall i j:I,
            DS_ord i j -> proj1_sig (X i) <= proj1_sig (X j)).
 { intros.
   destruct (X i0), (X j).
@@ -283,7 +283,7 @@ Proof.
 intros a b Hbound.
 apply net_cluster_point_impl_compact.
 intros.
-pose (y := fun i:DS_set I => proj1_sig (x i)).
+pose (y := fun i:I => proj1_sig (x i)).
 destruct (bounded_real_net_has_cluster_point _ y a b).
 { intros.
   unfold y.
diff --git a/theories/Topology/WeakTopology.v b/theories/Topology/WeakTopology.v
index d6a7a877..db4f503d 100644
--- a/theories/Topology/WeakTopology.v
+++ b/theories/Topology/WeakTopology.v
@@ -71,13 +71,13 @@ Qed.
 Section WeakTopology_and_Nets.
 
 Variable I:DirectedSet.
-Hypothesis I_nonempty: inhabited (DS_set I).
+Hypothesis I_nonempty: inhabited I.
 Variable x:Net I WeakTopology.
 Variable x0:X.
 
 Lemma net_limit_in_weak_topology_impl_net_limit_in_projections :
   net_limit x x0 ->
-  forall a:A, net_limit (fun i:DS_set I => (f a) (x i)) ((f a) x0).
+  forall a:A, net_limit (fun i:I => (f a) (x i)) ((f a) x0).
 Proof.
 intros.
 apply continuous_func_preserves_net_limits; trivial.
@@ -86,7 +86,7 @@ apply weak_topology_makes_continuous_funcs.
 Qed.
 
 Lemma net_limit_in_projections_impl_net_limit_in_weak_topology :
-  (forall a:A, net_limit (fun i:DS_set I => (f a) (x i))
+  (forall a:A, net_limit (fun i:I => (f a) (x i))
                          ((f a) x0)) ->
   net_limit x x0.
 Proof.
@@ -96,19 +96,19 @@ assert (@open_basis WeakTopology
         (finite_intersections weak_topology_subbasis)).
 { apply Build_TopologicalSpace_from_open_basis_basis. }
 destruct (open_basis_cover _ H2 x0 U) as [V [? [? ?]]]; trivial.
-assert (for large i:DS_set I, In V (x i)).
+assert (for large i:I, In V (x i)).
 { clear H4.
   induction H3.
   - destruct I_nonempty.
     exists X0; constructor.
   - destruct H3.
     destruct H5.
-    apply eventually_impl_base with (fun i:DS_set I => In V (f a (x i))).
+    apply eventually_impl_base with (fun i:I => In V (f a (x i))).
     + intros.
       constructor; trivial.
     + apply H; trivial.
   - apply eventually_impl_base with
-        (fun i:DS_set I => In U0 (x i) /\ In V (x i)).
+        (fun i:I => In U0 (x i) /\ In V (x i)).
     + intros.
       destruct H6.
       constructor; trivial.
diff --git a/theories/ZornsLemma/DirectedSets.v b/theories/ZornsLemma/DirectedSets.v
index 682886bb..3c5e6a26 100644
--- a/theories/ZornsLemma/DirectedSets.v
+++ b/theories/ZornsLemma/DirectedSets.v
@@ -5,7 +5,7 @@ From Coq Require Import Arith.
 From Coq Require Import Lia.
 
 Record DirectedSet := {
-  DS_set : Type;
+  DS_set :> Type;
   DS_ord : relation DS_set;
   DS_ord_cond : preorder DS_ord;
   DS_join_cond : forall i j:DS_set, exists k:DS_set,
@@ -20,13 +20,13 @@ Section for_large.
 
 Context {I : DirectedSet}.
 
-Definition eventually (P : DS_set I -> Prop) : Prop :=
-  exists i:DS_set I, forall j:DS_set I,
+Definition eventually (P : I -> Prop) : Prop :=
+  exists i : I, forall j : I,
   DS_ord i j -> P j.
 
-Lemma eventually_and: forall (P Q: DS_set I -> Prop),
+Lemma eventually_and: forall (P Q : I -> Prop),
   eventually P -> eventually Q ->
-  eventually (fun i:DS_set I => P i /\ Q i).
+  eventually (fun i : I => P i /\ Q i).
 Proof.
 intros.
 destruct H, H0.
@@ -39,8 +39,8 @@ intros; split;
   apply DS_ord_cond.
 Qed.
 
-Lemma eventually_impl_base: forall (P Q: DS_set I -> Prop),
-  (forall i:DS_set I, P i -> Q i) ->
+Lemma eventually_impl_base: forall (P Q : I -> Prop),
+  (forall i : I, P i -> Q i) ->
   eventually P -> eventually Q.
 Proof.
 intros.
@@ -50,23 +50,23 @@ intros.
 auto.
 Qed.
 
-Lemma eventually_impl: forall (P Q: DS_set I -> Prop),
-  eventually P -> eventually (fun i:DS_set I => P i -> Q i) ->
+Lemma eventually_impl: forall (P Q : I -> Prop),
+  eventually P -> eventually (fun i : I => P i -> Q i) ->
   eventually Q.
 Proof.
 intros.
-apply eventually_impl_base with (P := fun (i:DS_set I) =>
+apply eventually_impl_base with (P := fun (i : I) =>
   P i /\ (P i -> Q i)).
 - tauto.
 - now apply eventually_and.
 Qed.
 
-Definition exists_arbitrarily_large (P: DS_set I -> Prop) :=
-  forall i:DS_set I, exists j:DS_set I,
+Definition exists_arbitrarily_large (P : I -> Prop) :=
+  forall i : I, exists j : I,
   DS_ord i j /\ P j.
 
-Lemma exists_arbitrarily_large_all (P : DS_set I -> Prop) :
-  (forall i : DS_set I, P i) ->
+Lemma exists_arbitrarily_large_all (P : I -> Prop) :
+  (forall i : I, P i) ->
   exists_arbitrarily_large P.
 Proof.
   intros HP i.
@@ -74,9 +74,9 @@ Proof.
   apply DS_ord_cond.
 Qed.
 
-Lemma not_eal_eventually_not: forall (P: DS_set I -> Prop),
+Lemma not_eal_eventually_not: forall (P : I -> Prop),
   ~ exists_arbitrarily_large P ->
-  eventually (fun i:DS_set I => ~ P i).
+  eventually (fun i : I => ~ P i).
 Proof.
 intros.
 apply not_all_ex_not in H.
@@ -88,9 +88,9 @@ contradiction H.
 exists j; split; trivial.
 Qed.
 
-Lemma not_eventually_eal_not: forall (P: DS_set I -> Prop),
+Lemma not_eventually_eal_not: forall (P : I -> Prop),
   ~ eventually P ->
-  exists_arbitrarily_large (fun i:DS_set I => ~ P i).
+  exists_arbitrarily_large (fun i : I => ~ P i).
 Proof.
 intros.
 red; intros.