Hakyber jasmin eclib

theories/algebra/IntDiv.ec

@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import Core Int IntMin Ring StdOrder.
+require import Core Int IntMin Ring StdOrder List.
 (*---*) import Ring.IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
@@ -514,6 +514,14 @@ lemma nosmt eqz_mul d m n : d <> 0 => d %| m =>
   (m = n * d) <=> (m %/ d = n).
 proof. by move=> d_gt0 dv_d_m; rewrite eq_sym -eqz_div // eq_sym. qed.
 
+lemma divz_eqP (m d n : int) :
+  0 < d => m %/ d = n <=> n * d <= m < (n + 1) * d.
+proof.
+  move => lt0d; split => [<<-|[le_m ltm_]].
+  + by split => [|_]; [apply/lez_floor/gtr_eqF|apply/ltz_ceil].
+  by apply/eqz_leq; split; [apply/ltzS/ltz_divLR|apply/lez_divRL].
+qed.
+
 lemma nosmt leq_div2r (d m n : int) :
   m <= n => 0 <= d => m %/ d <= n %/ d.
 proof.
@@ -568,6 +576,47 @@ qed.
 lemma nosmt divzDr m n d : d %| n => (m + n) %/ d = (m %/ d) + (n %/ d).
 proof. by move=> dv_n; rewrite addrC divzDl // addrC. qed.
 
