Merge pull request #396 from CohenCyril/edivnD

More arithmetic theorems

2 files changed, 145 insertions, 4 deletions

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index d71db3a..48fb9fb 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -185,13 +185,56 @@ move/leq_divRL=> -> le_de.
 by apply: leq_trans (leq_trunc_div m e); apply: leq_mul.
 Qed.
 
-Lemma leq_divDl p m n : (m + n) %/ p <= m %/ p + n %/ p + 1.
+Lemma edivnD m n d (offset := m %% d + n %% d >= d) : 0 < d ->
+   edivn (m + n) d = (m %/ d + n %/ d + offset, m %% d + n %% d - offset * d).
+Proof.
+rewrite {}/offset; case: d => // d _; rewrite /divn !modn_def.
+case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt].
+rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt).
+have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq.
+rewrite addn1 mul1n -{1}(subnKC d_lt) addnA -mulSnr edivn_eq//.
+by rewrite ltn_subLR// -addnS leq_add.
+Qed.
+
+Lemma divnD m n d : 0 < d ->
+  (m + n) %/ d = (m %/ d) + (n %/ d) + (m %% d + n %% d >= d).
+Proof. by move=> /(@edivnD m n); rewrite edivn_def => -[]. Qed.
+
+Lemma modnD m n d : 0 < d ->
+  (m + n) %% d = m %% d + n %% d - (m %% d + n %% d >= d) * d.
+Proof. by move=> /(@edivnD m n); rewrite edivn_def => -[]. Qed.
+
+Lemma leqDmod m n d : 0 < d ->
+  (d <= m %% d + n %% d) = ((m + n) %% d < n %% d).
+Proof.
+move=> d_gt0; rewrite modnD//.
+have [d_le|_] := leqP d; last by rewrite subn0 ltnNge leq_addl.
+by rewrite -(ltn_add2r d) mul1n (subnK d_le) addnC ltn_add2l ltn_pmod.
+Qed.
+
+Lemma divnB n m d : 0 < d ->
+  (m - n) %/ d = (m %/ d) - (n %/ d) - (m %% d < n %% d).
 Proof.
