From a143c8da7dfe15406c6a6112e1a34c013d71919a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 22 Jan 2025 18:40:51 +0100 Subject: [PATCH 1/8] nat: least common multiple Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 146 ++++++++++++++++++++++++++++++++- 1 file changed, 143 insertions(+), 3 deletions(-) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index c87b6bba29..ef99aa4c38 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -640,6 +640,44 @@ Proof. rapply nat_div_mul_cancel_r. Defined. +Definition nat_div_moveR_nV n m k : 0 < k -> n = m * k -> n / k = m. +Proof. + intros H p. + symmetry. + rapply nat_div_moveL_nV. + by symmetry. +Defined. + +Definition nat_divides_div_l n m l + : 0 < m -> (m | n) -> (n | l * m) -> (n / m | l). +Proof. + intros H1 H2 [y q]. + exists y. + rewrite nat_div_mul_l; only 2: exact _. + by rapply nat_div_moveR_nV. +Defined. + +Definition nat_divides_div_r n m l + : (n * l | m) -> (n | m / l). +Proof. + destruct l; only 1: exact _. + intros [k p]. + exists k. + napply nat_div_moveL_nV. + 1: exact _. + by lhs_V napply nat_mul_assoc. +Defined. + +Definition nat_divides_div_r_inv n m l + : (l | m) -> (n | m / l) -> (n * l | m). +Proof. + intros H [k p]. + exists k. + rewrite nat_mul_assoc. + rewrite p. + rapply nat_mul_div_cancel_r. +Defined. + (** ** Greatest Common Divisor *) (** The greatest common divisor of [0] and a number is the number itself. *) @@ -731,9 +769,7 @@ Defined. (** [nat_gcd] is associative. *) Definition nat_gcd_assoc n m k : nat_gcd n (nat_gcd m k) = nat_gcd (nat_gcd n m) k. Proof. - napply nat_gcd_unique. - - intros q H1 H2. - rapply nat_divides_r_gcd. + rapply nat_gcd_unique. - rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)). - apply nat_divides_r_gcd; rapply nat_divides_trans. Defined. @@ -921,6 +957,110 @@ Proof. destruct n; [ right | left ]; exact _. Defined. +(** ** Least common multiple *) + +(** The least common multiple [nat_lcm n m] is the smallest natural number divisibile by both [n] and [m]. *) +Definition nat_lcm (n m : nat) : nat := n * (m / nat_gcd n m). + +(** The least common multiple of [0] and [n] is [0]. *) +Definition nat_lcm_zero_l n : nat_lcm 0 n = 0 := idpath. + +(** The least common multiple of [n] and [0] is [0]. *) +Definition nat_lcm_zero_r n : nat_lcm n 0 = 0. +Proof. + unfold nat_lcm. + by rewrite nat_div_zero_l, nat_mul_zero_r. +Defined. + +(** The least common multiple of [1] and [n] is [n]. *) +Definition nat_lcm_one_l n : nat_lcm 1 n = n. +Proof. + unfold nat_lcm. + by rewrite nat_gcd_one_l, nat_div_one_r, nat_mul_one_l. +Defined. + +(** The least common multiple of [n] and [1] is [n]. *) +Definition nat_lcm_one_r n : nat_lcm n 1 = n. +Proof. + unfold nat_lcm. + by rewrite nat_gcd_one_r, nat_div_one_r, nat_mul_one_r. +Defined. + +(** Idempotency. *) +Definition nat_lcm_idem n : nat_lcm n n = n. +Proof. + unfold nat_lcm. + by rewrite nat_gcd_idem, nat_mul_div_cancel_l. +Defined. + +(** [n] divides the least common multiple of [n] and [m]. *) +Global Instance nat_divides_r_lcm_l n m : (n | nat_lcm n m) := _. + +(** [m] divides the least common multiple of [n] and [m]. *) +Global Instance nat_divides_r_lcm_r n m : (m | nat_lcm n m). +Proof. + unfold nat_lcm. + rewrite nat_div_mul_l; only 2: exact _. + rewrite <- nat_div_mul_r; exact _. +Defined. + +(** The least common multiple of [n] and [m] divides any multiple of [n] and [m]. *) +Global Instance nat_divides_l_lcm n m k : (n | k) -> (m | k) -> (nat_lcm n m | k). +Proof. + intros H1 H2. + destruct (equiv_leq_lt_or_eq (n:=0) (m:=n) _) as [lt_n | p]; + only 2: by destruct p. + destruct (equiv_leq_lt_or_eq (n:=0) (m:=m) _) as [lt_m | q]; + only 2: (destruct q; by rewrite nat_lcm_zero_r). + unfold nat_lcm. + destruct (nat_bezout_pos_l n m _) as [a [b p]]. + apply nat_moveR_nV in p. + rewrite nat_div_mul_l. + 2: exact _. + napply nat_divides_div_l. + 1,2: exact _. + destruct p. + rewrite nat_dist_sub_l. + napply nat_divides_sub. + 1,2: rewrite nat_mul_assoc. + 1,2: only 1: rewrite nat_mul_comm; exact _. +Defined. + +Definition nat_divides_l_iff_divides_l_lcm n m k + : (n | k) * (m | k) <-> (nat_lcm n m | k). +Proof. + split. + - intros [H1 H2]; exact _. + - intros H; split. + + rapply (nat_divides_trans _ H). + + exact _. +Defined. + +(** If [k] divides all common multiples of [n] and [m], and [k] is also a common multiple, then it must necesserily be equal to the least common multiple. *) +Definition nat_lcm_unique n m k + (H : forall q, (n | q) -> (m | q) -> (k | q)) + : (n | k) -> (m | k) -> nat_lcm n m = k. +Proof. + intros H1 H2. + rapply nat_divides_antisym. +Defined. + +(** As a corollary of uniquness, we get that the least common multiple operation is commutative. *) +Definition nat_lcm_comm n m : nat_lcm n m = nat_lcm m n. +Proof. + rapply nat_lcm_unique. +Defined. + +(** [nat_lcm] is associative. *) +Definition nat_lcm_assoc n m k : nat_lcm n (nat_lcm m k) = nat_lcm (nat_lcm n m) k. +Proof. + rapply nat_lcm_unique. + intros q H1 H2. + rapply nat_divides_l_lcm. + rapply nat_divides_l_lcm. + rapply (nat_divides_trans _ H2). +Defined. + (** ** Prime Numbers *) (** A prime number is a number greater than [1] that is only divisible by [1] and itself. *) From 47cf5317e79fd6371d090be937d77199d63f93f3 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 17 Feb 2025 16:00:05 -0500 Subject: [PATCH 2/8] Nat/Division: minor simplifications/corrections --- theories/Spaces/Nat/Division.v | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index ef99aa4c38..262dd095ce 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -635,17 +635,15 @@ Defined. Definition nat_div_moveL_nV n m k : 0 < k -> n * k = m -> n = m / k. Proof. intros H p. - rewrite <- p. - symmetry. - rapply nat_div_mul_cancel_r. + destruct p. + symmetry; rapply nat_div_mul_cancel_r. Defined. Definition nat_div_moveR_nV n m k : 0 < k -> n = m * k -> n / k = m. Proof. intros H p. - symmetry. - rapply nat_div_moveL_nV. - by symmetry. + destruct p^. + rapply nat_div_mul_cancel_r. Defined. Definition nat_divides_div_l n m l @@ -1017,13 +1015,12 @@ Proof. apply nat_moveR_nV in p. rewrite nat_div_mul_l. 2: exact _. - napply nat_divides_div_l. - 1,2: exact _. + rapply nat_divides_div_l. destruct p. rewrite nat_dist_sub_l. napply nat_divides_sub. - 1,2: rewrite nat_mul_assoc. - 1,2: only 1: rewrite nat_mul_comm; exact _. + 1: rewrite nat_mul_comm. + 1,2: exact _. Defined. Definition nat_divides_l_iff_divides_l_lcm n m k @@ -1036,7 +1033,7 @@ Proof. + exact _. Defined. -(** If [k] divides all common multiples of [n] and [m], and [k] is also a common multiple, then it must necesserily be equal to the least common multiple. *) +(** If [k] divides all common multiples of [n] and [m], and [k] is also a common multiple, then it must necessarily be equal to the least common multiple. *) Definition nat_lcm_unique n m k (H : forall q, (n | q) -> (m | q) -> (k | q)) : (n | k) -> (m | k) -> nat_lcm n m = k. @@ -1045,7 +1042,7 @@ Proof. rapply nat_divides_antisym. Defined. -(** As a corollary of uniquness, we get that the least common multiple operation is commutative. *) +(** As a corollary of uniqueness, we get that the least common multiple operation is commutative. *) Definition nat_lcm_comm n m : nat_lcm n m = nat_lcm m n. Proof. rapply nat_lcm_unique. From 7bf4509bbe41de5debce583f48da5560f80cc532 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 18 Feb 2025 12:26:28 +0100 Subject: [PATCH 3/8] improve looping lt_succ_r Signed-off-by: Ali Caglayan --- theories/Spaces/Finite/FinNat.v | 5 ++++- theories/Spaces/Nat/Core.v | 2 +- theories/Spaces/Nat/Division.v | 3 +-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/theories/Spaces/Finite/FinNat.v b/theories/Spaces/Finite/FinNat.v index 85bf09c03c..523ac09688 100644 --- a/theories/Spaces/Finite/FinNat.v +++ b/theories/Spaces/Finite/FinNat.v @@ -72,7 +72,10 @@ Definition is_bounded_fin_to_nat@{} {n} (k : Fin n) Proof. induction n as [| n IHn]. - elim k. - - destruct k as [k | []]; exact _. + (** These instances are chosen on purpose. *) + - destruct k as [k | []]. + + rapply lt_succ_r. + + exact _. Defined. Definition fin_to_finnat {n} (k : Fin n) : FinNat n diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v index 63cd23b1ec..673fef7325 100644 --- a/theories/Spaces/Nat/Core.v +++ b/theories/Spaces/Nat/Core.v @@ -1139,7 +1139,7 @@ Hint Immediate nat_add_monotone : typeclass_instances. (** [nat_succ] is strictly monotone. *) Instance lt_succ {n m} : n < m -> n.+1 < m.+1 := _. -Instance lt_succ_r {n m} : n < m -> n < m.+1 := _. +Instance lt_succ_r {n m} : n < m -> n < m.+1 | 100 := _. (** Addition on the left is strictly monotone. *) Definition nat_add_l_strictly_monotone {n m} k diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index 262dd095ce..abfb66166a 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -661,8 +661,7 @@ Proof. destruct l; only 1: exact _. intros [k p]. exists k. - napply nat_div_moveL_nV. - 1: exact _. + rapply nat_div_moveL_nV. by lhs_V napply nat_mul_assoc. Defined. From 6582d64fa3ea8b9d3ec351bf1c7c52cd04c05c34 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Tue, 18 Feb 2025 07:20:51 -0500 Subject: [PATCH 4/8] FinNat: clarify why choice of proof of inequality is important --- theories/Spaces/Finite/FinNat.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/theories/Spaces/Finite/FinNat.v b/theories/Spaces/Finite/FinNat.v index 523ac09688..5e21ceb04e 100644 --- a/theories/Spaces/Finite/FinNat.v +++ b/theories/Spaces/Finite/FinNat.v @@ -72,15 +72,19 @@ Definition is_bounded_fin_to_nat@{} {n} (k : Fin n) Proof. induction n as [| n IHn]. - elim k. - (** These instances are chosen on purpose. *) - destruct k as [k | []]. - + rapply lt_succ_r. + + rapply lt_succ_r. (* Typeclass search finds a different solution, but we want this one. *) + exact _. Defined. Definition fin_to_finnat {n} (k : Fin n) : FinNat n := (fin_to_nat k; is_bounded_fin_to_nat k). +(** Because the proof of [is_bounded_fin_to_nat] was chosen carefully, we have the following definitional equality. *) +Definition path_fin_to_finnat_fin_incl_incl_finnat_fin_to_finnat {n} (k : Fin n) + : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k) + := idpath. + Fixpoint finnat_to_fin@{} {n : nat} : FinNat n -> Fin n := match n with | 0 => fun u => Empty_rec (not_lt_zero_r _ u.2) From 587d7206be22d922b893e94a27fa4850e28bde76 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 22:46:48 +0000 Subject: [PATCH 5/8] remove redundant instances Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Core.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v index 673fef7325..724816915f 100644 --- a/theories/Spaces/Nat/Core.v +++ b/theories/Spaces/Nat/Core.v @@ -149,7 +149,6 @@ Definition lt n m : Type0 := leq (S n) m. Existing Class lt. #[export] Hint Unfold lt : typeclass_instances. Infix "<" := lt : nat_scope. -Instance lt_is_leq n m : leq n.+1 m -> lt n m | 100 := idmap. (** *** Greater than or equal To [>=] *) @@ -157,7 +156,6 @@ Definition geq n m := leq m n. Existing Class geq. #[export] Hint Unfold geq : typeclass_instances. Infix ">=" := geq : nat_scope. -Instance geq_is_leq n m : leq m n -> geq n m | 100 := idmap. (*** Greater Than [>] *) @@ -165,7 +163,6 @@ Definition gt n m := lt m n. Existing Class gt. #[export] Hint Unfold gt : typeclass_instances. Infix ">" := gt : nat_scope. -Instance gt_is_leq n m : leq m.+1 n -> gt n m | 100 := idmap. (** *** Combined comparison predicates *) From 2134880528877123e254a3c2f680def77e5c4625 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 23:03:38 +0000 Subject: [PATCH 6/8] rename nat_divides_l_mul Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index abfb66166a..2a31b27474 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -665,7 +665,7 @@ Proof. by lhs_V napply nat_mul_assoc. Defined. -Definition nat_divides_div_r_inv n m l +Definition nat_divides_l_mul n m l : (l | m) -> (n | m / l) -> (n * l | m). Proof. intros H [k p]. From 830d4b63a66aa5c904090e6749e727fe49801a00 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 24 Feb 2025 23:05:19 +0000 Subject: [PATCH 7/8] rename nat_divides_{l,r}_div Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index 2a31b27474..572138cd5c 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -646,7 +646,7 @@ Proof. rapply nat_div_mul_cancel_r. Defined. -Definition nat_divides_div_l n m l +Definition nat_divides_l_div n m l : 0 < m -> (m | n) -> (n | l * m) -> (n / m | l). Proof. intros H1 H2 [y q]. @@ -655,7 +655,7 @@ Proof. by rapply nat_div_moveR_nV. Defined. -Definition nat_divides_div_r n m l +Definition nat_divides_r_div n m l : (n * l | m) -> (n | m / l). Proof. destruct l; only 1: exact _. @@ -1014,7 +1014,7 @@ Proof. apply nat_moveR_nV in p. rewrite nat_div_mul_l. 2: exact _. - rapply nat_divides_div_l. + rapply nat_divides_l_div. destruct p. rewrite nat_dist_sub_l. napply nat_divides_sub. From 7b4294249a8c6f3803f9cd99d6c824158c9df3bc Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 13 Mar 2025 15:48:39 +0000 Subject: [PATCH 8/8] remove `Global` keyword Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index 572138cd5c..8bcadbcd1b 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -991,10 +991,10 @@ Proof. Defined. (** [n] divides the least common multiple of [n] and [m]. *) -Global Instance nat_divides_r_lcm_l n m : (n | nat_lcm n m) := _. +Instance nat_divides_r_lcm_l n m : (n | nat_lcm n m) := _. (** [m] divides the least common multiple of [n] and [m]. *) -Global Instance nat_divides_r_lcm_r n m : (m | nat_lcm n m). +Instance nat_divides_r_lcm_r n m : (m | nat_lcm n m). Proof. unfold nat_lcm. rewrite nat_div_mul_l; only 2: exact _. @@ -1002,7 +1002,7 @@ Proof. Defined. (** The least common multiple of [n] and [m] divides any multiple of [n] and [m]. *) -Global Instance nat_divides_l_lcm n m k : (n | k) -> (m | k) -> (nat_lcm n m | k). +Instance nat_divides_l_lcm n m k : (n | k) -> (m | k) -> (nat_lcm n m | k). Proof. intros H1 H2. destruct (equiv_leq_lt_or_eq (n:=0) (m:=n) _) as [lt_n | p];