From 6b7707ec837ff726886d89e9eb3ac66e75eba94d Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 1 Oct 2024 10:27:40 -0400 Subject: [PATCH] unifying names --- CHANGELOG_UNRELEASED.md | 14 ++--- classical/classical_orders.v | 106 +++++++++++++++++------------------ 2 files changed, 60 insertions(+), 60 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c841c80c8..0a99e0909 100644 --- 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 index a5ea3ab1f..b79f4f7b3 100644 --- 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;