-have [-> //| p_gt0] := posnP p; rewrite -ltnS -addnS ltn_divLR // ltnW //.
-rewrite {1}(divn_eq n p) {1}(divn_eq m p) addnACA !mulnDl -3!addnS leq_add2l.
-by rewrite mul2n -addnn -addSn leq_add // ltn_mod.
+move=> d_gt0; have [mn|/ltnW nm] := leqP m n.
+  by rewrite (eqP mn) (eqP (leq_div2r _ _)) ?div0n.
+by rewrite -[in m %/ d](subnK nm) divnD// addnAC addnK leqDmod ?subnK ?addnK.
 Qed.
 
+Lemma modnB m n d : 0 < d -> n <= m ->
+  (m - n) %% d = (m %% d < n %% d) * d + m %% d - n %% d.
+Proof.
+move=> d_gt0 nm; rewrite -[in m %% _](subnK nm) -leqDmod// modnD//.
+have [d_le|_] := leqP d; last by rewrite mul0n add0n subn0 addnK.
+by rewrite mul1n addnBA// addnC !addnK.
+Qed.
+
+Lemma edivnB m n d (offset := m %% d < n %% d) : 0 < d -> n <= m ->
+   edivn (m - n) d = (m %/ d - n %/ d - offset, offset * d + m %% d - n %% d).
+Proof. by move=> d_gt0 le_nm; rewrite edivn_def divnB// modnB. Qed.
+
+Lemma leq_divDl p m n : (m + n) %/ p <= m %/ p + n %/ p + 1.
+Proof. by have [->//|p_gt0] := posnP p; rewrite divnD// !leq_add// leq_b1. Qed.
+
 Lemma geq_divBl k m p : k %/ p - m %/ p <= (k - m) %/ p + 1.
 Proof.
 rewrite leq_subLR addnA; apply: leq_trans (leq_divDl _ _ _).
@@ -478,12 +521,65 @@ Proof.
 by move=> le_mn; rewrite -{1}[n]add0n -{1}(subnK le_mn) eqn_modDr mod0n.
 Qed.
 
+Lemma divnDMl q m d : 0 < d -> (m + q * d) %/ d = (m %/ d) + q.
+Proof. by move=> d_gt0; rewrite addnC divnMDl// addnC. Qed.
+
+Lemma divnMBl q m d : 0 < d -> (q * d - m) %/ d = q - (m %/ d) - (~~ (d %| m)).
+Proof. by move=> d_gt0; rewrite divnB// mulnK// modnMl lt0n. Qed.
+
+Lemma divnBMl q m d : (m - q * d) %/ d = (m %/ d) - q.
+Proof. by case: d => [|d]//=; rewrite divnB// mulnK// modnMl ltn0 subn0. Qed.
+
 Lemma divnDl m n d : d %| m -> (m + n) %/ d = m %/ d + n %/ d.
 Proof. by case: d => // d /divnK{1}<-; rewrite divnMDl. Qed.
 
 Lemma divnDr m n d : d %| n -> (m + n) %/ d = m %/ d + n %/ d.
 Proof. by move=> dv_n; rewrite addnC divnDl // addnC. Qed.
 
+Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)).
+Proof. by case: d => [|d] // /divnK {1}<-; rewrite divnMBl. Qed.
+
+Lemma divnBr m n d : d %| n -> (m - n) %/ d = m %/ d - n %/ d.
+Proof. by case: d => [|d]// /divnK {1}<-; rewrite divnBMl. Qed.
+
+Lemma edivnS m d : 0 < d -> edivn m.+1 d =
+  if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1).
+Proof.
+case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1.
+rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//.
+rewrite addn1 addn0 ltnS; case: (ltngtP _ d.+1) => [ | |->].
+- by rewrite addn0 mul0n subn0.
+- by rewrite ltnNge -ltnS ltn_pmod.
+- by rewrite addn1 mul1n subnn.
+Qed.
+
+Lemma modnS m d : m.+1 %% d = if d %| m.+1 then 0 else (m %% d).+1.
+Proof. by case: d => [|d]//; rewrite modn_def edivnS//; case: ifP. Qed.
+
+Lemma divnS m d : 0 < d -> m.+1 %/ d = (d %| m.+1) + m %/ d.
+Proof. by move=> d_gt0; rewrite /divn edivnS//; case: ifP. Qed.
+
+Lemma divn_pred m d : m.-1 %/ d = (m %/ d) - (d %| m).
+Proof.
+by case: d m => [|d] [|m]; rewrite ?divn1 ?dvd1n ?subn1//= divnS// addnC addnK.
+Qed.
+
+Lemma modn_pred m d : d != 1 -> 0 < m ->
+  m.-1 %% d = if d %| m then d.-1 else (m %% d).-1.
+Proof.
+rewrite -subn1; case: d m => [|[|d]] [|m]//= _ _.
+  by rewrite ?modn1 ?dvd1n ?modn0 ?subn1.
+rewrite modnB// (@modn_small 1)// [_ < _]leqn0 /dvdn mulnbl/= subn1.
+by case: ifP => // /eqP->; rewrite addn0.
+Qed.
+
+Lemma edivn_pred m d : d != 1 -> 0 < m ->
+  edivn m.-1 d = if d %| m then ((m %/ d).-1, d.-1) else (m %/ d, (m %% d).-1).
+Proof.
+move=> d_neq1 m_gt0; rewrite edivn_def divn_pred modn_pred//.
+by case: ifP; rewrite ?subn0 ?subn1.
+Qed.
+
 (***********************************************************************)
 (*   A function that computes the gcd of 2 numbers                     *)
 (***********************************************************************)
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 3b7524e..746eafc 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -279,6 +279,9 @@ Proof. by move=> m; rewrite /= -{2}[n]addn0 subnDl subn0. Qed.
 Lemma addnK n : cancel (addn^~ n) (subn^~ n).
 Proof. by move=> m; rewrite /= (addnC m) addKn. Qed.
 
+Lemma addnKC n m : (n + m) - n = m.
+Proof. by rewrite addnC addnK. Qed.
+
 Lemma subSnn n : n.+1 - n = 1.
 Proof. exact (addnK n 1). Qed.
 
