unifying names

math-comp · Oct 1, 2024 · 6b7707e · 6b7707e
1 parent 5041bdb
commit 6b7707e
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 60 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -24,17 +24,17 @@
 - in `measure.v`:
   + lemma `measurable_fun_set1`
 - in file `classical_orders.v`,
-  + new definitions `same_prefix`, `first_diff`, `lexi_bigprod`, `start_with`,
-    `big_lexi_order`, and `big_lexi_ord`.
+  + new definitions `big_lexi_order`, `same_prefix`, `first_diff`,
+    `big_lexi_le`, and `start_with`.
   + new lemmas `same_prefix0`, `same_prefix_sym`, `same_prefix_leq`,
     `same_prefix_refl`, `same_prefix_trans`, `first_diff_sym`,
     `first_diff_unique`, `first_diff_SomeP`, `first_diff_NoneP`,
     `first_diff_lt`, `first_diff_eq`, `first_diff_dfwith`,
-    `lexi_bigprod_reflexive`, `lexi_bigprod_anti`, `lexi_bigprod_trans`,
-    `lexi_bigprod_total`, `start_with_prefix`, `lexi_bigprod_prefix_lt`,
-    `lexi_bigprod_prefix_gt`, `lexi_bigprod_between`,
-    `big_lexi_interval_prefix`, and `same_prefix_closed_itv`.
-  + lemma `leEbig_lexi_order`
+    `big_lexi_le_reflexive`, `big_lexi_le_anti`, `big_lexi_le_trans`,
+    `big_lexi_le_total`, `start_with_prefix`, `leEbig_lexi_order`,
+    `big_lexi_order_prefix_lt`, `big_lexi_order_prefix_gt`,
+    `big_lexi_order_between`, `big_lexi_order_interval_prefix`, and
+    `big_lexi_order_prefix_closed_itv`.
 
 ### Changed
 

