Skip to content

Commit bcca610

Browse files
mbbarbosambbarbosa
committed
Extended version of PolyReduce
1 parent 7859b9d commit bcca610

5 files changed

Lines changed: 399 additions & 18 deletions

File tree

‎theories/algebra/MaxBigop.eca‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(* ==================================================================== *)
2+
require import AllCore List.
3+
require Bigop TypeWithBot.
4+
5+
(* ==================================================================== *)
6+
(* Generic big-fold of [max] over a list, built atop [Bigop] using the *)
7+
(* max-monoid induced by a [TypeWithBot] instance. *)
8+
(* ==================================================================== *)
9+
10+
clone include TypeWithBot.
11+
12+
(* -------------------------------------------------------------------- *)
13+
op maxr (x y : t) : t = if x <= y then y else x.
14+
15+
lemma maxrA : associative maxr.
16+
proof. by move=> x y z; rewrite /maxr; smt(le_refl le_trans le_anti le_total). qed.
17+
18+
lemma maxrC : commutative maxr.
19+
proof. by move=> x y; rewrite /maxr; smt(le_anti le_total). qed.
20+
21+
lemma max0r : left_id bot maxr.
22+
proof. by move=> x; rewrite /maxr bot_le. qed.
23+
24+
lemma maxrr (x : t) : maxr x x = x.
25+
proof. by rewrite /maxr; case (x <= x). qed.
26+
27+
lemma maxr_lel (x y : t) : x <= y => maxr x y = y.
28+
proof. by rewrite /maxr => ->. qed.
29+
30+
lemma maxr_ler (x y : t) : y <= x => maxr x y = x.
31+
proof. by rewrite /maxr => H; case (x <= y) => Hxy //; smt(le_anti). qed.
32+
33+
lemma maxr_ge_l (x y : t) : x <= maxr x y.
34+
proof. by rewrite /maxr; case (x <= y) => // ?; apply le_refl. qed.
35+
36+
lemma maxr_ge_r (x y : t) : y <= maxr x y.
37+
proof. by rewrite /maxr; case (x <= y) => H; [apply le_refl | smt(le_total)]. qed.
38+
39+
lemma maxr_le_max (x y b : t) : x <= b => y <= b => maxr x y <= b.
40+
proof. by rewrite /maxr; case (x <= y). qed.
41+
42+
lemma maxr_le_max_iff (x y b : t) : (maxr x y <= b) <=> (x <= b /\ y <= b).
43+
proof.
44+
split; last by case=> *; apply maxr_le_max.
45+
move=> H; split; smt(maxr_ge_l maxr_ge_r le_trans).
46+
qed.
47+
48+
(* -------------------------------------------------------------------- *)
49+
clone include Bigop with
50+
type t <- t,
51+
op Support.idm <- bot,
52+
op Support.( + ) <- maxr
53+
proof Support.Axioms.* by smt(maxrA maxrC max0r).
54+
55+
(* -------------------------------------------------------------------- *)
56+
(* Soundness: the big-max is bounded above iff every element is. *)
57+
58+
lemma big_le_iff (P : 'a -> bool) (F : 'a -> t) (s : 'a list) (b : t) :
59+
big P F s <= b <=> bot <= b /\ forall x, x \in s => P x => F x <= b.
60+
proof.
61+
elim: s => [|x xs IH] /=.
62+
- by rewrite big_nil; smt().
63+
rewrite big_cons; case (P x) => Px /=.
64+
- rewrite maxr_le_max_iff IH; smt().
65+
- by rewrite IH; smt().
66+
qed.

‎theories/algebra/PolyReduce.ec‎

Lines changed: 220 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -460,17 +460,12 @@ end PolyReduce.
460460

461461
(* ==================================================================== *)
462462
abstract theory PolyReduceZp.
463-
type coeff.
464-
465-
op p : { int | 2 <= p } as ge2_p.
466463

467-
clone import ZModRing as Zp with
468-
op p <= p
469-
proof ge2_p by exact/ge2_p.
464+
clone import ZModRing as Zp.
470465

471466
clone import PolyReduce with
472-
type coeff <- Zp.zmod,
473-
theory Coeff <- ZModpRing.
467+
type coeff <= Zp.zmod,
468+
theory Coeff <= ZModpRing.
474469

475470
(* ==================================================================== *)
476471
(* 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.
526521
proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed.
527522

528523
end PolyReduceZp.
524+
525+
(* ==================================================================== *)
526+
(* PolyReduceZpCentered: same scaffolding as [PolyReduceZp] but the *)
527+
(* coefficient sub-theory is [ZqCentered] (extends [ZModRing] with *)
528+
(* centered representation [crepr], absolute value `|_|`, and the *)
529+
(* abs_zp lemma family). *)
530+
(* *)
531+
(* Built by first cloning [ZqCentered] (to get the extended Zp), then *)
532+
(* clone-including [PolyReduceZp] with PolyReduceZp's internal Zp *)
533+
(* rebound to ours — so the polynomial-ring construction and the *)
534+
(* distributions are inherited without copy-paste. *)
535+
(* ==================================================================== *)
536+
require import ZModPCentered Nneg.
537+
538+
abstract theory PolyReduceZpCentered.
539+
540+
clone import ZpCentered as ZpC.
541+
542+
clone import PolyReduceZp with
543+
theory Zp <- Zp.
544+
import PolyReduce.
545+
import Zp.
546+
547+
(* ==================================================================== *)
548+
(* Distributions over polyXnD1 — duplicated from PolyReduceZp because *)
549+
(* PolyReduceZp's internal Zp is not exposed as a rebindable theory *)
550+
(* parameter, so we cannot clone-include it with our extended Zp. *)
551+
(* ==================================================================== *)
552+
op dpolyX (dcoeff : zmod distr) : polyXnD1 distr =
553+
dmap (dpoly n dcoeff) pinject.
554+
555+
lemma dpolyX_ll d : is_lossless d => is_lossless (dpolyX d).
556+
proof. by move=> ll_d; apply/dmap_ll/BasePoly.dpoly_ll. qed.
557+
558+
lemma dpolyX_uni d : is_uniform d => is_uniform (dpolyX d).
559+
proof.
560+
move=> uni_d; apply/dmap_uni_in_inj/dpoly_uni/uni_d => //.
561+
move=> p q; rewrite !supp_dpoly //; case=> [degp _] [deqq _].
562+
by move/eqv_pi/reduce_eqP; rewrite !reduce_reduced // !reducedP.
563+
qed.
564+
565+
lemma dpolyX_full d : is_full d => is_full (dpolyX d).
566+
proof.
567+
move=> fu_d; apply/dmap_fu_in=> p; exists (crepr p).
568+
by rewrite creprK /=; apply/dpoly_fu/deg_crepr.
569+
qed.
570+
571+
lemma dpolyX_suppP d p :
572+
p \in dpolyX d <=> (forall i, 0 <= i < n => p.[i] \in d).
573+
proof. split.
574+
- case/supp_dmap=> q [+ ->>] i rg_i.
575+
rewrite supp_dpoly => // -[? /(_ i rg_i)].
576+
by rewrite piK //; apply/reducedP.
577+
- move=> h; apply/supp_dmap; exists (crepr p).
578+
by rewrite creprK /= &(supp_dpoly) // deg_crepr.
579+
qed.
580+
581+
(* -------------------------------------------------------------------- *)
582+
op dpolyXnD1 = dpolyX Zp.DZmodP.dunifin.
583+
584+
lemma dpolyXnD1_ll : is_lossless dpolyXnD1.
585+
proof. by apply/dpolyX_ll/DZmodP.dunifin_ll. qed.
586+
587+
lemma dpolyXnD1_uni : is_uniform dpolyXnD1.
588+
proof. by apply/dpolyX_uni/DZmodP.dunifin_uni. qed.
589+
590+
lemma dpolyXnD1_full : is_full dpolyXnD1.
591+
proof. by apply/dpolyX_full/DZmodP.dunifin_fu. qed.
592+
593+
lemma dpolyXnD1_funi : is_funiform dpolyXnD1.
594+
proof. by apply/is_full_funiform/dpolyXnD1_uni/dpolyXnD1_full. qed.
595+
596+
(* -------------------------------------------------------------------- *)
597+
lemma reduced_dpoly d p : p \in dpoly n d => reduced p.
598+
proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed.
599+
600+
(* ==================================================================== *)
601+
(* Centered-representation infinity-norm machinery on polyXnD1. *)
602+
(* *)
603+
(* Two complementary views, equivalent under non-negative bounds: *)
604+
(* - predicate-style checks: poly_infnorm_le, poly_infnorm_lt *)
605+
(* - computed norm: inf_norm : polyXnD1 -> Nneg.nneg *)
606+
(* The soundness lemmas tie them together. *)
607+
(* ==================================================================== *)
608+
609+
(* -------------------------------------------------------------------- *)
610+
(* Predicate-style inf-norm bound checks on coefficients. *)
611+
612+
op poly_infnorm_lt (q : polyXnD1) (b : int) : bool =
613+
forall i, 0 <= i < n => `|q.[i]| < b.
614+
615+
op poly_infnorm_le (q : polyXnD1) (b : int) : bool =
616+
forall i, 0 <= i < n => `|q.[i]| <= b.
617+
618+
(* -------------------------------------------------------------------- *)
619+
(* Basic monotonicity / equivalence lemmas. *)
620+
621+
lemma poly_infnorm_lt_le (q : polyXnD1) (b : int) :
622+
poly_infnorm_lt q b => poly_infnorm_le q b.
623+
proof. by move=> H i Hi; have := H i Hi; smt(). qed.
624+
625+
lemma poly_infnorm_le_mono (q : polyXnD1) (b1 b2 : int) :
626+
b1 <= b2 => poly_infnorm_le q b1 => poly_infnorm_le q b2.
627+
proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed.
628+
629+
lemma poly_infnorm_lt_mono (q : polyXnD1) (b1 b2 : int) :
630+
b1 <= b2 => poly_infnorm_lt q b1 => poly_infnorm_lt q b2.
631+
proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed.
632+
633+
(* -------------------------------------------------------------------- *)
634+
(* Trivial bounds. *)
635+
636+
lemma poly_infnorm_le_ub (q : polyXnD1) :
637+
poly_infnorm_le q (p %/ 2)
638+
by move=> i Hi; smt(abs_zp_ub).
639+
640+
lemma poly_infnorm_le_zero :
641+
poly_infnorm_le zeroXnD1 0.
642+
proof. move=> i Hi; rewrite rcoeff0; smt(abs_zp_zero). qed.
643+
644+
(* -------------------------------------------------------------------- *)
645+
(* Triangle inequality and negation bounds. *)
646+
647+
lemma poly_infnorm_le_add (q r : polyXnD1) (bq br : int) :
648+
poly_infnorm_le q bq
649+
=> poly_infnorm_le r br
650+
=> poly_infnorm_le (q + r) (bq + br).
651+
proof.
652+
move=> Hq Hr i Hi.
653+
rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i].
654+
have := Hq i Hi; have := Hr i Hi; smt().
655+
qed.
656+
657+
lemma poly_infnorm_lt_add (q r : polyXnD1) (bq br : int) :
658+
poly_infnorm_lt q bq
659+
=> poly_infnorm_lt r br
660+
=> poly_infnorm_lt (q + r) (bq + br).
661+
proof.
662+
move=> Hq Hr i Hi.
663+
rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i].
664+
have := Hq i Hi; have := Hr i Hi; smt().
665+
qed.
666+
667+
lemma poly_infnorm_le_opp (q : polyXnD1) (b : int) :
668+
poly_infnorm_le q b => poly_infnorm_le (- q) b.
669+
proof.
670+
move=> H i Hi.
671+
rewrite -rcoeffN -abs_zpN.
672+
have := H i Hi; smt().
673+
qed.
674+
675+
lemma poly_infnorm_lt_opp (q : polyXnD1) (b : int) :
676+
poly_infnorm_lt q b => poly_infnorm_lt (- q) b.
677+
proof.
678+
move=> H i Hi.
679+
rewrite -rcoeffN -abs_zpN.
680+
have := H i Hi; smt().
681+
qed.
682+
683+
(* -------------------------------------------------------------------- *)
684+
(* Computed inf-norm via big-max of coefficient absolute values. *)
685+
686+
op inf_norm (q : polyXnD1) : Nneg.nneg =
687+
Nneg.BMaxN.bigi predT (fun i => Nneg.ofint `|q.[i]|) 0 n.
688+
689+
(* Soundness against the [_le] check (for non-negative bounds). *)
690+
lemma poly_infnorm_le_iff (q : polyXnD1) (b : int) :
691+
0 <= b =>
692+
(poly_infnorm_le q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint b)).
693+
proof.
694+
move=> ge0_b; rewrite /poly_infnorm_le /inf_norm Nneg.BMaxN.big_le_iff.
695+
have valK_b : Nneg.val (Nneg.ofint b) = b by apply Nneg.valK_pos.
696+
have step : forall a, 0 <= a =>
697+
Nneg.(<=) (Nneg.ofint a) (Nneg.ofint b) <=> a <= b.
698+
- move=> a ge0_a; rewrite /Nneg.(<=) valK_b.
699+
by have -> : Nneg.val (Nneg.ofint a) = a by apply Nneg.valK_pos.
700+
split.
701+
- move=> H; split; first by apply Nneg.zero_le.
702+
move=> i; rewrite mem_range => Hi _ /=.
703+
have ge0_a : 0 <= `|q.[i]| by smt().
704+
by rewrite step //; apply H; smt().
705+
- case=> _ H i Hi.
706+
have Hi' : i \in range 0 n by rewrite mem_range; smt().
707+
have ge0_a : 0 <= `|q.[i]| by smt().
708+
have := H i Hi' _; first by [].
709+
by rewrite /= step.
710+
qed.
711+
712+
(* Soundness against the [_lt] check. Strictly-less bound means *)
713+
(* coefficient bounds by [b - 1] (since values are integers). *)
714+
lemma poly_infnorm_lt_iff (q : polyXnD1) (b : int) :
715+
1 <= b =>
716+
(poly_infnorm_lt q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint (b - 1))).
717+
proof.
718+
move=> ge1_b.
719+
have -> : poly_infnorm_lt q b <=> poly_infnorm_le q (b - 1)
720+
by rewrite /poly_infnorm_lt /poly_infnorm_le; smt().
721+
by apply poly_infnorm_le_iff; smt().
722+
qed.
723+
724+
end PolyReduceZpCentered.
725+
726+
(* ==================================================================== *)
727+
(* Field version: when [p] is prime, additionally make available the *)
728+
(* prime-only coefficient lemmas (creprN, creprND, creprN2) on the same *)
729+
(* polyXnD1 coefficient instantiation. *)
730+
(* ==================================================================== *)
731+
abstract theory PolyReduceZpCenteredField.
732+
733+
clone import ZpCenteredField as ZpCF.
734+
import ZpC.
735+
736+
clone import PolyReduceZpCentered with
737+
theory ZpC <- ZpC.
738+
import Zp.
739+
740+
end PolyReduceZpCenteredField.

‎theories/algebra/TypeWithBot.eca‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
(* ==================================================================== *)
2+
require import AllCore.
3+
4+
(* ==================================================================== *)
5+
(* A type equipped with a total order having a least element [bot]. *)
6+
(* *)
7+
(* This abstraction is exactly what is needed to form a max-monoid: *)
8+
(* [maxr x y = if x <= y then y else x] is associative, commutative, *)
9+
(* and has [bot] as identity (since [bot <= x] for all [x]). *)
10+
(* *)
11+
(* On types without a global minimum (e.g. plain [int]) one must *)
12+
(* restrict to a subtype bounded below. *)
13+
(* ==================================================================== *)
14+
15+
type t.
16+
17+
op (<=) : t -> t -> bool.
18+
op bot : t.
19+
20+
axiom le_refl (x : t) : x <= x.
21+
axiom le_trans (y x z : t) : x <= y => y <= z => x <= z.
22+
axiom le_anti (x y : t) : x <= y => y <= x => x = y.
23+
axiom le_total (x y : t) : x <= y \/ y <= x.
24+
axiom bot_le (x : t) : bot <= x.

theories/algebra/ZqCentered.ec renamed to theories/algebra/ZModPCentered.ec

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,9 @@ require ZModP.
2626
(* ==================================================================== *)
2727
2828
(* ==================================================================== *)
29-
abstract theory ZqCentered.
29+
abstract theory ZpCentered.
3030
31-
clone include ZModP.ZModRing.
31+
clone import ZModP.ZModRing as Zp.
3232
3333
(* -------------------------------------------------------------------- *)
3434
(* Auxiliary congruence lemmas. *)
@@ -225,19 +225,17 @@ suff : (p - asint x) %% p = ((p - asint x) + p) %% p by smt(rg_asint).
225225
by smt(modzDr).
226226
qed.
227227
228-
end ZqCentered.
228+
end ZpCentered.
229229
230230
(* ==================================================================== *)
231231
(* Field version: when p is prime, additionally provide negation *)
232232
(* symmetry for the centered representative. *)
233233
(* ==================================================================== *)
234-
abstract theory ZqCenteredField.
234+
abstract theory ZpCenteredField.
235235
236-
const p : { int | prime p } as prime_p.
237-
238-
clone include ZqCentered with
239-
op p <- p
240-
proof ge2_p by smt(gt1_prime prime_p).
236+
clone import ZpCentered as ZpC.
237+
import Zp.
238+
axiom prime_p : prime p.
241239
242240
(* prime_p is now in scope; ZqCentered's content is available. *)
243241

@@ -297,4 +295,4 @@ case (p = 2); 2: by smt(creprD creprN).
297295
by smt(creprD creprN2).
298296
qed.
299297

300-
end ZqCenteredField.
298+
end ZpCenteredField.

0 commit comments

Comments
 (0)