+lemma divz_mulp (n d1 d2 : int) : 
+  0 < d1 =>
+  0 < d2 =>
+  n %/ (d1 * d2) = n %/ d1 %/ d2.
+proof.
+  move => lt0d1 lt0d2; rewrite (mulzC d1); apply divz_eqP; [by apply mulr_gt0|split => [|_]].
+  + by rewrite mulrA; apply (lez_trans (n %/ d1 * d1));
+    [apply/ler_pmul2r => //|]; apply/lez_floor/gtr_eqF.
+  by rewrite mulrA; apply (ltr_le_trans ((n %/ d1 + 1) * d1));
+  [|apply/ler_pmul2r => //; apply/ltzE]; apply/ltz_ceil.
+qed.
+
+lemma divz_mul (n d1 d2 : int) :
+  0 <= d1 =>
+  n %/ (d1 * d2) = n %/ d1 %/ d2.
+proof.
+move => /lez_eqVlt [<<- //=|lt0d1];
+(case (0 <= d2) => [/lez_eqVlt [<<- //=|lt0d2]|/ltzNge ltd20]).
+(*FIXME: why no automatic rewriting here for divz0 and div0z?*)
++ by rewrite !divz0.
++ by rewrite !divz0 div0z.
++ by rewrite !divz0 div0z.
++ by rewrite !divz0.
++ by rewrite divz_mulp.
+by rewrite -(oppzK d2) mulrN 2!divzN eqr_opp divz_mulp // ltr_oppr.
+qed.
+
+lemma divzpMr p m d : d %| m => p * (m %/ d) = p * m %/ d.
+proof. by move => /dvdzP [q ->>]; case (d = 0) => [->> /=|neqd0]; [rewrite divz0|rewrite mulrA !mulzK]. qed.
+
+lemma dvdNdiv x y : x <> 0 => x %| y => (-y) %/ x = - y %/ x.
+proof. by move => neqx0 /dvdzP [z ->>]; rewrite -mulNr !mulzK. qed.
+
+lemma exprD_subz (x m n : int) : x <> 0 => 0 <= n <= m => x ^ (m - n) = (x ^ m) %/ (x ^ n).
+proof.
+move => neqx0 [le0n lenm]; rewrite eq_sym -(eqz_mul (x ^ n) (x ^ m) (x ^ (m - n))).
++ by move: neqx0; rewrite implybNN expf_eq0.
++ by apply dvdz_exp2l.
+by rewrite -exprD_nneg ?subrK // ler_subr_addr.
+qed.
+
 lemma nosmt expz_div (x n m : int) :
   0 <= m <= n => 0 < x => x^n %/ x^m = x^(n-m).
 proof.
@@ -856,6 +905,178 @@ move=> lt_pn; rewrite {1}(divz_eq i (k^n)); rewrite -addrA; congr.
 by rewrite {1}(divz_eq (i %% k^n) (k^p)) modz_dvd_pow.
 qed.
 
+lemma dvdz_mod_div d1 d2 m :
+  0 < d1 =>
+  0 < d2 =>
+  d2 %| d1 =>
+  m %% d1 %/ d2 = (m %/ d2) %% (d1 %/ d2).
+proof.
+  move => lt0d1 lt0d2 /dvdzP [q ->>]; rewrite modzE mulrA -mulNr mulzK; first by rewrite gtr_eqF.
+  rewrite divzMDr //; first by rewrite gtr_eqF.
+  rewrite addrC modzE; do 2!congr.
+  by rewrite (mulrC q) divz_mulp // -(pmulr_lgt0 _ _ lt0d2).
+qed.
+
+lemma modz_pow_div x n p m :
+  0 < x =>
+  0 <= p <= n =>
+  m %% x ^ n %/ x ^ p = (m %/ x ^ p) %% (x ^ (n - p)).
+proof.
+  by move => lt0x [le0p lepn]; rewrite dvdz_mod_div //;
+  [apply expr_gt0|apply expr_gt0|apply dvdz_exp2l|rewrite exprD_subz // gtr_eqF].
+qed.
+
+lemma modz_pow2_div n p m :
+  0 <= p <= n =>
+  m %% 2 ^ n %/ 2 ^ p = (m %/ 2 ^ p) %% (2 ^ (n - p)).
+proof. by apply modz_pow_div. qed.
+
+(* ==================================================================== *)
+lemma pow_normr (p x : int) :
+  p ^ x = p ^ `|x|.
+proof.
+by rewrite normE; case (0 <= x) => //; rewrite exprN. qed.
+
+lemma lt_pow (p x : int) :
+  1 < p =>
+  x < p ^ x.
+proof.
+  move => lt1p; case (0 <= x) => [|/ltzNge ltx0]; last by apply/(ltr_le_trans _ _ _ ltx0)/expr_ge0/ltzW/ltzE/ltzW.
+  elim x => [|x le0x ltxpow]; first by rewrite expr0.
+  apply/(ler_lt_trans (p ^ x)); first by apply/ltzE.
+  by rewrite exprSr // ltr_pmulr // expr_gt0 ltzE ltzW.
+qed.
+
+lemma Ndvd_pow (p x : int) :
+  1 < `|p| =>
+  x <> 0 =>
+  ! p ^ x %| x.
+proof.
+  move => lt1norm neqx0; apply/negP => dvdpowx.
+  move: (dvdz_le _ _ _ dvdpowx) => //.
+  rewrite pow_normr normrX_nat ?normr_ge0 //; apply/negP/ltzNge.
+  by apply/lt_pow.
+qed.
+
+lemma dvdz2_eq m n :
+  0 <= m =>
+  0 <= n =>
+  m %| n =>
+  n %| m =>
+  m = n.
+proof.
+  move => le0m le0n /dvdzP [x ->>] /dvdzP [y /(congr1 (transpose (%/) m) _ _) /=].
+  rewrite mulrA divzz; case (m = 0) => /= [->> //=|neqm0]. 
+  rewrite /b2i mulzK //= => eq1mul; move: (unitrM y x); move: eq1mul => <- /=.
+  move => [_ [|] ->> //=]; move: le0n; rewrite mulNr /= oppr_ge0 => lem0.
+  by move: neqm0; rewrite eqz_leq lem0 le0m.
+qed.
+
+lemma dvd_le_pow (p m n : int) :
+  1 < `|p| =>
+  p ^ m %| p ^ n =>
+  `|m| <= `|n|.
+proof.
+  rewrite (pow_normr p m) (pow_normr p n) => lt1norm dvdpow2.
+  have:= (dvdz_le _ _ _ dvdpow2); first by rewrite expf_eq0 -negP => -[_ ->>].
+  rewrite !normrX_nat ?normr_ge0 //.
+  by apply ler_weexpn2r => //; apply normr_ge0.
+qed.
+
+lemma le_dvd_pow (p m n : int) :
+  `|m| <= `|n| =>
+  p ^ m %| p ^ n.
+proof.
+  rewrite (pow_normr p m) (pow_normr p n) => lenormr2.
+  apply/dvdzP; exists (p ^ (`|n| - `|m|)).
+  by rewrite -exprD_nneg; [apply subr_ge0|apply normr_ge0|rewrite -addrA].
+qed.
+
+(*-----------------------------------------------------------------------------*)
+
+lemma eq_range m n : m = n <=> m \in range n (n+1).
+proof. by rewrite mem_range ltzS eqz_leq. qed.
+
+lemma range_div_range m d min max : 0 < d => m %/ d \in range min max <=> m \in range (min * d) (max * d).
+proof.
+move => lt0d; rewrite !mem_range !andabP; apply andb_id2.
++ by apply lez_divRL.
+by rewrite -ltz_divLR // ltzS.
+qed.
+
+lemma eq_div_range m d n : 0 < d => m %/ d = n <=> m \in range (n * d) ((n + 1) * d).
+proof. by move => lt0d; rewrite eq_range range_div_range. qed.
+
+(*-----------------------------------------------------------------------------*)
+abbrev (%\) (m d : int) : int = - ((- m) %/ d).
+
+lemma lez_ceil m d : d <> 0 => m <= m %\ d * d.
+proof. by rewrite mulNr => neqd0; apply/ler_oppr/lez_floor. qed.
+
+lemma ltz_floor m d : 0 < d => (m %\ d - 1) * d < m.
+proof. by rewrite -opprD mulNr => lt0d; apply/ltr_oppl/ltz_ceil. qed.
+
+lemma lez_NdivNLR (d m n : int) : 0 < d => d %| n => m <= n %\ d <=> m * d <= n.
+proof.
+move => lt0d dvddn; rewrite ler_oppr lez_divLR //; first by apply dvdzN.
+by rewrite mulNr ler_opp2.
+qed.
+
+lemma lez_NdivNRL (m n d : int) : 0 < d => m %\ d <= n <=> m <= n * d.
+proof. by move => lt0d; rewrite ler_oppl lez_divRL // mulNr ler_opp2. qed.
+
+lemma ltz_NdivNLR (m n d : int) : 0 < d => m < n %\ d <=> m * d < n.
+proof. by move => lt0d; rewrite ltr_oppr ltz_divLR // mulNr ltr_opp2. qed.
+
+lemma ltz_NdivNRL (d m n : int) : 0 < d => d %| m => m %\ d < n  <=> m < n * d.
+move => lt0d dvddm; rewrite ltr_oppl ltz_divRL //; first by apply dvdzN.
+by rewrite mulNr ltr_opp2.
+qed.
+
+(*-----------------------------------------------------------------------------*)
+
+lemma mem_range_mull (m n x y : int) :
+  0 < x =>
+  x * y \in range m n <=> y \in range (m %\ x) (n %\ x).
+proof. by move => lt0x; rewrite !mem_range lez_NdivNRL // ltz_NdivNLR // !(mulrC y). qed.
+
+lemma mem_range_mulr (m n x y : int) :
+  0 < y =>
+  x * y \in range m n <=> x \in range (m %\ y) (n %\ y).
+proof. by rewrite mulrC; apply/mem_range_mull. qed.
+
+lemma mem_range_mod (x y : int) :
+  y <> 0 =>
+  x %% y \in range 0 `|y|.
+proof. by move => neqy0; rewrite mem_range modz_ge0 // ltz_mod. qed.
+
+lemma mem_range_add_mul (m n l x y : int) :
+  x \in range 0 l =>
+  y \in range m n =>
+  x + l * y \in range (m * l) (n * l).
+proof.
+  move => Hx_range Hy_range; rewrite mem_range_addl mem_range_mull; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+  move: Hy_range; apply/mem_range_incl.
+  + rewrite lez_NdivNRL; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+    by rewrite ler_subl_addr ler_addl; move/mem_range: Hx_range.
+  rewrite -ltzS -ltr_subl_addr ltz_NdivNLR; first by apply/(ler_lt_trans x); move/mem_range: Hx_range.
+  by rewrite mulrDl mulNr /= ler_lt_sub //; move/mem_range: Hx_range.
+qed.
+
+lemma mem_range_add_mul_eq (x1 y1 x2 y2 l : int) :
+  x1 \in range 0 l =>
+  x2 \in range 0 l =>
+  x1 + l * y1 = x2 + l * y2 <=>
+  x1 = x2 /\ y1 = y2.
+proof.
+  move => /mem_range [le0x1 ltx1l] /mem_range [le0x2 ltx2l]; split => [Heq|[->> ->>] //]; split.
+  + move: (congr1 (transpose (%%)%IntID l) _ _ Heq) => /=.
+    by rewrite !(mulrC l) !modzMDr !pmod_small.
+  move: (congr1 (transpose (%/)%IntID l) _ _ Heq) => /=.
+  rewrite !(mulrC l) !divzMDr; try by apply/gtr_eqF/(ler_lt_trans x1).
+  by rewrite !pdiv_small.
+qed.
+
 lemma nosmt divzMr i a b :  
   0 <= a => 0 <= b => i %/ (a * b) = i %/ a %/ b.
 proof.
@@ -877,13 +1098,15 @@ lemma nosmt divzMl i a b :
   0 <= a => 0 <= b => i %/ (a * b) = i %/ b %/ a.
 proof. by move=> *; rewrite mulrC divzMr. qed.
 
+(*
 lemma nosmt modz_pow2_div n p i: 
   0 <= p <= n => (i %% 2^n) %/ 2^p = (i %/ 2^p) %% 2^(n-p).
 proof.
 move=> [ge0_p len_p].
 rewrite !modzE (: 2^n = 2^(n-p) * 2^p) 1:-exprD_nneg 1:subr_ge0 3:subrK //.
 by rewrite -mulNr mulrA divzMDr 1:expf_eq0 // mulNr addrC divzMl 1,2:expr_ge0.
 qed.
+*)
 
 (* -------------------------------------------------------------------- *)
 require import Real.

theories/algebra/Number.ec

@@ -350,6 +350,25 @@ proof. by rewrite ltr_neqAle normr_le0 normr0P; case: (_ = _). qed.
 lemma nosmt normr_gt0 (x : t): (zeror < `|x|) <=> (x <> zeror).
 proof. by rewrite ltr_def normr0P normr_ge0; case: (_ = _). qed.
 
+lemma nosmt unit_normr (x : t): unit (`|x|) => unit x.
+proof.
+case: (real_axiom x) => [le0n|len0].
+  by move: (normr_idP x); rewrite le0n /= => ->.
+by rewrite ler0_norm // unitrN.
+qed.
+
+lemma nosmt normrX n (x : t) : `|exp x n| = exp `|x| n.
+proof.
+case (0 <= n); [by apply normrX_nat|].
+rewrite -ltzNge -{1}(invrK x) exprV => ltn0.
+rewrite normrX_nat; [by rewrite oppz_ge0 ltzW|].
+case: (unit x) => [unitx|Nunitx].
+  by rewrite normrV // exprV.
+move: (unit_normr x) => /contra; rewrite Nunitx /=.
+move => unitNx; rewrite invr_out //.
+by rewrite -{1}(@invr_out `|_|) // exprV.
+qed.
+
 (*-------------------------------------------------------------------- *)
 hint rewrite normrE : normr_id normr0 normr1 normrN1.
 hint rewrite normrE : normr_ge0 normr_lt0 normr_le0 normr_gt0.
@@ -729,7 +748,10 @@ proof. by rewrite ltrNge. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma leVge x y : (x <= y) \/ (y <= x).
-proof. by case: (x <= y) => // /ltrNge /ltrW. qed.
+proof. exact ler_total. qed.
+
+lemma leVgt x y : (x <= y) \/ (y < x).
+proof. by case: (x <= y) => // /ltrNge. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma nosmt ltrN10: -oner < zeror.
@@ -1099,6 +1121,14 @@ rewrite exprD_nneg 1:subz_ge0 // ler_pemull ?(expr_ge0, exprn_ege1) //.
 + by rewrite (@ler_trans oner). + by rewrite subz_ge0.
 qed.
 
+lemma ler_weexpn2r x : oner < x =>
+  forall m n, 0 <= m => 0 <= n => exp x m <= exp x n => m <= n.
+proof.
+move => lt1x m n le0m le0n; rewrite -implybNN -ltrNge -ltzNge ltzE => le_m; apply (ltr_le_trans (exp x (n + 1))).
++ by rewrite exprS //; apply ltr_pmull => //; apply/expr_gt0/(ler_lt_trans oner).
+by apply ler_weexpn2l; [apply ltrW|split => //; apply addz_ge0].
+qed.
+
 lemma nosmt ieexprn_weq1 x n : 0 <= n => zeror <= x =>
   (exp x n = oner) <=> (n = 0 || x = oner).
 proof.
@@ -1189,6 +1219,14 @@ proof. by rewrite ger0_def. qed.
 lemma nosmt eqr_normN (x : t): (`|x| = - x) <=> (x <= zeror).
 proof. by rewrite ler0_def. qed.
 
+lemma nosmt normE n :
+  `|n| = if zeror <= n then n else -n.
+proof.
+move: (real_axiom n); rewrite or_andr => -[le0n|[Nle0n len0]].
++ by rewrite le0n /= eqr_norm_id.
+by rewrite Nle0n /= eqr_normN.
+qed.
+
 (* -------------------------------------------------------------------- *)
 lemma ler_norm x : x <= `|x|.
 proof.

theories/algebra/Poly.ec

@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 require import AllCore Finite Distr DList List.
-require import Ring Bigalg StdBigop StdOrder.
+require import Ring IntMin Bigalg StdBigop StdOrder.
 require (*--*) Subtype.
 (*---*) import Bigint IntID IntOrder.
 

theories/algebra/Ring.ec

@@ -235,6 +235,9 @@ abstract theory ComRing.
   lemma nosmt mulrACA: interchange ( * ) ( * ).
   proof. by move=> x y z t; rewrite -!mulrA (mulrCA y). qed.
 
+  lemma nosmt mulrSl x y : (x + oner) * y = x * y + y.
+  proof. by rewrite mulrDl mul1r. qed.
+
   lemma nosmt mulrDr: right_distributive ( * ) (+).
   proof. by move=> x y z; rewrite mulrC mulrDl !(@mulrC _ x). qed.
 

theories/algebra/StdOrder.ec

@@ -71,6 +71,7 @@ move=> nz_0; rewrite b2i1 /= -{1}(mul1r `|z|); congr.
 rewrite -exprD_nneg ?b2i_ge0 -signr_odd ?addr_ge0 ?b2i_ge0.
 by rewrite -mul1r2z oddM /ofint_id intmulz odd2 expr0.
 qed.
+
 end IntOrder.
 
 (* -------------------------------------------------------------------- *)