use mathcomp's log

src/bintree.v

@@ -313,16 +313,16 @@ apply/leq_trans/(exp_h_geq t).
 by rewrite !size1_size leq_add2r.
 Qed.
 
-Lemma acomplete_h t : acomplete t -> height t = log2n (size1_tree t).
+Lemma acomplete_h t : acomplete t -> height t = up_log 2 (size1_tree t).
 Proof.
 case/boolP: (complete t).
-- by move/completeE=>->_; rewrite exp2nK.
+- by move/completeE=>->_; rewrite up_expnK.
 move=>/[dup] H /[swap] /acomplete_h1 /[apply] E; rewrite E; symmetry.
-apply: log2n_eq; rewrite (ncomplete_mh_size1 H) /= -E.
+apply: up_log_eq=>//; rewrite (ncomplete_mh_size1 H) /= -E.
 by exact: exp_h_geq.
 Qed.
 
-Lemma acomplete_mh t : acomplete t -> min_height t = trunc_log' 2 (size1_tree t).
+Lemma acomplete_mh t : acomplete t -> min_height t = trunc_log 2 (size1_tree t).
 Proof.
 case/boolP: (complete t).
 - move/[dup]/complete_mh_h/eqP=>->.
@@ -419,7 +419,7 @@ Proof. by rewrite /balance_tree bal_tree_take // take_oversize // size_inorder.
 
 Lemma bal_h_mh n xs t ss :
   n <= size xs -> bal n xs = (t, ss) ->
-  height t = log2n n.+1 /\ min_height t = trunc_log' 2 n.+1.
+  height t = up_log 2 n.+1 /\ min_height t = trunc_log 2 n.+1.
 Proof.
 elim/ltn_ind: n xs t ss; case.
 - by move=>_ ??? _; simp bal=>/=; case=><-.
@@ -442,8 +442,8 @@ have Hmm : m' <= m.
 - rewrite /m' (half_uphalfK n) /m addnK uphalf_half.
   by apply: leq_addl.
 rewrite -(leq_add2r 1) !addn1 in Hmm.
-rewrite /maxn /minn !ltnNge leq_log2n // leq_trunc_log //=.
-rewrite (log2nS (isT : 0 < n.+1)) (trunc_log2S (isT : 1 < n.+2)); split.
+rewrite /maxn /minn !ltnNge leq_up_log // leq_trunc_log //=.
+rewrite (up_log2S (isT : 0 < n.+1)) (trunc_log2S (isT : 1 < n.+2)); split.
 - by rewrite -addn1 addn1.
 rewrite /m' /m {1}(half_uphalfK n) addnK.
 by rewrite -(addn2 n) halfD /= andbF /= add0n !addn1.
@@ -454,8 +454,8 @@ Corollary bal_acomplete n xs t ss :
 Proof.
 rewrite /acomplete.
 move/bal_h_mh => /[apply] [[->->]].
