From f719cdc6d1b72990cb31d856af116070c4bd3399 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 3 Sep 2024 15:07:13 +0300 Subject: [PATCH 1/4] prove nat_div_div_r Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index 558502b630..da36427a5c 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -579,6 +579,19 @@ Proof. symmetry; apply nat_div_mod_spec. Defined. +(** Dividing a number by a quotient is the same as dividing the product of the number with the divisor of the quotient by the divdend of the quotient. *) +Definition nat_div_div_r n m k : (k | m) -> n / (m / k) = (n * k) / m. +Proof. + intros [d r]. + destruct (nat_zero_or_gt_zero k) as [[] | kp]. + 1: by rewrite nat_mul_zero_r, nat_div_zero_l. + destruct r. + rhs nrapply nat_div_cancel_mul_r. + 2: exact _. + apply ap. + rapply nat_div_mul_cancel_r. +Defined. + (** We can cancel common factors on the left in a modulo. *) Definition nat_mod_mul_l n m k : (k * n) mod (k * m) = k * (n mod m). From f21db8903016f83302c5b85ef7d3dbc45adc378e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 4 Sep 2024 13:58:33 +0300 Subject: [PATCH 2/4] add variant of nat_div_div_r without assumption Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Division.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v index da36427a5c..4a168f2719 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -556,6 +556,15 @@ Proof. snrapply nat_div_mul_l. Defined. +Definition nat_div_sub_mod n m : n / m = (n - n mod m) / m. +Proof. + destruct (nat_zero_or_gt_zero m) as [[] | mp]. + 1: reflexivity. + symmetry. + rewrite nat_div_mod_spec''. + rapply nat_div_mul_cancel_l. +Defined. + (** Dividing a quotient is the same as dividing by the product of the divisors. *) Definition nat_div_div_l n m k : (n / m) / k = n / (m * k). Proof. @@ -592,6 +601,13 @@ Proof. rapply nat_div_mul_cancel_r. Defined. +(** A variant of [nat_div_div_r] without the divisibility assumption, by modifying [m] to become divisible. *) +Definition nat_div_div_r' n m k : n / (m / k) = (n * k) / (m - m mod k). +Proof. + rewrite (nat_div_sub_mod m k). + rapply nat_div_div_r. +Defined. + (** We can cancel common factors on the left in a modulo. *) Definition nat_mod_mul_l n m k : (k * n) mod (k * m) = k * (n mod m). From b451138f0fe878f36f71b1b73e52e7e73dd27503 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 7 Sep 2024 01:14:47 +0300 Subject: [PATCH 3/4] clarify comment 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 4a168f2719..6c7f93504d 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -588,7 +588,7 @@ Proof. symmetry; apply nat_div_mod_spec. Defined. -(** Dividing a number by a quotient is the same as dividing the product of the number with the divisor of the quotient by the divdend of the quotient. *) +(** Dividing a number by a quotient is the same as dividing the product of the number with the denominator the quotient by the numerator of the quotient. *) Definition nat_div_div_r n m k : (k | m) -> n / (m / k) = (n * k) / m. Proof. intros [d r]. From 101525c964e43c189c54f905602cc0b1169d0021 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sat, 7 Sep 2024 01:48:15 +0300 Subject: [PATCH 4/4] Update theories/Spaces/Nat/Division.v Co-authored-by: Dan Christensen --- 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 6c7f93504d..7e8f888f24 100644 --- a/theories/Spaces/Nat/Division.v +++ b/theories/Spaces/Nat/Division.v @@ -588,7 +588,7 @@ Proof. symmetry; apply nat_div_mod_spec. Defined. -(** Dividing a number by a quotient is the same as dividing the product of the number with the denominator the quotient by the numerator of the quotient. *) +(** Dividing a number by a quotient is the same as dividing the product of the number with the denominator of the quotient by the numerator of the quotient. *) Definition nat_div_div_r n m k : (k | m) -> n / (m / k) = (n * k) / m. Proof. intros [d r].