From 49d896b759666fec3e58b40058e392d786142fa2 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Sat, 9 Nov 2024 14:07:39 -0500
Subject: [PATCH] more idiomatic naming

---
 CHANGELOG_UNRELEASED.md                     |  6 ++++--
 classical/mathcomp_extra.v                  | 12 ++++++------
 theories/topology_theory/product_topology.v |  4 ++--
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7b3f64650..174346d49 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -73,9 +73,11 @@
   + lemma `cvgr_dnbhsP`
   + new definitions `left_assoc_prod`, and `right_assoc_prod`.
   + new lemmas `left_assoc_prodK`, `right_assoc_prodK`, and `swapK`.
+  + new definitions `prodA`, and `prodAr`.
+  + new lemmas `prodAK`, `prodArK`, and `swapK`.
 - in file `product_topology.v`,
-  + new lemmas `swap_continuous`, `left_assoc_prod_continuous`, and 
-    `right_assoc_prod_continuous`.
+  + new lemmas `swap_continuous`, `prodA_continuous`, and 
+    `prodAr_continuous`.
 
 ### Changed
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 86aaf9a0b..f0ecf3733 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -18,8 +18,8 @@ From mathcomp Require Import finset interval.
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
 (*             sigT_fun f := lifts a family of functions f into a function on *)
 (*                           the dependent sum                                *)
-(*      left_assoc_prod x := sends (X * Y) * Z to X * (Y * Z)                 *)
-(*     right_assoc_prod x := sends X * (Y * Z) to (X * Y) * Z                 *)
+(*                prodA x := sends (X * Y) * Z to X * (Y * Z)                 *)
+(*               prodAr x := sends X * (Y * Z) to (X * Y) * Z                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -380,16 +380,16 @@ Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).
 Section reassociate_products.
 Context {X Y Z : Type}.
 
-Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) :=
+Definition prodA (xyz : (X * Y) * Z) : X * (Y * Z) :=
   (xyz.1.1, (xyz.1.2, xyz.2)).
 
-Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z :=
+Definition prodAr (xyz : X * (Y * Z)) : (X * Y) * Z :=
   ((xyz.1, xyz.2.1), xyz.2.2).
 
-Lemma left_assoc_prodK : cancel left_assoc_prod right_assoc_prod.
+Lemma prodAK : cancel prodA prodAr.
 Proof. by case; case. Qed.
 
-Lemma right_assoc_prodK : cancel right_assoc_prod left_assoc_prod.
+Lemma prodArK : cancel prodAr prodA.
 Proof. by case => ? []. Qed.
 
 End reassociate_products.
diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index 77eab686a..4755458fc 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -241,7 +241,7 @@ Qed.
 Section reassociate_continuous.
 Context {X Y Z : topologicalType}.
 
-Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z).
+Lemma prodA_continuous : continuous (@prodA X Y Z).
 Proof.
 move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU.
 exists ((P `*` Q), R); first split.
@@ -251,7 +251,7 @@ exists ((P `*` Q), R); first split.
 - by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV.
 Qed.
 
-Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z).
+Lemma prodAr_continuous : continuous (@prodAr X Y Z).
 Proof.
 case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU.
 exists (P, (Q `*` R)); first split => //.