Adds theories/algebra/ZqCentered.ec providing the centered (signed) i…

theories/algebra/MaxBigop.eca

@@ -0,0 +1,66 @@
+(* ==================================================================== *)
+require import AllCore List.
+require Bigop TypeWithBot.
+
+(* ==================================================================== *)
+(* Generic big-fold of [max] over a list, built atop [Bigop] using the  *)
+(* max-monoid induced by a [TypeWithBot] instance.                      *)
+(* ==================================================================== *)
+
+clone include TypeWithBot.
+
+(* -------------------------------------------------------------------- *)
+op maxr (x y : t) : t = if x <= y then y else x.
+
+lemma maxrA : associative maxr.
+proof. by move=> x y z; rewrite /maxr; smt(le_refl le_trans le_anti le_total). qed.
+
+lemma maxrC : commutative maxr.
+proof. by move=> x y; rewrite /maxr; smt(le_anti le_total). qed.
+
+lemma max0r : left_id bot maxr.
+proof. by move=> x; rewrite /maxr bot_le. qed.
+
+lemma maxrr (x : t) : maxr x x = x.
+proof. by rewrite /maxr; case (x <= x). qed.
+
+lemma maxr_lel (x y : t) : x <= y => maxr x y = y.
+proof. by rewrite /maxr => ->. qed.
+
+lemma maxr_ler (x y : t) : y <= x => maxr x y = x.
+proof. by rewrite /maxr => H; case (x <= y) => Hxy //; smt(le_anti). qed.
+
+lemma maxr_ge_l (x y : t) : x <= maxr x y.
+proof. by rewrite /maxr; case (x <= y) => // ?; apply le_refl. qed.
+
+lemma maxr_ge_r (x y : t) : y <= maxr x y.
+proof. by rewrite /maxr; case (x <= y) => H; [apply le_refl | smt(le_total)]. qed.
+
+lemma maxr_le_max (x y b : t) : x <= b => y <= b => maxr x y <= b.
+proof. by rewrite /maxr; case (x <= y). qed.
+
+lemma maxr_le_max_iff (x y b : t) : (maxr x y <= b) <=> (x <= b /\ y <= b).
+proof.
+split; last by case=> *; apply maxr_le_max.
+move=> H; split; smt(maxr_ge_l maxr_ge_r le_trans).
+qed.
+
+(* -------------------------------------------------------------------- *)
+clone include Bigop with
+  type t <- t,
+    op Support.idm   <- bot,
+    op Support.( + ) <- maxr
+proof Support.Axioms.* by smt(maxrA maxrC max0r).
+
+(* -------------------------------------------------------------------- *)
+(* Soundness: the big-max is bounded above iff every element is.        *)
+
+lemma big_le_iff (P : 'a -> bool) (F : 'a -> t) (s : 'a list) (b : t) :
+  big P F s <= b <=> bot <= b /\ forall x, x \in s => P x => F x <= b.
+proof.
+elim: s => [|x xs IH] /=.
+- by rewrite big_nil; smt().
+rewrite big_cons; case (P x) => Px /=.
+- rewrite maxr_le_max_iff IH; smt().
+- by rewrite IH; smt().
+qed.

theories/algebra/PolyReduce.ec

@@ -460,17 +460,12 @@ end PolyReduce.
 
 (* ==================================================================== *)
 abstract theory PolyReduceZp.
-type coeff.
-
-op p : { int | 2 <= p } as ge2_p.
 
-clone import ZModRing as Zp with
-    op    p     <= p
-    proof ge2_p by exact/ge2_p.
+clone import ZModRing as Zp.
 
 clone import PolyReduce with
-    type coeff <- Zp.zmod,
-  theory Coeff <- ZModpRing.
+    type coeff <= Zp.zmod,
+  theory Coeff <= ZModpRing.
 
 (* ==================================================================== *)
 (* We already know that polyXnD1 is finite. However, we prove here that *)
@@ -526,3 +521,220 @@ lemma reduced_dpoly d p : p \in dpoly n d => reduced p.
 proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed.
 
 end PolyReduceZp.
+
+(* ==================================================================== *)
+(* PolyReduceZpCentered: same scaffolding as [PolyReduceZp] but the     *)
+(* coefficient sub-theory is [ZqCentered] (extends [ZModRing] with     *)
+(* centered representation [crepr], absolute value `|_|`, and the      *)
+(* abs_zp lemma family).                                                *)
+(*                                                                      *)
+(* Built by first cloning [ZqCentered] (to get the extended Zp), then  *)
+(* clone-including [PolyReduceZp] with PolyReduceZp's internal Zp       *)
+(* rebound to ours — so the polynomial-ring construction and the       *)
+(* distributions are inherited without copy-paste.                     *)
+(* ==================================================================== *)
+require import ZModPCentered Nneg.
+
+abstract theory PolyReduceZpCentered.
+
+clone import ZpCentered as ZpC.
+
+clone import PolyReduceZp with
+  theory Zp <- Zp.
+import PolyReduce.
+import Zp.
+
+(* ==================================================================== *)
+(* Distributions over polyXnD1 — duplicated from PolyReduceZp because    *)
+(* PolyReduceZp's internal Zp is not exposed as a rebindable theory     *)
+(* parameter, so we cannot clone-include it with our extended Zp.       *)
+(* ==================================================================== *)
+op dpolyX (dcoeff : zmod distr) : polyXnD1 distr =
+  dmap (dpoly n dcoeff) pinject.
+
+lemma dpolyX_ll d : is_lossless d => is_lossless (dpolyX d).
+proof. by move=> ll_d; apply/dmap_ll/BasePoly.dpoly_ll. qed.
+
+lemma dpolyX_uni d : is_uniform d => is_uniform (dpolyX d).
+proof.
+move=> uni_d; apply/dmap_uni_in_inj/dpoly_uni/uni_d => //.
+move=> p q; rewrite !supp_dpoly //; case=> [degp _] [deqq _].
+by move/eqv_pi/reduce_eqP; rewrite !reduce_reduced // !reducedP.
+qed.
+
+lemma dpolyX_full d : is_full d => is_full (dpolyX d).
+proof.
+move=> fu_d; apply/dmap_fu_in=> p; exists (crepr p).
+by rewrite creprK /=; apply/dpoly_fu/deg_crepr.
+qed.
+
+lemma dpolyX_suppP d p :
+  p \in dpolyX d <=> (forall i, 0 <= i < n => p.[i] \in d).
+proof. split.
+- case/supp_dmap=> q [+ ->>] i rg_i.
+  rewrite supp_dpoly => // -[? /(_ i rg_i)].
+  by rewrite piK //; apply/reducedP.
+- move=> h; apply/supp_dmap; exists (crepr p).
+  by rewrite creprK /= &(supp_dpoly) // deg_crepr.
+qed.
+
+(* -------------------------------------------------------------------- *)
+op dpolyXnD1 = dpolyX Zp.DZmodP.dunifin.
+
+lemma dpolyXnD1_ll : is_lossless dpolyXnD1.
+proof. by apply/dpolyX_ll/DZmodP.dunifin_ll. qed.
+
+lemma dpolyXnD1_uni : is_uniform dpolyXnD1.
+proof. by apply/dpolyX_uni/DZmodP.dunifin_uni. qed.
+
+lemma dpolyXnD1_full : is_full dpolyXnD1.
+proof. by apply/dpolyX_full/DZmodP.dunifin_fu. qed.
+
+lemma dpolyXnD1_funi : is_funiform dpolyXnD1.
+proof. by apply/is_full_funiform/dpolyXnD1_uni/dpolyXnD1_full. qed.
+
+(* -------------------------------------------------------------------- *)
+lemma reduced_dpoly d p : p \in dpoly n d => reduced p.
+proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed.
+
+(* ==================================================================== *)
+(* Centered-representation infinity-norm machinery on polyXnD1.         *)
+(*                                                                      *)
+(* Two complementary views, equivalent under non-negative bounds:       *)
+(*   - predicate-style checks: poly_infnorm_le, poly_infnorm_lt         *)
+(*   - computed norm: inf_norm : polyXnD1 -> Nneg.nneg                   *)
+(* The soundness lemmas tie them together.                               *)
+(* ==================================================================== *)
+
+(* -------------------------------------------------------------------- *)
+(* Predicate-style inf-norm bound checks on coefficients.                *)
+
+op poly_infnorm_lt (q : polyXnD1) (b : int) : bool =
+  forall i, 0 <= i < n => `|q.[i]| < b.
+
+op poly_infnorm_le (q : polyXnD1) (b : int) : bool =
+  forall i, 0 <= i < n => `|q.[i]| <= b.
+
+(* -------------------------------------------------------------------- *)
+(* Basic monotonicity / equivalence lemmas.                              *)
+
+lemma poly_infnorm_lt_le (q : polyXnD1) (b : int) :
+  poly_infnorm_lt q b => poly_infnorm_le q b.
+proof. by move=> H i Hi; have := H i Hi; smt(). qed.
+
+lemma poly_infnorm_le_mono (q : polyXnD1) (b1 b2 : int) :
+  b1 <= b2 => poly_infnorm_le q b1 => poly_infnorm_le q b2.
+proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed.
+
+lemma poly_infnorm_lt_mono (q : polyXnD1) (b1 b2 : int) :
+  b1 <= b2 => poly_infnorm_lt q b1 => poly_infnorm_lt q b2.
+proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed.
+
+(* -------------------------------------------------------------------- *)
+(* Trivial bounds.                                                       *)
+
+lemma poly_infnorm_le_ub (q : polyXnD1) :
+  poly_infnorm_le q (p %/ 2)
+  by move=> i Hi; smt(abs_zp_ub).
+
+lemma poly_infnorm_le_zero :
+  poly_infnorm_le zeroXnD1 0.
+proof. move=> i Hi; rewrite rcoeff0; smt(abs_zp_zero). qed.
+
+(* -------------------------------------------------------------------- *)
+(* Triangle inequality and negation bounds.                              *)
+
+lemma poly_infnorm_le_add (q r : polyXnD1) (bq br : int) :
+     poly_infnorm_le q bq
+  => poly_infnorm_le r br
+  => poly_infnorm_le (q + r) (bq + br).
+proof.
+move=> Hq Hr i Hi.
+rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i].
+have := Hq i Hi; have := Hr i Hi; smt().
+qed.
+
+lemma poly_infnorm_lt_add (q r : polyXnD1) (bq br : int) :
+     poly_infnorm_lt q bq
+  => poly_infnorm_lt r br
+  => poly_infnorm_lt (q + r) (bq + br).
+proof.
+move=> Hq Hr i Hi.
+rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i].
+have := Hq i Hi; have := Hr i Hi; smt().
+qed.
+
+lemma poly_infnorm_le_opp (q : polyXnD1) (b : int) :
+  poly_infnorm_le q b => poly_infnorm_le (- q) b.
+proof.
+move=> H i Hi.
+rewrite -rcoeffN -abs_zpN.
+have := H i Hi; smt().
+qed.
+
+lemma poly_infnorm_lt_opp (q : polyXnD1) (b : int) :
+  poly_infnorm_lt q b => poly_infnorm_lt (- q) b.
+proof.
+move=> H i Hi.
+rewrite -rcoeffN -abs_zpN.
+have := H i Hi; smt().
+qed.
+
+(* -------------------------------------------------------------------- *)
+(* Computed inf-norm via big-max of coefficient absolute values.        *)
+
+op inf_norm (q : polyXnD1) : Nneg.nneg =
+  Nneg.BMaxN.bigi predT (fun i => Nneg.ofint `|q.[i]|) 0 n.
+
+(* Soundness against the [_le] check (for non-negative bounds). *)
+lemma poly_infnorm_le_iff (q : polyXnD1) (b : int) :
+  0 <= b =>
+  (poly_infnorm_le q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint b)).
+proof.
+move=> ge0_b; rewrite /poly_infnorm_le /inf_norm Nneg.BMaxN.big_le_iff.
+have valK_b : Nneg.val (Nneg.ofint b) = b by apply Nneg.valK_pos.
+have step : forall a, 0 <= a =>
+  Nneg.(<=) (Nneg.ofint a) (Nneg.ofint b) <=> a <= b.
+- move=> a ge0_a; rewrite /Nneg.(<=) valK_b.
+  by have -> : Nneg.val (Nneg.ofint a) = a by apply Nneg.valK_pos.
+split.
+- move=> H; split; first by apply Nneg.zero_le.
+  move=> i; rewrite mem_range => Hi _ /=.
+  have ge0_a : 0 <= `|q.[i]| by smt().
+  by rewrite step //; apply H; smt().
+- case=> _ H i Hi.
+  have Hi' : i \in range 0 n by rewrite mem_range; smt().
+  have ge0_a : 0 <= `|q.[i]| by smt().
+  have := H i Hi' _; first by [].
+  by rewrite /= step.
+qed.
+
+(* Soundness against the [_lt] check. Strictly-less bound means         *)
+(* coefficient bounds by [b - 1] (since values are integers).           *)
+lemma poly_infnorm_lt_iff (q : polyXnD1) (b : int) :
+  1 <= b =>
+  (poly_infnorm_lt q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint (b - 1))).
+proof.
+move=> ge1_b.
+have -> : poly_infnorm_lt q b <=> poly_infnorm_le q (b - 1)
+  by rewrite /poly_infnorm_lt /poly_infnorm_le; smt().
+by apply poly_infnorm_le_iff; smt().
+qed.
+
+end PolyReduceZpCentered.
+
+(* ==================================================================== *)
+(* Field version: when [p] is prime, additionally make available the    *)
+(* prime-only coefficient lemmas (creprN, creprND, creprN2) on the same *)
+(* polyXnD1 coefficient instantiation.                                  *)
+(* ==================================================================== *)
+abstract theory PolyReduceZpCenteredField.
+
+clone import ZpCenteredField as ZpCF.
+import ZpC.
+
+clone import PolyReduceZpCentered with
+  theory ZpC <- ZpC.
+import Zp.
+
+end PolyReduceZpCenteredField.

theories/algebra/TypeWithBot.eca

@@ -0,0 +1,24 @@
+(* ==================================================================== *)
+require import AllCore.
+
+(* ==================================================================== *)
+(* A type equipped with a total order having a least element [bot].     *)
+(*                                                                      *)
+(* This abstraction is exactly what is needed to form a max-monoid:     *)
+(* [maxr x y = if x <= y then y else x] is associative, commutative,    *)
+(* and has [bot] as identity (since [bot <= x] for all [x]).            *)
+(*                                                                      *)
+(* On types without a global minimum (e.g. plain [int]) one must        *)
+(* restrict to a subtype bounded below.                                 *)
+(* ==================================================================== *)
+
+type t.
+
+op (<=) : t -> t -> bool.
+op bot  : t.
+
+axiom le_refl  (x   : t) : x <= x.
+axiom le_trans (y x z : t) : x <= y => y <= z => x <= z.
+axiom le_anti  (x y : t) : x <= y => y <= x => x = y.
+axiom le_total (x y : t) : x <= y \/ y <= x.
+axiom bot_le   (x   : t) : bot <= x.