Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

nat: least common multiple #2207

Merged
merged 8 commits into from
Mar 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion theories/Spaces/Finite/FinNat.v
Original file line number Diff line number Diff line change
Expand Up @@ -72,12 +72,19 @@ Definition is_bounded_fin_to_nat@{} {n} (k : Fin n)
Proof.
induction n as [| n IHn].
- elim k.
- destruct k as [k | []]; exact _.
- destruct k as [k | []].
+ 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)
Expand Down
5 changes: 1 addition & 4 deletions theories/Spaces/Nat/Core.v
Original file line number Diff line number Diff line change
Expand Up @@ -149,23 +149,20 @@ 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 [>=] *)

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 [>] *)

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 *)

Expand Down Expand Up @@ -1139,7 +1136,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
Expand Down
146 changes: 141 additions & 5 deletions theories/Spaces/Nat/Division.v
Original file line number Diff line number Diff line change
Expand Up @@ -635,11 +635,46 @@ Defined.
Definition nat_div_moveL_nV n m k : 0 < k -> n * k = m -> n = m / k.
Proof.
intros H p.
rewrite <- p.
symmetry.
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.
destruct p^.
rapply nat_div_mul_cancel_r.
Defined.

Definition nat_divides_l_div 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_r_div n m l
: (n * l | m) -> (n | m / l).
Proof.
destruct l; only 1: exact _.
intros [k p].
exists k.
rapply nat_div_moveL_nV.
by lhs_V napply nat_mul_assoc.
Defined.

Definition nat_divides_l_mul 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. *)
Expand Down Expand Up @@ -731,9 +766,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.
Expand Down Expand Up @@ -921,6 +954,109 @@ 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]. *)
Instance nat_divides_r_lcm_l n m : (n | nat_lcm n m) := _.

(** [m] divides the least common multiple of [n] and [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 _.
rewrite <- nat_div_mul_r; exact _.
Defined.

(** The least common multiple of [n] and [m] divides any multiple of [n] and [m]. *)
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 _.
rapply nat_divides_l_div.
destruct p.
rewrite nat_dist_sub_l.
napply nat_divides_sub.
1: rewrite nat_mul_comm.
1,2: 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 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.
Proof.
intros H1 H2.
rapply nat_divides_antisym.
Defined.

(** 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.
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. *)
Expand Down
Loading