@@ -326,6 +329,12 @@ Hint Resolve leqnSn : core.
 Lemma leq_pred n : n.-1 <= n.           Proof. by case: n => /=. Qed.
 Lemma leqSpred n : n <= n.-1.+1.        Proof. by case: n => /=. Qed.
 
+Lemma ltn_predl n : (n.-1 < n) = (n != 0).
+Proof. by case: n => [//|n]; rewrite ltnSn. Qed.
+
+Lemma ltn_predr m n : (m < n.-1) = (m.+1 < n).
+Proof. by case: n => [//|n]; rewrite succnK. Qed.
+
 Lemma ltn_predK m n : m < n -> n.-1.+1 = n.
 Proof. by case: n. Qed.
 
@@ -532,6 +541,9 @@ Proof. by move=> le_pm le_pn; rewrite addnBA // addnBAC. Qed.
 Lemma subnBA m n p : p <= n -> m - (n - p) = m + p - n.
 Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) subnDr. Qed.
 
+Lemma ltn_subr m n : m <= n -> (n - m < n) = (m > 0).
+Proof. by move=> le_mn; rewrite -subn_gt0 subnBA// addnKC. Qed.
+
 Lemma subKn m n : m <= n -> n - (n - m) = m.
 Proof. by move/subnBA->; rewrite addKn. Qed.
 
@@ -541,6 +553,9 @@ Proof. by rewrite -add1n => /addnBA <-. Qed.
 Lemma subnSK m n : m < n -> (n - m.+1).+1 = n - m.
 Proof. by move/subSn. Qed.
 
+Lemma predn_sub m n : (m - n).-1 = (m.-1 - n).
+Proof. by case: m => // m; rewrite subSKn. Qed.
+
 Lemma leq_sub2r p m n : m <= n -> m - p <= n - p.
 Proof.
 by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR.
@@ -564,6 +579,36 @@ Proof. by move/subnSK <-; apply: leq_sub2l. Qed.
 Lemma ltn_subRL m n p : (n < p - m) = (m + n < p).
 Proof. by rewrite !ltnNge leq_subLR. Qed.
 
+Lemma leq_psubRL m n p : 0 < n -> (n <= p - m) = (m + n <= p).
+Proof. by move=> /prednK<-; rewrite ltn_subRL addnS. Qed.
+
+Lemma ltn_psubLR m n p : 0 < p -> (m - n < p) = (m < n + p).
+Proof. by move=> /prednK<-; rewrite ltnS leq_subLR addnS. Qed.
+
+Lemma leq_subRL m n p : m <= p -> (n <= p - m) = (m + n <= p).
+Proof. by move=> /subnKC{2}<-; rewrite leq_add2l. Qed.
+
+Lemma ltn_subLR m n p : n <= m -> (m - n < p) = (m < n + p).
+Proof. by move=> /subnKC{2}<-; rewrite ltn_add2l. Qed.
+
+Lemma leq_subCl m n p : (m - n <= p) = (m - p <= n).
+Proof. by rewrite !leq_subLR // addnC. Qed.
+
+Lemma ltn_subCr m n p : (p < m - n) = (n < m - p).
+Proof. by rewrite !ltn_subRL // addnC. Qed.
+
+Lemma leq_psubCr m n p : 0 < p -> 0 < n -> (p <= m - n) = (n <= m - p).
+Proof. by move=> p_gt0 n_gt0; rewrite !leq_psubRL // addnC. Qed.
+
+Lemma ltn_psubCl m n p : 0 < p -> 0 < n -> (m - n < p) = (m - p < n).
+Proof. by move=> p_gt0 n_gt0; rewrite !ltn_psubLR // addnC. Qed.
+
+Lemma leq_subCr m n p : n <= m -> p <= m -> (p <= m - n) = (n <= m - p).
+Proof. by move=> np pm; rewrite !leq_subRL // addnC. Qed.
+
+Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n).
+Proof. by move=> nm pm; rewrite !ltn_subLR // addnC. Qed.
+
 (* Eliminating the idiom for structurally decreasing compare and subtract. *)
 Lemma subn_if_gt T m n F (E : T) :
   (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).