-have /andP [H1 H2] := trunc_up_log_ltn n.+1.
-by rewrite -(leq_add2r (trunc_log' 2 n.+1)) addnBAC // addnK addnC.
+have/andP [H1 H2] := trunc_up_log_ltn n.+1 (isT : 1 < 2).
+by rewrite -(leq_add2r (trunc_log 2 n.+1)) addnBAC // addnK addnC.
 Qed.
 
 (* Exercise 4.3 *)

src/braun.v

@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat seq.
+From mathcomp Require Import eqtype ssrnat seq prime.
 From favssr Require Import prelude bintree.
 
 Set Implicit Arguments.
@@ -45,14 +45,14 @@ Lemma acomplete_compose (l : tree A) x r :
   acomplete (Node l x r).
 Proof.
 move=>Hl Hr E; rewrite /acomplete.
-have/eqP->: height (Node l x r) == log2n (size1_tree r + 1) + 1.
+have/eqP->: height (Node l x r) == up_log 2 (size1_tree r + 1) + 1.
 - rewrite /= eqn_add2r (acomplete_h Hl) (acomplete_h Hr) size1_size (eqP E) -size1_size.
-  by apply/eqP/maxn_idPl/leq_log2n/leq_addr.
-have/eqP->: min_height (Node l x r) == trunc_log' 2 (size1_tree r) + 1.
+  by apply/eqP/maxn_idPl/leq_up_log/leq_addr.
+have/eqP->: min_height (Node l x r) == trunc_log 2 (size1_tree r) + 1.
 - rewrite /= eqn_add2r (acomplete_mh Hl) (acomplete_mh Hr) size1_size (eqP E) -size1_size.
   by apply/eqP/minn_idPr/leq_trunc_log/leq_addr.
 rewrite -subnBA ?addnK; last by rewrite addn1.
-rewrite log2_trunc_log; last by rewrite size1_size !addn1.
+rewrite up_log_trunc_log //; last by rewrite size1_size !addn1.
 by rewrite addn1 /= subSnn.
 Qed.
 

src/prelude.v

@@ -292,191 +292,20 @@ Proof. by move=>H; apply: eq_all=>z /=; apply: perm_all. Qed.
 
 End Allrel.
 
-Section TruncLog.
+Section Log.
 
-(* TODO added to Mathcomp in https://github.com/math-comp/math-comp/pull/823, should be available in 1.14 *)
-
-Definition trunc_log' p n :=
-  let fix loop n k :=
-    if k is k'.+1 then if p <= n then (loop (n %/ p) k').+1 else 0 else 0
-  in if p <= 1 then 0 else loop n n.
-
-Lemma trunc_log0 p : trunc_log' p 0 = 0.
-Proof. by case: p => [] // []. Qed.
-
-Lemma trunc_log0n n : trunc_log' 0 n = 0.
-Proof. by []. Qed.
-
-Lemma trunc_log_bounds p n :
-  1 < p -> 0 < n -> let k := trunc_log' p n in p ^ k <= n < p ^ k.+1.
-Proof.
-rewrite {+}/trunc_log' => p_gt1; have p_gt0 := ltnW p_gt1.
-rewrite [p <= 1]leqNgt p_gt1 /=.
-set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m.
-have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _.
-have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //.
-by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)).
-Qed.
-
-Lemma trunc_logP p n : 1 < p -> 0 < n -> p ^ trunc_log' p n <= n.
-Proof. by move=> p_gt1 /(trunc_log_bounds p_gt1)/andP[]. Qed.
-
-Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log' p n).+1.
-Proof.
-have [-> | n_gt0] := posnP n; first by rewrite trunc_log0 => /ltnW.
-by case/trunc_log_bounds/(_ n_gt0)/andP.
-Qed.
-
-Lemma trunc_log_max p k j : 1 < p -> p ^ j <= k -> j <= trunc_log' p k.
-Proof.
-move=> p_gt1 le_pj_k; rewrite -ltnS -(@ltn_exp2l p) //.
-exact: leq_ltn_trans (trunc_log_ltn _ _).
-Qed.
-
-Lemma leq_trunc_log p m n : m <= n -> trunc_log' p m <= trunc_log' p n.
-Proof.
-move=> mlen; case: p => [|[|p]]; rewrite ?trunc_log0n ?trunc_log1n //.
-case: m mlen => [|m] mlen; first by rewrite trunc_log0.
-apply/trunc_log_max => //; apply: leq_trans mlen; exact: trunc_logP.
-Qed.
-
-Lemma trunc_log_eq p n k : 1 < p -> p ^ n <= k < p ^ n.+1 -> trunc_log' p k = n.
-Proof.
-move=> p_gt1 /andP[npLk kLpn]; apply/anti_leq.
-rewrite trunc_log_max// andbT -ltnS -(ltn_exp2l _ _ p_gt1).
-apply: leq_ltn_trans kLpn; apply: trunc_logP => //.
-by apply: leq_trans npLk; rewrite expn_gt0 ltnW.
-Qed.
-
-Lemma trunc_expnK p n : 1 < p -> trunc_log' p (p ^ n) = n.
-Proof. by move=> ?; apply: trunc_log_eq; rewrite // leqnn ltn_exp2l /=. Qed.
-
-Lemma trunc_logMp p n : 1 < p -> 0 < n ->
-  trunc_log' p (p * n) = (trunc_log' p n).+1.
-Proof.
-case: p => [//|p] => p_gt0 n_gt0; apply: trunc_log_eq => //.
-rewrite expnS leq_pmul2l// trunc_logP//=.
-by rewrite expnS ltn_pmul2l// trunc_log_ltn.
-Qed.
-
-Lemma trunc_log2_double n : 0 < n -> trunc_log' 2 n.*2 = (trunc_log' 2 n).+1.
-Proof. by move=> n_gt0; rewrite -mul2n trunc_logMp. Qed.
-
-Lemma trunc_log2S n : 1 < n -> trunc_log' 2 n = (trunc_log' 2 n./2).+1.
-Proof.
-move=> n_gt1.
-rewrite -trunc_log2_double ?half_gt0//.
-rewrite -[n in LHS]odd_double_half.
-case: odd => //; rewrite add1n.
-apply: trunc_log_eq => //.
-rewrite leqW ?trunc_logP //= ?double_gt0 ?half_gt0//.
-rewrite trunc_log2_double ?half_gt0// expnS.
-by rewrite -doubleS mul2n leq_double trunc_log_ltn.
-Qed.
-
-End TruncLog.
-
-Section Log2.
-
-(* ceiling of log_2, from https://github.com/thery/mathcomp-extra/blob/master/more_thm.v *)
-(* TODO added to Mathcomp in https://github.com/math-comp/math-comp/pull/823, should be available in 1.14 *)
-Definition log2n n :=
-  let v := trunc_log' 2 n in if n <= 2 ^ v then v else v.+1.
-
-Lemma up_log0 : log2n 0 = 0.
-Proof. by []. Qed.
-
-Lemma log2n_eq0 n : (log2n n == 0) = (n <= 1).
-Proof.
-case: n => [|[|n]]; rewrite /log2n //.
-have /= := trunc_log_bounds (isT : 1 < 2) (isT : 0 < n.+2).
-by case: (leqP _ n.+1).
-Qed.
-
-Lemma log2n_gt0 n : (0 < log2n n) = (1 < n).
-Proof. by rewrite ltnNge leqn0 log2n_eq0 ltnNge. Qed.
-
-Lemma log2n_bounds n :
-  1 < n -> let k := log2n n in 2 ^ k.-1 < n <= 2 ^ k.
-Proof.
-move=> /= n_gt1.
-have n_gt0 : 0 < n by apply: leq_trans n_gt1.
-rewrite /log2n.
-have /= /andP[t2Ln nLt2S] := trunc_log_bounds (isT : 1 < 2) n_gt0.
-have [nLn2|n2Ln] := leqP n (2 ^ trunc_log' 2 n); last by rewrite n2Ln ltnW.
-rewrite nLn2 (leq_trans _ t2Ln) // ltn_exp2l // prednK ?leqnn //.
-by case: trunc_log' (leq_trans n_gt1 nLn2).
-Qed.
-
-Lemma log2n_geq n : n <= 2 ^ log2n n.
-Proof.
-by case: n => [|[|n]] //; have /andP[] := log2n_bounds (isT: 1 < n.+2).
-Qed.
-
-Lemma log2n_ltn n : 1 < n -> 2 ^ (log2n n).-1 < n.
-Proof.
-by case: n => [|[|n]] _ //; have /andP[] := log2n_bounds (isT: 1 < n.+2).
-Qed.
-
-Lemma log2n_exp k j : k <= 2 ^ j -> log2n k <= j.
-Proof.
-case: k => [|[|k]] // kLj.
-rewrite -[log2n _]prednK ?log2n_gt0 // -(@ltn_exp2l 2) //.
-by apply: leq_trans (log2n_ltn (isT : 1 < k.+2)) _.
-Qed.
-
-Lemma leq_log2n m n : m <= n -> log2n m <= log2n n.
-Proof. by move=> mLn; apply/log2n_exp/(leq_trans _ (log2n_geq _)). Qed.
-
-Lemma log2n_eq n k : 2 ^ n < k <= 2 ^ n.+1 -> log2n k = n.+1.
-Proof.
-case/andP=>n2Lk kL2n; apply/eqP; rewrite eqn_leq.
-apply/andP; split; first by apply: log2n_exp.
-rewrite -(ltn_exp2l _ _ (_ : 1 < 2)) //.
-by apply: leq_trans n2Lk (log2n_geq k).
-Qed.
-
-Lemma exp2nK n : log2n (2 ^ n) = n.
-Proof. by case: n=>//= n; apply: log2n_eq; rewrite leqnn andbT ltn_exp2l. Qed.
-
-Lemma log2nS n : 1 <= n -> log2n n.+1 = (log2n (n./2.+1)).+1.
-Proof.
-case: n=> // [] [|n] // _.
-apply/log2n_eq/andP; split.
-- apply: leq_trans (_ : n./2.+1.*2 < n.+3); last first.
-  by rewrite doubleS !ltnS -[X in _ <= X]odd_double_half leq_addl.
-- have /= /andP[H1n _] := log2n_bounds (isT : 1 < n./2.+2).
-  by rewrite ltnS -leq_double -mul2n -expnS prednK ?log2n_gt0 // in H1n.
-rewrite -[_./2.+1]/(n./2.+2).
-have /= /andP[_ H2n] := log2n_bounds (isT : 1 < n./2.+2).
-rewrite -leq_double -!mul2n -expnS in H2n.
-apply: leq_trans H2n.
-rewrite mul2n !doubleS !ltnS.
-by rewrite -[X in X <= _]odd_double_half -add1n leq_add2r; case: odd.
-Qed.
-
-Lemma trunc_up_log_ltn n :
-  trunc_log' 2 n <= log2n n <= trunc_log' 2 n + 1.
+Lemma trunc_up_log_ltn p n :
+  1 < p -> trunc_log p n <= up_log p n <= trunc_log p n + 1.
 Proof.
+move=>Hp.
 apply/andP; split.
 - case: n; first by rewrite up_log0 trunc_log0.
-  move=>n; rewrite -(@leq_exp2l 2) //.
-  apply: (leq_trans (n:=n.+1)).
-  - by apply: trunc_logP.
-  by apply: log2n_geq.
-apply: log2n_exp.
-by rewrite addn1; apply/ltnW/trunc_log_ltn.
-Qed.
-
-Lemma log2_trunc_log n :
-  1 < n -> log2n n = (trunc_log' 2 n.-1).+1.
-Proof.
-move=> n_gt1; apply: log2n_eq => //.
-rewrite -[n]prednK ?ltnS -?pred_Sn ?[0 < n]ltnW//.
-by rewrite trunc_logP ?ltn_predRL// trunc_log_ltn.
+  move=>n; rewrite -(@leq_exp2l p) //.
+  by apply: (leq_trans (n:=n.+1)); [apply: trunc_logP | apply: up_logP].
+by apply: up_log_min=>//; rewrite addn1; apply/ltnW/trunc_log_ltn.
 Qed.
 
-End Log2.
+End Log.
 
 Section UpDiv.
 

src/selection.v

@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq path order bigop div ssrnum ssralg ssrint.
+From mathcomp Require Import ssrnat eqtype seq path order bigop div ssrnum ssralg ssrint prime.
 From favssr Require Import prelude sorting.
 Set Implicit Arguments.
 Unset Strict Implicit.

src/sorting.v

@@ -1,6 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq path order bigop.
+From mathcomp Require Import ssrnat eqtype seq path order bigop prime.
 From favssr Require Import prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -607,11 +607,11 @@ by rewrite catA !size_cat H size_merge size_cat.
 Qed.
 
 Lemma C_merge_adj_log2 xss :
-  C_merge_all xss <= size (flatten xss) * log2n (size xss).
+  C_merge_all xss <= size (flatten xss) * up_log 2 (size xss).
 Proof.
 funelim (C_merge_all xss)=>//=; move: H; simp C_merge_adj merge_adj.
 rewrite /= !size_cat merge_adj_flat size_merge_adj size_merge size_cat =>IH.
-rewrite log2nS //= mulnS !addnA; apply: leq_add=>//.
+rewrite up_log2S //= mulnS !addnA; apply: leq_add=>//.
 by apply/leq_add/C_merge_adj_flat/C_merge_leq.
 Qed.
 
@@ -679,17 +679,17 @@ Lemma C_size_runs_leq xs : (C_runs xs <= (size xs).-1)%N.
 Proof. by case: xs=>//=x xs; case: (C_size_runs_asc_desc_leq x xs). Qed.
 
 Lemma C_merge_runs_leq xs n :
-  size xs = n -> (C_merge_all (runs xs) <= n * log2n n)%N.
+  size xs = n -> (C_merge_all (runs xs) <= n * up_log 2 n)%N.
 Proof.
 move=>H; apply: leq_trans; first by apply: C_merge_adj_log2.
 rewrite size_runs H leq_mul2l; apply/orP.
 case: n H=>[H|n H]; first by left.
-right; apply: leq_log2n; rewrite -H.
+right; apply: leq_up_log; rewrite -H.
 by apply: size_runs_leq.
 Qed.
 
 Lemma C_nmsort_leq xs n :
-  size xs = n -> (C_nmsort xs <= n + n * log2n n)%N.
+  size xs = n -> (C_nmsort xs <= n + n * up_log 2 n)%N.
 Proof.
 move=>H; rewrite /C_nmsort; apply/leq_add/C_merge_runs_leq=>//.
 apply: leq_trans; first by apply: C_size_runs_leq.