diff --git a/classical/classical_orders.v b/classical/classical_orders.v
@@ -9,10 +9,10 @@ From mathcomp Require Import functions set_interval.
 (* This file provides some additional order theory that requires stronger     *)
 (* axioms than mathcomp's own orders expect.                                  *)
 (* ```                                                                        *)
-(*    same_prefix n == two elements in a product space agree up n             *)
+(*     same_prefix n == two elements in a product space agree up n            *)
 (*    first_diff x y == the first occurrence where x n != y n, or None        *)
-(*      lexi_bigprod == the (countably) infinite lexicographical ordering     *)
-(*    big_lexi_order == an alias for attack this order type                   *)
+(*       big_lexi_le == the (countably) infinite lexicographical ordering     *)
+(*    big_lexi_order == an alias for attaching this order type                *)
 (*  start_with n x y == x for the first n values, then switches to y          *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -25,7 +25,11 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 
 Local Open Scope classical_set_scope.
 
-Section big_lexi_order.
+Definition big_lexi_order {I : Type} (T : I -> Type) : Type := forall i, T i.
+HB.instance Definition _ (I : Type) (K : I -> choiceType) :=
+  Choice.on (big_lexi_order K).
+
+Section big_lexi_le.
 Context {K : nat -> eqType}.
 
 Definition same_prefix n (t1 t2 : forall n, K n) :=
@@ -123,32 +127,32 @@ apply/first_diff_SomeP; split; last by rewrite dfwithin.
 by move=> n ni; rewrite dfwithout// gt_eqF.
 Qed.
 
-Definition lexi_bigprod
+Definition big_lexi_le
     (R : forall n, K n -> K n -> bool) (t1 t2 : forall n, K n) :=
   if first_diff t1 t2 is Some n then R n (t1 n) (t2 n) else true.
 
-Lemma lexi_bigprod_reflexive R : reflexive (lexi_bigprod R).
+Lemma big_lexi_le_reflexive R : reflexive (big_lexi_le R).
 Proof.
-move=> x; rewrite /lexi_bigprod /= /first_diff.
+move=> x; rewrite /big_lexi_le /= /first_diff.
 by case: xgetP => //= -[n _|//] [m []]; rewrite eqxx.
 Qed.
 
-Lemma lexi_bigprod_anti R : (forall n, antisymmetric (R n)) ->
-  antisymmetric (lexi_bigprod R).
+Lemma big_lexi_le_anti R : (forall n, antisymmetric (R n)) ->
+  antisymmetric (big_lexi_le R).
 Proof.
 move=> antiR x y /andP[xy yx]; apply/first_diff_NoneP; move: xy yx.
-rewrite /lexi_bigprod first_diff_sym.
+rewrite /big_lexi_le first_diff_sym.
 case E : (first_diff y x) => [n|]// Rxy Ryx.
 case/first_diff_SomeP : E => _.
 by apply: contra_neqP => _; apply/antiR; rewrite Ryx.
 Qed.
 
-Lemma lexi_bigprod_trans R :
+Lemma big_lexi_le_trans R :
   (forall n, transitive (R n)) ->
   (forall n, antisymmetric (R n)) ->
-  transitive (lexi_bigprod R).
+  transitive (big_lexi_le R).
 Proof.
-move=> Rtrans Ranti y x z; rewrite /lexi_bigprod /=.
+move=> Rtrans Ranti y x z; rewrite /big_lexi_le /=.
 case Ep : (first_diff x y) => [p|]; last by move/first_diff_NoneP : Ep ->.
 case Er : (first_diff x z) => [r|]; last by move/first_diff_NoneP : Er ->.
 case Eq : (first_diff y z) => [q|]; first last.
@@ -168,12 +172,12 @@ have [pq|qp|pqE]:= ltgtP p q.
   by apply/Ranti/andP; split.
 Qed.
 
-Lemma lexi_bigprod_total R : (forall n, total (R n)) -> total (lexi_bigprod R).
+Lemma big_lexi_le_total R : (forall n, total (R n)) -> total (big_lexi_le R).
 Proof.
 move=> Rtotal x y.
 case E : (first_diff x y) => [n|]; first last.
-  by move/first_diff_NoneP : E ->; rewrite lexi_bigprod_reflexive.
-by rewrite /lexi_bigprod E first_diff_sym E; exact: Rtotal.
+  by move/first_diff_NoneP : E ->; rewrite big_lexi_le_reflexive.
+by rewrite /big_lexi_le E first_diff_sym E; exact: Rtotal.
 Qed.
 
 Definition start_with n (t1 t2 : forall n, K n) (i : nat) : K i :=
@@ -182,79 +186,75 @@ Definition start_with n (t1 t2 : forall n, K n) (i : nat) : K i :=
 Lemma start_with_prefix n x y : same_prefix n x (start_with n x y).
 Proof. by move=> r rn; rewrite /start_with rn. Qed.
 
-End big_lexi_order.
-
-Definition big_lexi_order {I : Type} (T : I -> Type) : Type := forall i, T i.
-HB.instance Definition _ (I : Type) (K : I -> choiceType) :=
-  Choice.on (big_lexi_order K).
+End big_lexi_le.
 
 Section big_lexi_porder.
 Context {d} {K : nat -> porderType d}.
 
-Definition big_lexi_ord : rel (big_lexi_order K) :=
-  lexi_bigprod (fun n k1 k2 => k1 <= k2)%O.
+Let Rn n (k1 k2 : K n) := (k1 <= k2)%O.
 
-Local Lemma big_lexi_ord_reflexive : reflexive big_lexi_ord.
-Proof. exact: lexi_bigprod_reflexive. Qed.
+Local Lemma big_lexi_ord_reflexive : reflexive (big_lexi_le Rn).
+Proof. exact: big_lexi_le_reflexive. Qed.
 
-Local Lemma big_lexi_ord_anti : antisymmetric big_lexi_ord.
-Proof. by apply: lexi_bigprod_anti => n; exact: le_anti. Qed.
+Local Lemma big_lexi_ord_anti : antisymmetric (big_lexi_le Rn).
+Proof. by apply: big_lexi_le_anti => n; exact: le_anti. Qed.
 
-Local Lemma big_lexi_ord_trans : transitive big_lexi_ord.
-Proof. by apply: lexi_bigprod_trans=> n; [exact: le_trans|exact: le_anti]. Qed.
+Local Lemma big_lexi_ord_trans : transitive (big_lexi_le Rn).
+Proof. by apply: big_lexi_le_trans => n; [exact: le_trans|exact: le_anti]. Qed.
 
 HB.instance Definition _ := Order.Le_isPOrder.Build d (big_lexi_order K)
   big_lexi_ord_reflexive big_lexi_ord_anti big_lexi_ord_trans.
 
+Lemma leEbig_lexi_order (a b : big_lexi_order K) :
+  (a <= b)%O = if first_diff a b is Some n then (a n <= b n)%O else true.
+
+Proof. by []. Qed.
+
 End big_lexi_porder.
 
 Section big_lexi_total.
 Context {d} {K : nat -> orderType d}.
 
-Local Lemma big_lexi_ord_total : total (@big_lexi_ord _ K).
-Proof. by apply: lexi_bigprod_total => ?; exact: le_total. Qed.
+Local Lemma big_lexi_ord_total : total (@Order.le _ (big_lexi_order K)).
+Proof. by apply: big_lexi_le_total => ?; exact: le_total. Qed.
 
 HB.instance Definition _ := Order.POrder_isTotal.Build _
   (big_lexi_order K) big_lexi_ord_total.
 
-Lemma leEbig_lexi_order (a b : big_lexi_order K) :
-  (a <= b)%O = if first_diff a b is Some n then (a n <= b n)%O else true.
-Proof. by []. Qed.
-
 End big_lexi_total.
 
 Section big_lexi_bottom.
 Context {d} {K : nat -> bPOrderType d}.
 
-Local Lemma big_lex_bot x : (@big_lexi_ord _ K) (fun=> \bot)%O x.
+Let b : big_lexi_order K := (fun=> \bot)%O.
+Local Lemma big_lex_bot (x : big_lexi_order K) : (b <= x)%O.
 Proof.
-rewrite /big_lexi_ord /lexi_bigprod.
-by case: first_diff => // ?; exact: Order.le0x.
+by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.le0x.
 Qed.
 
 HB.instance Definition _ := @Order.hasBottom.Build _
-  (big_lexi_order K) (fun=> \bot)%O big_lex_bot.
+  (big_lexi_order K) b big_lex_bot.
 
 End big_lexi_bottom.
 
 Section big_lexi_top.
 Context {d} {K : nat -> tPOrderType d}.
 
-Local Lemma big_lex_top x : (@big_lexi_ord _ K) x (fun=> \top)%O.
+Let t : big_lexi_order K := (fun=> \top)%O.
+Local Lemma big_lex_top (x : big_lexi_order K) : (x <= t)%O.
 Proof.
-rewrite /big_lexi_ord /lexi_bigprod.
-by case: first_diff => // ?; exact: Order.lex1.
+by rewrite leEbig_lexi_order; case: first_diff => // ?; exact: Order.lex1.
 Qed.
 
 HB.instance Definition _ := @Order.hasTop.Build _
-  (big_lexi_order K) (fun=> \top)%O big_lex_top.
+  (big_lexi_order K) t big_lex_top.
 
 End big_lexi_top.
 
 Section big_lexi_intervals.
 Context {d} {K : nat -> orderType d}.
 
-Lemma lexi_bigprod_prefix_lt (b a x: big_lexi_order K) n :
+Lemma big_lexi_order_prefix_lt (b a x: big_lexi_order K) n :
   (a < b)%O ->
   first_diff a b = Some n ->
   same_prefix n.+1 x b ->
@@ -273,7 +273,7 @@ apply: (@first_diff_unique _ a x) => //=; [| |by case/first_diff_SomeP : E1..].
 - by rewrite (pfx n (ltnSn _)).
 Qed.
 
-Lemma lexi_bigprod_prefix_gt (b a x : big_lexi_order K) n :
+Lemma big_lexi_order_prefix_gt (b a x : big_lexi_order K) n :
   (b < a)%O ->
   first_diff a b = Some n ->
   same_prefix n.+1 x b ->
@@ -293,7 +293,7 @@ apply: (@first_diff_unique _ x a) => //=; [| |by case/first_diff_SomeP : E1..].
 - by rewrite (pfx n (ltnSn _)) eq_sym; exact/eqP.
 Qed.
 
-Lemma lexi_bigprod_between (a x b : big_lexi_order K) n :
+Lemma big_lexi_order_between (a x b : big_lexi_order K) n :
   (a <= x <= b)%O ->
   same_prefix n a b ->
   same_prefix n x a.
@@ -324,7 +324,7 @@ rewrite leq_eqVlt => /predU1P[->//|nr].
 by case/first_diff_SomeP : E => /(_ n nr) ->.
 Qed.
 
-Lemma big_lexi_interval_prefix (i : interval (big_lexi_order K))
+Lemma big_lexi_order_interval_prefix (i : interval (big_lexi_order K))
     (x : big_lexi_order K) :
   itv_open_ends i -> x \in i ->
   exists n, same_prefix n x `<=` [set` i].
@@ -337,28 +337,28 @@ move: i; case=> [][[]l|[]] [[]r|[]] [][]; rewrite ?in_itv /= ?andbT.
     by move: xr; move/first_diff_NoneP : E2 ->; rewrite bnd_simp.
   exists (Order.max n m).+1 => p xppfx; rewrite set_itvE.
   apply/andP; split.
-    apply: (lexi_bigprod_prefix_lt lx E1) => w wm; apply/esym/xppfx.
+    apply: (big_lexi_order_prefix_lt lx E1) => w wm; apply/esym/xppfx.
     by move/ltnSE/leq_ltn_trans : wm; apply; rewrite ltnS leq_max leqnn orbT.
   rewrite first_diff_sym in E2.
-  apply: (lexi_bigprod_prefix_gt xr E2) => w wm; apply/esym/xppfx.
+  apply: (big_lexi_order_prefix_gt xr E2) => w wm; apply/esym/xppfx.
   by move/ltnSE/leq_ltn_trans : wm; apply; rewrite ltnS leq_max leqnn.
 - move=> lx.
   case E1 : (first_diff l x) => [m|]; first last.
     by move: lx; move/first_diff_NoneP : E1 ->; rewrite bnd_simp.
   exists m.+1 => p xppfx; rewrite set_itvE /=.
-  by apply: (lexi_bigprod_prefix_lt lx E1) => w wm; exact/esym/xppfx.
+  by apply: (big_lexi_order_prefix_lt lx E1) => w wm; exact/esym/xppfx.
 - move=> xr.
   case E2 : (first_diff x r) => [n|]; first last.
     by move: xr; move/first_diff_NoneP : E2 ->; rewrite bnd_simp.
   exists n.+1; rewrite first_diff_sym in E2 => p xppfx.
   rewrite set_itvE /=.
-  by apply: (lexi_bigprod_prefix_gt xr E2) => w wm; exact/esym/xppfx.
+  by apply: (big_lexi_order_prefix_gt xr E2) => w wm; exact/esym/xppfx.
 by move=> _; exists 0 => ? ?; rewrite set_itvE.
 Qed.
 End big_lexi_intervals.
 
 (** TODO: generalize to tbOrderType when that's available in mathcomp *)
-Lemma same_prefix_closed_itv {d} {K : nat -> finOrderType d} n
+Lemma big_lexi_order_prefix_closed_itv {d} {K : nat -> finOrderType d} n
   (x : big_lexi_order K) :
   same_prefix n x = `[
     (start_with n x (fun=>\bot):big_lexi_order K)%O,
@@ -367,7 +367,7 @@ Proof.
 rewrite eqEsubset; split=> [z pfxz|z]; first last.
   rewrite set_itvE /= => xbt; apply: same_prefix_trans.
     exact: (start_with_prefix _ (fun=> \bot)%O).
-  apply/same_prefix_sym/(lexi_bigprod_between xbt).
+  apply/same_prefix_sym/(big_lexi_order_between xbt).
   apply: same_prefix_trans (start_with_prefix _ _).
   exact/same_prefix_sym/start_with_prefix.
 rewrite set_itvE /= !leEbig_lexi_order; apply/andP; split;