diff options
| -rw-r--r-- | mathcomp/ssreflect/order.v | 227 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 41 |
2 files changed, 266 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index f5dfa03..bfb247f 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2019 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. -From mathcomp Require Import div choice fintype tuple bigop finset. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq. +From mathcomp Require Import path fintype tuple bigop finset div prime. (******************************************************************************) (* This files defines order relations. It contains several modules *) @@ -352,6 +352,83 @@ Reserved Notation "x <=^l y ?= 'iff' c" (at level 70, y, c at next level, Reserved Notation "x <=^l y ?= 'iff' c :> T" (at level 70, y, c at next level, format "x '[hv' <=^l y '/' ?= 'iff' c :> T ']'"). +(* Reserved notations for divisibility *) +Reserved Notation "x %<| y" (at level 70, no associativity). + +Reserved Notation "\gcd_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \gcd_ i '/ ' F ']'"). +Reserved Notation "\gcd_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \gcd_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \gcd_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \gcd_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \gcd_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \gcd_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\gcd_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\gcd_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \gcd_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \gcd_ ( i < n ) F ']'"). +Reserved Notation "\gcd_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \gcd_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\gcd_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \gcd_ ( i 'in' A ) '/ ' F ']'"). + +Reserved Notation "\lcm_ i F" + (at level 41, F at level 41, i at level 0, + format "'[' \lcm_ i '/ ' F ']'"). +Reserved Notation "\lcm_ ( i <- r | P ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \lcm_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( i <- r ) F" + (at level 41, F at level 41, i, r at level 50, + format "'[' \lcm_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \lcm_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \lcm_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( i | P ) F" + (at level 41, F at level 41, i at level 50, + format "'[' \lcm_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( i : t | P ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\lcm_ ( i : t ) F" + (at level 41, F at level 41, i at level 50, + only parsing). +Reserved Notation "\lcm_ ( i < n | P ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \lcm_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( i < n ) F" + (at level 41, F at level 41, i, n at level 50, + format "'[' \lcm_ ( i < n ) F ']'"). +Reserved Notation "\lcm_ ( i 'in' A | P ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \lcm_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\lcm_ ( i 'in' A ) F" + (at level 41, F at level 41, i, A at level 50, + format "'[' \lcm_ ( i 'in' A ) '/ ' F ']'"). + (* Reserved notation for converse lattice operations. *) Reserved Notation "A `&^l` B" (at level 48, left associativity). Reserved Notation "A `|^l` B" (at level 52, left associativity). @@ -3831,6 +3908,150 @@ Definition ltEnat := ltEnat. End Exports. End NatOrder. +Module DvdSyntax. + +Lemma dvd_display : unit. Proof. exact: tt. Qed. + +Notation dvd := (@le dvd_display _). +Notation "@ 'dvd' T" := + (@le dvd_display T) (at level 10, T at level 8, only parsing). +Notation sdvd := (@lt dvd_display _). +Notation "@ 'sdvd' T" := + (@lt dvd_display T) (at level 10, T at level 8, only parsing). + +Notation "x %| y" := (dvd x y) : order_scope. +Notation "x %<| y" := (sdvd x y) (at level 70, no associativity) : order_scope. + +Notation gcd := (@meet dvd_display _). +Notation "@ 'gcd' T" := + (@meet dvd_display T) (at level 10, T at level 8, only parsing). +Notation lcm := (@join dvd_display _). +Notation "@ 'lcm' T" := + (@join dvd_display T) (at level 10, T at level 8, only parsing). + +Notation nat0 := (@top dvd_display _). +Notation nat1 := (@bottom dvd_display _). + +Notation "\gcd_ ( i <- r | P ) F" := + (\big[gcd/nat0]_(i <- r | P%B) F%O) : order_scope. +Notation "\gcd_ ( i <- r ) F" := + (\big[gcd/nat0]_(i <- r) F%O) : order_scope. +Notation "\gcd_ ( i | P ) F" := + (\big[gcd/nat0]_(i | P%B) F%O) : order_scope. +Notation "\gcd_ i F" := + (\big[gcd/nat0]_i F%O) : order_scope. +Notation "\gcd_ ( i : I | P ) F" := + (\big[gcd/nat0]_(i : I | P%B) F%O) (only parsing) : + order_scope. +Notation "\gcd_ ( i : I ) F" := + (\big[gcd/nat0]_(i : I) F%O) (only parsing) : order_scope. +Notation "\gcd_ ( m <= i < n | P ) F" := + (\big[gcd/nat0]_(m <= i < n | P%B) F%O) : order_scope. +Notation "\gcd_ ( m <= i < n ) F" := + (\big[gcd/nat0]_(m <= i < n) F%O) : order_scope. +Notation "\gcd_ ( i < n | P ) F" := + (\big[gcd/nat0]_(i < n | P%B) F%O) : order_scope. +Notation "\gcd_ ( i < n ) F" := + (\big[gcd/nat0]_(i < n) F%O) : order_scope. +Notation "\gcd_ ( i 'in' A | P ) F" := + (\big[gcd/nat0]_(i in A | P%B) F%O) : order_scope. +Notation "\gcd_ ( i 'in' A ) F" := + (\big[gcd/nat0]_(i in A) F%O) : order_scope. + +Notation "\lcm_ ( i <- r | P ) F" := + (\big[lcm/nat1]_(i <- r | P%B) F%O) : order_scope. +Notation "\lcm_ ( i <- r ) F" := + (\big[lcm/nat1]_(i <- r) F%O) : order_scope. +Notation "\lcm_ ( i | P ) F" := + (\big[lcm/nat1]_(i | P%B) F%O) : order_scope. +Notation "\lcm_ i F" := + (\big[lcm/nat1]_i F%O) : order_scope. +Notation "\lcm_ ( i : I | P ) F" := + (\big[lcm/nat1]_(i : I | P%B) F%O) (only parsing) : + order_scope. +Notation "\lcm_ ( i : I ) F" := + (\big[lcm/nat1]_(i : I) F%O) (only parsing) : order_scope. +Notation "\lcm_ ( m <= i < n | P ) F" := + (\big[lcm/nat1]_(m <= i < n | P%B) F%O) : order_scope. +Notation "\lcm_ ( m <= i < n ) F" := + (\big[lcm/nat1]_(m <= i < n) F%O) : order_scope. +Notation "\lcm_ ( i < n | P ) F" := + (\big[lcm/nat1]_(i < n | P%B) F%O) : order_scope. +Notation "\lcm_ ( i < n ) F" := + (\big[lcm/nat1]_(i < n) F%O) : order_scope. +Notation "\lcm_ ( i 'in' A | P ) F" := + (\big[lcm/nat1]_(i in A | P%B) F%O) : order_scope. +Notation "\lcm_ ( i 'in' A ) F" := + (\big[lcm/nat1]_(i in A) F%O) : order_scope. + +End DvdSyntax. + +Module NatDvd. +Section NatDvd. + +Implicit Types m n p : nat. + +Lemma lcmnn n : lcmn n n = n. +Proof. by case: n => // n; rewrite /lcmn gcdnn mulnK. Qed. + +Lemma le_def m n : m %| n = (gcdn m n == m)%N. +Proof. by apply/gcdn_idPl/eqP. Qed. + +Lemma joinKI n m : gcdn m (lcmn m n) = m. +Proof. by rewrite (gcdn_idPl _)// dvdn_lcml. Qed. + +Lemma meetKU n m : lcmn m (gcdn m n) = m. +Proof. by rewrite (lcmn_idPl _)// dvdn_gcdl. Qed. + +Lemma meetUl : left_distributive gcdn lcmn. +Proof. +move=> [|m'] [|n'] [|p'] //=; rewrite ?lcmnn ?lcm0n ?lcmn0 ?gcd0n ?gcdn0//. +- by rewrite gcdnC meetKU. +- by rewrite lcmnC gcdnC meetKU. +apply: eqn_from_log; rewrite ?(gcdn_gt0, lcmn_gt0)//= => p. +by rewrite !(logn_gcd, logn_lcm) ?(gcdn_gt0, lcmn_gt0)// minn_maxl. +Qed. + +Definition t_latticeMixin := MeetJoinMixin le_def (fun _ _ => erefl _) + gcdnC lcmnC gcdnA lcmnA joinKI meetKU meetUl gcdnn. + +Import DvdSyntax. +Definition t := nat. + +Canonical eqType := [eqType of t]. +Canonical choiceType := [choiceType of t]. +Canonical countType := [countType of t]. +Canonical porderType := POrderType dvd_display t t_latticeMixin. +Canonical latticeType := LatticeType t t_latticeMixin. +Canonical blatticeType := BLatticeType t + (BLatticeMixin (dvd1n : forall m : t, (1 %| m)%N)). +Canonical tlatticeType := TBLatticeType t + (TBLatticeMixin (dvdn0 : forall m : t, (m %| 0)%N)). + +Lemma dvdE : dvd = dvdn :> rel t. Proof. by []. Qed. +Lemma gcdE : gcd = gcdn :> (t -> t -> t). Proof. by []. Qed. +Lemma lcmE : lcm = lcmn :> (t -> t -> t). Proof. by []. Qed. +Lemma nat1E : nat1 = 1%N :> t. Proof. by []. Qed. +Lemma nat0E : nat0 = 0%N :> t. Proof. by []. Qed. + +End NatDvd. +Module Exports. +Notation natdvd := t. +Canonical eqType. +Canonical choiceType. +Canonical countType. +Canonical porderType. +Canonical latticeType. +Canonical blatticeType. +Canonical tlatticeType. +Definition dvdEnat := dvdE. +Definition gcdEnat := gcdE. +Definition lcmEnat := lcmE. +Definition nat1E := nat1E. +Definition nat0E := nat0E. +End Exports. +End NatDvd. + Module BoolOrder. Section BoolOrder. Implicit Types (x y : bool). @@ -5463,6 +5684,7 @@ Export CBLatticeSyntax. Export CTBLatticeSyntax. Export TotalSyntax. Export ConverseSyntax. +Export DvdSyntax. End Syntax. Module LTheory. @@ -5515,6 +5737,7 @@ Export Order.CanMixin.Exports. Export Order.SubOrder.Exports. Export Order.NatOrder.Exports. +Export Order.NatDvd.Exports. Export Order.BoolOrder.Exports. Export Order.ProdOrder.Exports. Export Order.SigmaOrder.Exports. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 4e55abe..4f0ee77 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -715,6 +715,9 @@ set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn. by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn. Qed. +Lemma logn_coprime p m : coprime p m -> logn p m = 0. +Proof. by move=> coprime_pm; rewrite -[m]muln1 logn_Gauss// logn1. Qed. + Lemma lognM p m n : 0 < m -> 0 < n -> logn p (m * n) = logn p m + logn p n. Proof. case p_pr: (prime p); last by rewrite /logn p_pr. @@ -738,6 +741,29 @@ case: (posnP n) => [-> |]; first by rewrite div0n logn0. by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK. Qed. +Lemma logn_gcd p m n : 0 < m -> 0 < n -> + logn p (gcdn m n) = minn (logn p m) (logn p n). +Proof. +case p_pr: (prime p); last by rewrite /logn p_pr. +wlog le_log_mn: m n / logn p m <= logn p n => [hwlog m_gt0 n_gt0|]. + have /orP[] := leq_total (logn p m) (logn p n) => /hwlog; first exact. + by rewrite gcdnC minnC; apply. +have xlp := pfactor_coprime p_pr => /xlp[m' cpm' {1}->] /xlp[n' cpn' {1}->]. +rewrite (minn_idPl _)// -(subnK le_log_mn) expnD mulnA -muln_gcdl. +rewrite lognM//; last first. + rewrite Gauss_gcdl ?coprime_expr 1?coprime_sym// gcdn_gt0. + by case: m' cpm' p_pr => //; rewrite /coprime gcdn0 => /eqP->. +rewrite pfactorK// Gauss_gcdl; last by rewrite coprime_expr// coprime_sym. +by rewrite logn_coprime// /coprime gcdnA (eqP cpm') gcd1n. +Qed. + +Lemma logn_lcm p m n : 0 < m -> 0 < n -> + logn p (lcmn m n) = maxn (logn p m) (logn p n). +Proof. +move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//. +by rewrite lognM// logn_gcd// -addn_min_max addnC addnK. +Qed. + Lemma dvdn_pfactor p d n : prime p -> reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n). Proof. @@ -899,6 +925,14 @@ apply: eq_bigr => p _; rewrite ltnS lognE. by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq. Qed. +Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n -> + (forall p, p \in pi -> logn p m = logn p n) -> m`_pi = n`_pi. +Proof. +move=> m_gt0 n_gt0 eq_log. +rewrite !(@widen_partn (maxn m n)) ?leq_max ?leqnn ?orbT//. +by apply: eq_bigr => p /eq_log ->. +Qed. + Lemma partn0 pi : 0`_pi = 1. Proof. by apply: big1_seq => [] [|n]; rewrite andbC. Qed. @@ -983,6 +1017,13 @@ move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=. by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _). Qed. +Lemma eqn_from_log m n : 0 < m -> 0 < n -> + (forall p, logn p m = logn p n) -> m = n. +Proof. +move=> m_gt0 n_gt0 eq_log; rewrite -[m]partnT// -[n]partnT//. +exact: eq_partn_from_log. +Qed. + Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n. Proof. move=> n_gt0; rewrite -{3}(partnT n_gt0) /partn. |