From 40228322186ad70961c8ef3e714638e756746a84 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 21 Aug 2024 11:37:01 +0200 Subject: [PATCH 01/21] stdlib: basic commutative algebra --- theories/algebra/CommAlgebra.ec | 1088 +++++++++++++++++++++++++++++++ 1 file changed, 1088 insertions(+) create mode 100644 theories/algebra/CommAlgebra.ec diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec new file mode 100644 index 000000000..4743c4fa7 --- /dev/null +++ b/theories/algebra/CommAlgebra.ec @@ -0,0 +1,1088 @@ +(* -------------------------------------------------------------------- *) +require import AllCore StdOrder Finite IntDiv IntMin List Ring Bigalg. +require (*--*) Ideal. +(* - *) import IntOrder. + +pragma +implicits. + +(* -------------------------------------------------------------------- *) +clone import IDomain. + +(* -------------------------------------------------------------------- *) +clone Ideal.Ideal as I with + type t <- IDomain.t, + theory IDomain <= IDomain. + +(* -------------------------------------------------------------------- *) +abbrev (+) = I.idD. + +(* -------------------------------------------------------------------- *) +clone BigComRing as BR + with theory CR <= IDomain, + op BAdd.big ['a] <= I.BigDom.BAdd.big<:'a>, + op BMul.big ['a] <= I.BigDom.BMul.big<:'a>. + +(* -------------------------------------------------------------------- *) +import I. + +(* -------------------------------------------------------------------- *) +hint simplify [reduce] addr0, add0r. +hint simplify [reduce] mulr0, mul0r. +hint simplify [reduce] mulr1, mul1r. + +hint simplify [reduce] andbb, orbb. + +(* -------------------------------------------------------------------- *) +hint exact : dvdrr. +hint exact : ideal_idgen. + +(* -------------------------------------------------------------------- *) +lemma eqmodf1P (x : t) : (unit x) <=> (x %= oner). +proof. +split; first by move=> unit_x; apply/eqmodfP; exists x. +by case/eqmodfP=> y [unit_y ->]. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_eqpL (x y z : t) : x %| z => x %= y => y %| z. +proof. +case=> [c ->>] /eqmodfP[u] [unit_u ->>]. +by exists (c * u); rewrite mulrA. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_eqpR (x y z : t) : x %| y => y %= z => x %| z. +proof. +case=> [c ->>] /eqp_sym /eqmodfP[u] [unit_u ->>]. +by rewrite mulrA dvdr_mull dvdrr. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_add (x y z : t) : x %| y => x %| z => x %| (y + z). +proof. by move=> [cy ->] [cz ->]; exists (cy + cz); rewrite mulrDl. qed. + +(* -------------------------------------------------------------------- *) +lemma predeq_leP ['a] (p1 p2 : 'a -> bool) : + (p1 <= p2 /\ p2 <= p1) <=> (p1 = p2). +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma le_idDrL (I J1 J2 : t -> bool) : + ideal J2 => I <= J1 => I <= J1 + J2. +proof. by move=> idJ2 le_I_J2 x Ix; exists x zeror; do! split=> //#. qed. + +(* -------------------------------------------------------------------- *) +lemma le_idDrR (I J1 J2 : t -> bool) : + ideal J1 => I <= J2 => I <= J1 + J2. +proof. by move=> 2?; rewrite idDC; apply/le_idDrL. qed. + +(* -------------------------------------------------------------------- *) +hint exact : ideal_idgen. +hint exact : mem_idgen1_gen. + +hint simplify [reduce] mem_id0. + +(* -------------------------------------------------------------------- *) +lemma addi0 (I : t -> bool) : I + id0 = I. +proof. +apply/fun_ext => x /=; apply/eq_iff; split. +- by case=> y z [#] Iy /mem_id0 -> ->. +- by move=> Ix; exists x zeror. +qed. + +hint simplify [reduce] addi0. + +(* -------------------------------------------------------------------- *) +op w : t -> int. + +axiom ge0_w : forall x, 0 <= w x. +axiom eq0_wP : forall x, w x = 0 <=> x = zeror. +axiom dvdw : forall (x y : t), x %| y => w x <= w y. + +axiom Euclide : + forall x y, y <> zeror => + exists q r, x = y * q + r /\ w r < w y. + +(* -------------------------------------------------------------------- *) +hint exact : ge0_w. + +(* -------------------------------------------------------------------- *) +op coprime (x y : t) = + forall a, a %| x => a %| y => unit a. + +(* -------------------------------------------------------------------- *) +lemma coprimeC (x y : t) : coprime x y <=> coprime y x. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma Ncoprime0 : coprime zeror zeror => false. +proof. +move/(_ zeror _ _); 1,2: by apply/dvdr0. +by apply/unitr0. +qed. + +(* -------------------------------------------------------------------- *) +lemma idfunE ['a] (x : 'a) : idfun x = x. +proof. done. qed. + +hint simplify idfunE. + +(* -------------------------------------------------------------------- *) +lemma principal (I : t -> bool) : ideal I => principal I. +proof. +move=> idI; case: (I = pred1 zeror) => [->|nzI]; first by exists zeror. +have [x [Ix nz_x]]: exists a, I a /\ a <> zeror by apply: contraR nzI => /#. +pose P k := exists x, x <> zeror /\ I x /\ w x = k. +have := argminP_r<:int> idfun P (w x) _ _ => //=; ~-1: smt(). +move: (argmin _ _) => n [# ge0_n [a [# nz_a Ia waE]] min_a]. +exists a => y; split; last by case=> b ->; apply/idealMl. +move=> Iy; have [q r] [yE lt_w] := Euclide y a nz_a. +have rE: r = y - a * q by rewrite yE; ring. +have Ir: I r by rewrite rE; apply/idealB=> //; apply/idealMr. +case: (r = zeror) => [->>|nz_r]. +- by exists q; rewrite yE mulrC addr0. +have: P (w r) by exists r; split=> //. +by rewrite min_a //; smt(ge0_w). +qed. + +(* -------------------------------------------------------------------- *) +op isgcd (a b d : t) = + if a = zeror /\ b = zeror + then d = zeror + else d %| a /\ d %| b /\ (forall d', d' %| a => d' %| b => d' %| d). + +(* -------------------------------------------------------------------- *) +lemma isgcdW (P : t -> t -> t -> bool) : + P zeror zeror zeror + => (forall a b d, + a <> zeror \/ b <> zeror + => d %| a + => d %| b + => (forall d', d' %| a => d' %| b => d' %| d) + => P a b d) + => forall a b d, isgcd a b d => P a b d. +proof. by move=> /#. qed. + +(* -------------------------------------------------------------------- *) +lemma gcd (a b : t) : exists d, isgcd a b d. +proof. +rewrite /isgcd; case (a = zeror /\ b = zeror). +- by case=> ->> ->>; exists zeror. +move=> _; pose M := idgen [a] + idgen[b]. +have /principal: ideal M by apply/ideal_idD; apply/ideal_idgen. +case=> d /= ME; exists d; do! split. +- by rewrite /(%|) -ME /M mem_idDl //; solve. +- by rewrite /(%|) -ME /M mem_idDr //; solve. +move=> d' [a' aE] [b' bE]; apply/dvdrP. +have: M d; first by rewrite ME; exists oner. +case=> xa xb [#] /mem_idgen1[ca ->>] /mem_idgen1[cb ->>] ->>. +by rewrite aE bE !mulrA -mulrDl /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd_nzP (a b d : t) : (a <> zeror \/ b <> zeror) => + isgcd a b d <=> (d %| a /\ d %| b /\ (forall d', d' %| a => d' %| b => d' %| d)). +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd0 : isgcd zeror zeror zeror. +proof. done. qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd_refl (x : t) : isgcd x x x. +proof. by case: (x = zeror) => [->>//|nz_x]; apply/isgcd_nzP. qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd_sym (x y d : t) : isgcd x y d => isgcd y x d. +proof. +move: x y d; apply: isgcdW => //= a b d nz dvda dvdb mind. +by apply/isgcd_nzP => /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma idD_idgen (xs ys : t list) : idgen xs + idgen ys = idgen (xs ++ ys). +proof. +apply/predeq_leP; split=> z @/idD. +- case=> cx cy [+ ->] - []. + case/idgenP=> csx [eqx ->]; case/idgenP=> csy [eqy ->]. + exists (csx ++ csy); rewrite size_cat &(eq_sym). + rewrite (@BR.BAdd.big_cat_int (size xs)) ~-1:#smt:(size_ge0); congr. + - by apply: BR.BAdd.eq_big_int => i [_ lti] /=; rewrite !nth_cat eqx lti. + rewrite (@BR.BAdd.big_addn 0 _ (size xs)) addrAC /=. + apply: BR.BAdd.eq_big_int => /= i [ge0i lti]. + by rewrite !nth_cat -!addrA /= eqx ltzNge lez_addr ge0i. +- case/idgenP=> cs [sz_cs ->]. + pose csx := take (size xs) cs; pose csy := drop (size xs) cs. + pose x := BigDom.BAdd.bigi predT (fun (i : int) => csx.[i] * xs.[i]) 0 (size xs). + pose y := BigDom.BAdd.bigi predT (fun (i : int) => csy.[i] * ys.[i]) 0 (size ys). + exists x y; rewrite size_cat; split. + - by split; [exists csx | exists csy]. + rewrite (@BR.BAdd.big_cat_int (size xs)) ~-1:#smt:(size_ge0); congr. + - apply: BR.BAdd.eq_big_int => i [_ lti] /=; rewrite nth_cat lti /=. + by rewrite /csx nth_take ?size_ge0. + - rewrite (@BR.BAdd.big_addn 0 _ (size xs)) addrAC /=. + apply: BR.BAdd.eq_big_int => i [ge0i lti] /=; rewrite nth_cat. + rewrite ltzNge lez_addr ge0i /= -addrA /=. + by rewrite /csy nth_drop ?size_ge0 // [size xs + i]addrC. +qed. + +(* -------------------------------------------------------------------- *) +lemma big_int2 (F : int -> t) : BR.BAdd.bigi predT F 0 2 = F 0 + F 1. +proof. +by rewrite (@BR.BAdd.big_int_recr 1) // (@BR.BAdd.big_int_recr 0) // BR.BAdd.big_geq . +qed. + +(* -------------------------------------------------------------------- *) +lemma mem_idgen2 (x y a : t) : + idgen [x; y] a <=> exists (cx cy : t), a = cx * x + cy * y. +proof. split. +- by case=> cs -> /=; exists cs.[0] cs.[1]; rewrite big_int2. +- by case=> cx cy ->; exists [cx; cy]; rewrite big_int2. +qed. + +(* -------------------------------------------------------------------- *) +lemma principalP (I : t -> bool) : + principal I <=> exists x, I = idgen [x]. +proof. split; case=> x h; exists x. +- by apply/fun_ext=> y; rewrite h -mem_idgen1. +- by move=> y; rewrite h -mem_idgen1. +qed. + +(* -------------------------------------------------------------------- *) +lemma le_idgen_dvd (x : t) (ys : t list) : + (forall y, y \in ys => x %| y) <=> idgen ys <= idgen [x]. +proof. +split=> h; last first. +- by move=> y /in_idgen_mem /h /mem_idgen1_dvd. +move=> y /idgenP [cs] [eqsz ->]; rewrite mem_idgen1. +pose F y := choiceb (fun c => y = c * x) y. +pose ds := map (fun y => F y) ys. +pose d := BR.BAdd.bigi predT (fun i => cs.[i] * ds.[i]) 0 (size ys). +exists d => @/d; rewrite BR.BAdd.mulr_suml &(BR.BAdd.eq_big_int) /=. +move=> i [ge0i lti]; rewrite -mulrA; congr => @/ds. +rewrite (@nth_map zeror) //=. +have // := choicebP (fun c => ys.[i] = c * x) ys.[i] _ => /=. +have := h ys.[i] _; first by rewrite mem_nth. +by case/dvdrP=> q ->; exists q; rewrite mulrC. +qed. + +(* -------------------------------------------------------------------- *) +hint simplify subpred_refl. + +(* -------------------------------------------------------------------- *) +lemma isgcdP (a b d : t) : + isgcd a b d => idgen [a] + idgen [b] = idgen [d]. +proof. +move: a b d; apply/isgcdW => /=; first by rewrite idgen1_0. +move=> a b d nz dvda dvdb mind; apply: predeq_leP; split. +- by (apply: le_idDl; first by solve); apply/le_idgen1_dvd. +rewrite idD_idgen /=; have: ideal (idgen [a; b]) by apply/ideal_idgen. +case/principal/principalP=> y ^id_eq ->. +have := le_idgen_dvd y [a; b]; rewrite id_eq /= => dvdy. +by apply/le_idgen1_dvd/mind; apply/dvdy. +qed. + +(* -------------------------------------------------------------------- *) +lemma uniq_gcd (a b d1 d2 : t) : isgcd a b d1 => isgcd a b d2 => d1 %= d2. +proof. +rewrite /isgcd; case: (_ /\ _) => //=. +move=> [# dvd_d1a dvd_d1b mind1] [# dvd_d2a dvd_d2b mind2]. +by split; [apply mind2 | apply mind1]. +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcdsim (a b d1 d2 : t) : isgcd a b d1 => d1 %= d2 => isgcd a b d2. +proof. +move=> h; move: a b d1 h d2; apply: isgcdW => /= => [d2 |a b d1]. +- by move/eqp_sym=> /eqpf0P ->. +move=> nz dvda dvdb min_d1 d2 eqd; apply/isgcd_nzP => //; do! split. +- by apply/(dvdr_eqpL _ dvda). - by apply/(dvdr_eqpL _ dvdb). +by move=> d' dvda' dvdb'; apply/(dvdr_eqpR _ _ eqd)/min_d1. +qed. + +(* -------------------------------------------------------------------- *) +lemma Bezout (a b d : t) : isgcd a b d => + exists ca cb, ca * a + cb * b = d. +proof. +move/isgcdP=> eqid; have: idgen [d] d by apply/mem_idgen1_gen. +rewrite -eqid; case=> [ca cb] [#] + + ->>. +by move=> /mem_idgen1[ca' ->>] /mem_idgen1[cb' ->>]; exists ca' cb'. +qed. + +(* -------------------------------------------------------------------- *) +lemma coprime_isgcdP (x y : t) : isgcd x y oner <=> coprime x y. +proof. split. +- case/Bezout=> [cx cy] eq z dvd_za dvd_zb. + have: z %| oner by rewrite -eq dvdr_add dvdr_mull. + by case=> zI /eq_sym /unitP. +- case: (x = zeror /\ y = zeror); first by case=> ->> ->> /Ncoprime0. + move=> /negb_and nz; case: (gcd x y) => d ^hgcd /(isgcd_nzP _ _ _ nz). + by move=> [#] dvdx dvdy _ /(_ d dvdx dvdy) /eqmodf1P /(isgcdsim _ _ _ _ hgcd). +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd00 d : isgcd zeror zeror d => d = zeror. +proof. done. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_mul (a b a' b' : t) : a %| b => a' %| b' => a * a' %| b * b'. +proof. +move=> /dvdrP[d ->] /dvdrP[d' ->]; rewrite mulrACA. +by apply/dvdrP; exists (d * d'). +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcd0r (a : t) : isgcd zeror a a. +proof. +rewrite /isgcd /=; case: (a = zeror) => // _. +by rewrite dvdr0 dvdrr. +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcdr0 (a : t) : isgcd a zeror a. +proof. by rewrite isgcd_sym isgcd0r. qed. + +(* -------------------------------------------------------------------- *) +hint exact : isgcd0r isgcdr0. + +(* -------------------------------------------------------------------- *) +lemma isgcd0r_eqm (a b : t) : isgcd zeror a b <=> a %= b. +proof. +split. +- by have := isgcd0r a; apply: uniq_gcd. +- by have := isgcd0r a; apply: isgcdsim. +qed. + +(* -------------------------------------------------------------------- *) +lemma isgcdr0_eqm (a b : t) : isgcd a zeror b <=> a %= b. +proof. +split. +- by move/isgcd_sym/isgcd0r_eqm. +- by move/isgcd0r_eqm/isgcd_sym. +qed. + +(* -------------------------------------------------------------------- *) +lemma eqp_mulr (c a b : t) : a %= b => a * c %= b * c. +proof. +case/eqmodfP=> u [unit_u ->]; rewrite -mulrA. +by apply/eqmodfP; exists u. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_isgcdl (a b d : t) : isgcd a b d => d %| a. +proof. by move: a b d; apply/isgcdW. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_isgcdr (a b d : t) : isgcd a b d => d %| b. +proof. by move: a b d; apply/isgcdW. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrD (d a b : t) : d %| a => d %| b => d %| (a + b). +proof. by move=> /dvdrP[ca ->] /dvdrP[cb ->]; rewrite -mulrDl dvdr_mull. qed. + +(* -------------------------------------------------------------------- *) +lemma isgcdMr (a b c : t) (da d : t) : + isgcd (b * a) (c * a) da => isgcd b c d => da %= a * d. +proof. +case: (a = zeror) => [-> /= /isgcd00 ->//|nz_a]. +case: (b = zeror /\ c = zeror). +- by case=> [-> ->] /= /isgcd00 -> /isgcd00 ->. +move=> nz_bAc hgcda hgcd; apply/eqp_sym/(uniq_gcd _ _ _ hgcda). +rewrite /isgcd iffalse ?mulf_eq0 1:/#; do! split. +- by rewrite [a*_]mulrC dvdr_mul //; apply: dvdr_isgcdl hgcd. +- by rewrite [a*_]mulrC dvdr_mul //; apply: dvdr_isgcdr hgcd. +move=> d' d'_ba d'_ca; case: (Bezout _ _ _ hgcd) => cb cc <-. +by rewrite mulrDr !(mulrCA a) ![a*_]mulrC dvdrD dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvd_gcd (a b c d : t) : + isgcd b c d => a %| b => a %| c => a %| d. +proof. +rewrite /isgcd; case: (_ /\ _) => /=. +- by move=> -> _ _; apply: dvdr0. - by move=> [#] _ _; apply. +qed. + +(* -------------------------------------------------------------------- *) +lemma Gauss (a b c : t) : a %| b * c => coprime a b => a %| c. +proof. +move=> dvd_a_bc /coprime_isgcdP cop_ab. +have dvd_a_ac: a %| a * c by apply: dvdr_mulr. +have [d gcd_d] := gcd (a * c) (b * c). +have: d %= c by rewrite -[c]mulr1 &(isgcdMr _ _ gcd_d cop_ab). +by apply/dvdr_eqpR/(dvd_gcd _ _ gcd_d). +qed. + +(* -------------------------------------------------------------------- *) +op isdecomp (x : t) (xs : t list) = + x = BR.BMul.big predT idfun xs. + +(* -------------------------------------------------------------------- *) +op irreducible (x : t) = + (x <> zeror /\ !unit x) /\ forall y, y %| x => (unit y \/ x %= y). + +(* -------------------------------------------------------------------- *) +lemma irdc_neq0 (x : t) : irreducible x => x <> zeror. +proof. by move=> [/#]. qed. + +hint exact : irdc_neq0. + +(* -------------------------------------------------------------------- *) +lemma irdc_Nunit (x : t) : irreducible x => !unit x. +proof. by move=> [/#]. qed. + +(* -------------------------------------------------------------------- *) +lemma eqp_unit_mull (u x y : t) : unit u => (x %= u * y) <=> (x %= y). +proof. +move=> unit_u; split=> /eqmodfP[q [unit_q ->]]. +- by apply/eqmodP; exists (q * u); rewrite mulrA /= unitrM. +- apply/eqmodP; exists (q * invr u); rewrite unitrM unitrV; split=> //. + by rewrite -mulrA; congr; rewrite mulrA mulVr. +qed. + +(* -------------------------------------------------------------------- *) +lemma irdc_Ml (x y : t) : unit x => irreducible (x * y) <=> irreducible y. +proof. +move=> unit_x @/irreducible; split; last first. +- move=> [# nz_y Nunit_y irry]; do! split. + - by rewrite mulf_neq0 //; apply: contraL unit_x => ->; apply: unitr0. + - by rewrite unitrM Nunit_y. + move=> z dvdz; have: z %| y. + - case/dvdrP: dvdz=> q /(congr1 (( * ) (invr x))). + by rewrite !mulrA mulVr //= => ->; apply/dvdrP; exists (invr x * q). + by case/irry=> [->//|eq_zy]; right; apply/eqp_sym/eqp_unit_mull/eqp_sym. +- move=> [# nz_xMy + irr]; rewrite unitrM unit_x /= => Nunit_y. + do !split=> //; first by apply: contra nz_xMy => ->. + move=> z dvd_zy; have := irr z _; first by apply: dvdr_mull. + by case=> [->//|/eqp_sym /(eqp_unit_mull _ _ _ unit_x) /eqp_sym ?]; right. +qed. + +(* -------------------------------------------------------------------- *) +lemma isdecomp_nil (x : t) : isdecomp x [] <=> x = oner. +proof. by rewrite /isdecomp /BR.BMul.big BR.BMul.big_nil. qed. (* FIXME *) + +(* -------------------------------------------------------------------- *) +lemma isdecompM (x : t) (y : t) (ys : t list) : + isdecomp y ys => isdecomp (x * y) (x :: ys). +proof. +by move=> -> @/isdecomp; rewrite /BR.BMul.big BR.BMul.big_consT. (* FIXME *) +qed. + +(* -------------------------------------------------------------------- *) +lemma isdecomp_cons (x : t) (y : t) (ys : t list) : + isdecomp x (y :: ys) => exists z, x = y * z /\ isdecomp z ys. +proof. +move=> ->; pose z := BR.BMul.big predT idfun ys. +by exists z; rewrite /BR.BMul.big BR.BMul.big_consT. (* FIXME *) +qed. + +(* -------------------------------------------------------------------- *) +lemma irdc_coprime (x y : t) : + irreducible x => irreducible y => !(x %= y) => coprime x y. +proof. +move=> irr_x irr_y ne_xy a dvd_ax dvd_ay. +case: irr_x=> _ /(_ a dvd_ax); case: irr_y=> _ /(_ a dvd_ay). +by case: (unit a) => //=; smt(eqp_trans). +qed. + +(* -------------------------------------------------------------------- *) +lemma isdecomp_irdcMl (x y : t) (xs : t list) : + irreducible x => all irreducible xs => isdecomp (x * y) xs => + exists u ys, + unit u + /\ perm_eq xs ((u * x) :: ys) + /\ isdecomp (invr u * y) ys. +proof. +move=> irr_x irr_xs hdecomp; suff: exists x', x' \in xs /\ x %= x'. +- case=> x' [x'_in_xs /eqmodfP [u] [unit_u ->>]]. + exists (invr u) (rem x' xs); rewrite mulrA mulVr //= invrK. + rewrite unitrV unit_u /= perm_to_rem //=. + move: hdecomp => @/isdecomp @/BR.BMul.big. + rewrite (@BR.BMul.eq_big_perm _ _ _ _ (perm_to_rem x'_in_xs)). (* FIXME *) + rewrite BR.BMul.big_consT /= -mulrA mulrCA &(mulfI). + by apply: irdc_neq0; apply: irdc_Ml irr_x. +elim: xs x irr_x y irr_xs hdecomp => [|v vs ih] x irr_x y /=. +- by rewrite isdecomp_nil mulrC; apply/negP => /unitP; apply/irdc_Nunit. +case=> irr_v irr_vs hdecomp ; case: (x %= v)=> [eq_xv|ne_xv]. +- by exists v. +have cop_xv: coprime x v by apply: irdc_coprime. +move: (hdecomp) => @/isdecomp; rewrite /BR.BMul.big. +rewrite BR.BMul.big_consT /=; pose z := BigDom.BMul.big _ _ _. +move=> eq; have [dvdx dvdv]: x %| v * z /\ v %| x * y. +- split; apply/dvdrP. + - by exists y; rewrite [_*x]mulrC &(eq_sym). + - by exists z; rewrite [_*v]mulrC. +have: v %| y by apply/(Gauss _ dvdv)/coprimeC. +case/dvdrP=> k ->>; move: eq; rewrite mulrA [v*z]mulrC. +have nz_v: v <> zeror by apply: irdc_neq0. +move/(mulIf v nz_v) => {hdecomp} hdecomp. +have /# := ih x irr_x k irr_vs hdecomp. +qed. + +(* -------------------------------------------------------------------- *) +lemma unit_eqm (x y : t) : x %= y => unit x => unit y. +proof. by case/eqmodfP=> [u] [unit_u ->>] /(unitrMr _ _ unit_u). qed. + +(* -------------------------------------------------------------------- *) +lemma unitrP_eqm (x : t) : unit x <=> exists y, y * x %= oner. +proof. +rewrite unitrP; split; case=> y; first by move=> <-; exists y. +case/eqmodfP=> [u] [unit_u /= eq]; exists (y * invr u). +by rewrite mulrAC eq divrr. +qed. + +(* -------------------------------------------------------------------- *) +lemma perm_cons_eq ['a] (x y : 'a) (xs ys : 'a list) : + x = y => perm_eq (x :: xs) (y :: ys) <=> perm_eq xs ys. +proof. by move=> ->; apply/perm_cons. qed. + +(* -------------------------------------------------------------------- *) +lemma inj_bij_fin ['a] (f : 'a -> 'a) : + is_finite (fun x => f x <> x) + => injective f + => bijective f. +proof. +case=> s [uq_s memsP] inj_f; have dom: perm_eq s (map f s). +- apply/perm_eq_sym/uniq_perm_eq_size => //. + - by rewrite map_inj_in_uniq // => x y _ _; apply: inj_f. + - by rewrite size_map. + by move=> x /mapP[y] [y_in_s ->]; smt(). +pose g (y : 'a) := + if y \in map f s then nth y s (index y (map f s)) else y. +exists g; split. +- move=> x @/g; rewrite mem_map //; case: (x \in s). + - by move=> ?; rewrite index_map // nth_index. + - by rewrite memsP. +- move=> y @/g; case: (y \in map f s). + - case/mapP=> [x] [x_in_s ->>]; rewrite index_map //. + by rewrite nth_index //. + - by rewrite -(perm_eq_mem dom) memsP. +qed. + +(* -------------------------------------------------------------------- *) +op isperm (n : int) (f : int -> int) = + (forall i, 0 <= i < n => 0 <= f i < n) + /\ (forall i, !(0 <= i < n) => f i = i) + /\ (forall i j, 0 <= i < n => 0 <= j < n => i <> j => f i <> f j). + +(* -------------------------------------------------------------------- *) +lemma inj_isperm (n : int) (f : int -> int) : isperm n f => injective f. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma bij_isperm (n : int) (f : int -> int) : isperm n f => bijective f. +proof. +move=> pf; apply/inj_bij_fin/(inj_isperm n) => //. +apply/finiteP; exists (iota_ 0 n) => /=. +by move=> x; rewrite mem_iota /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma isperm_idfun (n : int) : isperm n idfun. +proof. done. qed. + +hint exact : isperm_idfun. + +(* -------------------------------------------------------------------- *) +lemma isperm_comp (n : int) (f g : int -> int) : + isperm n f => isperm n g => isperm n (f \o g). +proof. by rewrite /isperm /(\o); smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma ispermW (m n : int) (f : int -> int) : + m <= n => isperm m f => isperm n f. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +op shift1 (f : int -> int) = + fun i => if i = 0 then 0 else f (i - 1) + 1. + +(* -------------------------------------------------------------------- *) +lemma isperm_shift1 (m : int) (f : int -> int) : + isperm m f => isperm (m + 1) (shift1 f). +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma shift1_0E (f : int -> int) : shift1 f 0 = 0. +proof. done. qed. + +hint simplify shift1_0E. + +(* -------------------------------------------------------------------- *) +lemma shift1_nzE (f : int -> int) (i : int) : + i <> 0 => shift1 f i = f (i - 1) + 1. +proof. by move=> @/shift1 ->. qed. + +hint simplify shift1_0E. + +(* -------------------------------------------------------------------- *) +op rol1 (m : int) = + fun i => if 0 <= i < m then (i - 1) %% m else i. + +(* -------------------------------------------------------------------- *) +lemma isperm_rol1 (m n : int) : m <= n => isperm n (rol1 m). +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma rol1_0E (m : int) : 0 <= m => rol1 (m+1) 0 = m. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma rol1_psmallE (m i : int) : 0 < i <= m => rol1 (m+1) i = i-1. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +lemma rol1_bigE (m i : int) : 0 <= m => m < i => rol1 (m+1) i = i. +proof. smt(). qed. + +(* -------------------------------------------------------------------- *) +hint simplify drop0. +hint simplify index_cons. + +(* -------------------------------------------------------------------- *) +lemma rem_take_drop ['a] (x : 'a) (s : 'a list) : x \in s => + rem x s = take (index x s) s ++ drop (index x s + 1) s. +proof. +elim: s => //= y s ih; case: (x = y) => [<<-|ne_xy] //=. +move/ih => ->; rewrite [y=x]eq_sym ne_xy /=. +by rewrite !iffalse; ~-1:smt(index_ge0). +qed. + +(* -------------------------------------------------------------------- *) +lemma nth_rem ['a] (x0 : 'a) (x : 'a) (s : 'a list) (i : int) : + nth x0 (rem x s) i = + if i < index x s then nth x0 s i else nth x0 s (i+1). +proof. +case: (i < 0) => [lt0i|/lezNgt ge0_i]. +- by rewrite iftrue ?nth_neg //; smt(index_ge0). +elim: s i ge0_i => //= y s ih i ge0_i; rewrite [y=x]eq_sym. +case: (x = y) => [<<-|ne_xy]; first by smt(). +case: (i = 0) => [->>|nz_i] /=. +- by rewrite iftrue //; smt(index_ge0). +- by rewrite ih //#. +qed. + +(* -------------------------------------------------------------------- *) +lemma perm_eq_reindex ['a] (x0 : 'a) (s1 s2 : 'a list) : + perm_eq s1 s2 => exists (f : int -> int), + isperm (size s1) f + /\ (forall i, 0 <= i < size s1 => nth x0 s1 i = nth x0 s2 (f i)). +proof. +elim: s1 s2 => [|x1 s1 ih] s2. +- by move/perm_eq_size => /= /eq_sym /size_eq0 => -> /=; exists idfun. +move=> heq; have x1_in_s2: x1 \in s2 by move/perm_eq_mem: heq; apply. +have /= /eq_sym sz_s2 := perm_eq_size _ _ heq. +move/perm_to_rem/(perm_eq_trans _ _ _ heq)/perm_cons: (x1_in_s2). +case/ih=> f [permf eqnth]; pose j := index x1 s2. +pose g := rol1 (j+1) \o shift1 f; exists g; split. +- apply/isperm_comp. + - by apply: isperm_rol1; smt(index_mem). + - by rewrite addrC &(isperm_shift1). +move=> i [ge0i lti] @/g @/(\o) /=; case: (i = 0) => [->>|nz_i] /=. +- by rewrite rol1_0E 1:&(index_ge0) nth_index. +rewrite /shift1 nz_i /=; rewrite eqnth 1://# nth_rem -/j. +case: (f (i - 1) < j) => [lt_fPi_j|]. +- by rewrite rol1_psmallE 1:/#. +- by move=> ?; rewrite rol1_bigE ?index_ge0 //#. +qed. + +(* -------------------------------------------------------------------- *) +lemma perm_eq_of_perm ['a] (x0 : 'a) (f : int -> int) (s : 'a list) : + isperm (size s) f => perm_eq s (mkseq (fun i => nth x0 s (f i)) (size s)). +proof. +move=> pf; rewrite -{1}[s](@mkseq_nth x0). +rewrite -(@map_mkseq (fun i => nth x0 s i) f) /=. +apply: perm_eq_map => @/mkseq; move: (size s) pf => {s} n pf. +apply: uniq_perm_eq. +- by apply: iota_uniq. +- apply: map_inj_in_uniq. + - by move=> ?? _ _; apply: (inj_isperm _ _ pf). + by apply: iota_uniq. +move=> x; rewrite mem_iota /=; split; last first. +- by case/mapP=> y [/mem_iota /= rgy ->] /#. +- move=> rgx; apply/mapP; have := bij_isperm _ _ pf. + case=> g [can_fg can_gf]; exists (g x). + by rewrite mem_iota //#. +qed. + +(* -------------------------------------------------------------------- *) +lemma decomp_uniq (z1 z2 : t) (xs1 xs2 : t list) : + all irreducible xs1 + => all irreducible xs2 + => isdecomp z1 xs1 + => isdecomp z2 xs2 + => z1 %= z2 + => exists cs, + size cs = size xs2 + /\ all unit cs + /\ perm_eq xs1 (mkseq (fun i => cs.[i] * xs2.[i]) (size xs2)). +proof. +elim: xs1 z1 z2 xs2 => [|x1 xs1 ih] z1 z2 xs2 /=. +- move=> irdc_xs2 eq1x dcp2 eqz; have ->>: z1 = oner. + - by rewrite eq1x /(BR.BMul.big) BR.BMul.big_nil. + suff -> /=: xs2 = [] by exists [] => /=; rewrite mkseq0. + case: xs2 irdc_xs2 dcp2 => //= x2 xs2; case=> + _. + move/irdc_Nunit; apply: contra => /isdecomp_cons. + case=> [z] [/eq_sym eq _]; apply/unitrP_eqm. + by exists z; rewrite mulrC eq eqp_sym. +case=> irdc_x1 irdc_xs1 irdc_xs2 /isdecomp_cons [x'] [->> dcp_xs1] dcp_xs2. +case/eqmodfP=> [w] [unit_w]; move/(congr1 (( * ) (invr w))). +rewrite !mulrA mulVr //= => <<-. +have := isdecomp_irdcMl (invr w * x1) x' xs2 _ irdc_xs2 dcp_xs2. +- by apply/(irdc_Ml _); first by apply/unitrV. +case=> [u ys] [# unit_u eq_xs2 dcp_ys]. +wlog: xs2 irdc_xs2 dcp_xs2 eq_xs2 / (xs2 = (u * (invr w * x1)) :: ys). +- move=> /(_ ((u * (invr w * x1)) :: ys) _ _ _ _) => //. + - apply/allP=> z /=; case=> [->|]. + - by do! apply/irdc_Ml => //; apply/unitrV. + move=> ?; move/allP: irdc_xs2; apply. + by move/perm_eq_mem: eq_xs2 => -> /=; right. + - rewrite /isdecomp /(BR.BMul.big) BR.BMul.big_consT /=. + apply/(mulrI (w * invr u) _). + - by apply/unitrM; split=> //; apply/unitrV. + rewrite -[_ * BigDom.BMul.big _ _ _]mulrA; congr. + rewrite [u*_]mulrC -!mulrA; do 2! congr. + apply/(mulrI (invr u)); first by apply/unitrV. + by rewrite mulrA dcp_ys mulrAC mulVr. + - by apply: perm_eq_refl. + case=> cs [# eq_sz unit_cs]; + move/perm_eq_size: (eq_xs2) eq_sz => /= <- eq_sz heq. + case/(perm_eq_reindex zeror): eq_xs2 => f. + move=> [# permf hreindex]. + pose ds := mkseq (fun i => cs.[f i]) (size xs2); exists ds. + do 2? split. + - by rewrite size_mkseq lez_maxr ?size_ge0. + - apply/allP => x /mkseqP[i] [rgi /= ->]. + by move/allP: unit_cs => /(_ cs.[f i]); apply; apply/mem_nth => /#. + move/perm_eqlE: heq => ->; pose s := mkseq _ _. + have szsE: size s = size xs2. + - by rewrite size_mkseq lez_maxr ?size_ge0. + have := perm_eq_of_perm zeror f s _; first by rewrite szsE. + move/perm_eqlE; apply; apply/perm_eq_refl_eq. + rewrite szsE &(eq_in_mkseq) => /= i [ge0i lti]. + by rewrite !nth_mkseq ~-1:/# /= hreindex. +move=> {eq_xs2} ->> /=; move: irdc_xs2 => /= [_ irdc_ys]. +have := ih x' (invr u * x') ys irdc_xs1 irdc_ys dcp_xs1 dcp_ys _. +- by apply/eqmodfP; exists u; rewrite mulrA divrr. +case=> cs [# eq_sz unit_cs eqp]. +exists ((w * invr u) :: cs); do 2? split => //=. +- by rewrite eq_sz. +- by rewrite unit_cs /=; rewrite unitrM unitrV. +rewrite [1+_]addrC mkseqSr ?size_ge0 /= &(perm_cons_eq). +- by rewrite !mulrA [_ * u]mulrAC mulrK // divrr. +move/perm_eqlE: eqp; apply; apply/perm_eq_refl_eq/eq_in_mkseq. +by move=> @/(\o) /= i [ge0i lti]; rewrite add1z_neq0. +qed. + +(* -------------------------------------------------------------------- *) +lemma Gauss_dvdr (a b c : t) : coprime a b => (a %| b * c) <=> (a %| c). +proof. by move=> cop_a_b; split; [move/Gauss; apply | apply: dvdr_mull]. qed. + +(* -------------------------------------------------------------------- *) +lemma Gauss_dvdl (a b c : t) : coprime a c => (a %| b * c) <=> (a %| b). +proof. by move=> ?; rewrite mulrC; apply: Gauss_dvdr. qed. + +(* -------------------------------------------------------------------- *) +lemma coprime_eqmr (a b b' : t) : coprime a b => b %= b' => coprime a b'. +proof. +move=> cop /eqp_sym eq x dvda dvdb'. +by apply: cop => //; apply: dvdr_eqpR eq. +qed. + +(* -------------------------------------------------------------------- *) +lemma coprime_eqml (a a' b : t) : coprime a b => a %= a' => coprime a' b. +proof. by rewrite ![coprime _ b]coprimeC; apply: coprime_eqmr. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr1 (a : t) : a %| oner <=> a %= oner. +proof. by rewrite -eqmodf1P unitrP /#. qed. + +(* -------------------------------------------------------------------- *) +lemma coprime1r (a : t) : coprime oner a. +proof. by move=> x /dvdr1 /eqmodf1P. qed. + +(* -------------------------------------------------------------------- *) +lemma coprimer1 (a : t) : coprime a oner. +proof. by rewrite coprimeC &(coprime1r). qed. + +(* -------------------------------------------------------------------- *) +lemma coprime0r_unit (a : t) : coprime zeror a => unit a. +proof. by move=> /(_ a); apply=> //; apply: dvdr0. qed. + +(* -------------------------------------------------------------------- *) +lemma coprimer0_unit (a : t) : coprime a zeror => unit a. +proof. by move/coprimeC/coprime0r_unit. qed. + +(* -------------------------------------------------------------------- *) +lemma eqpC (x y : t) : (x %= y) <=> (y %= x). +proof. by split=> /eqp_sym. qed. + +(* -------------------------------------------------------------------- *) +lemma dvd1r (a : t) : oner %| a. +proof. by exists a. qed. + +(* -------------------------------------------------------------------- *) +lemma coprimeP (a b : t) : + coprime a b <=> exists (u v : t), u * a + v * b = oner. +proof. +split; first by move=> /coprime_isgcdP /Bezout. +case=> u v eq; apply/coprime_isgcdP => @/isgcd; do! split => /=. +- by case=> ->> ->>; move: eq => /= => ->. +move=> nz_aAb; rewrite !dvd1r /= => d' dvda dvdb. +by rewrite -eq dvdrD dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma Gauss_gcdr (c a b d : t) : + coprime c a => isgcd c (a * b) d <=> isgcd c b d. +proof. +case: (c = zeror) => [->|nz_c]. +- move/coprime0r_unit => unit_a; rewrite !isgcd0r_eqm. + by rewrite ![_ %= d]eqpC eqp_unit_mull. +move=> cop_ca; split => @/isgcd; rewrite nz_c /=; last first. +- move=> [# dvd_c dvd_d mind]; do! split => //. + - by rewrite dvdr_mull. + - move=> d' dvd'_c dvd'_ab; apply: mind=> //. + suff: coprime d' a by move/Gauss_dvdr; apply. + case/coprimeP: cop_ca=> u v eq; apply/coprimeP. + by case/dvdrP: dvd'_c => q ->>; exists (u*q) v; ring eq. +- move=> [# dvd_c dvd_ab mind]; do! split => //. + - suff: coprime d a by move/Gauss_dvdr; apply. + case/coprimeP: cop_ca=> u v eq; apply/coprimeP. + by case/dvdrP: dvd_c => q ->>; exists (u*q) v; ring eq. + - by move=> d' dvd'_c dvd'_b; apply: mind => //; apply: dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma Gauss_gcdl (c a b d : t) : + coprime c b => isgcd c (a * b) d <=> isgcd c a d. +proof. by move=> ?; rewrite mulrC &(Gauss_gcdr). qed. + +(* -------------------------------------------------------------------- *) +lemma coprimeMr (c a b : t) : + coprime c (a * b) <=> (coprime c a /\ coprime c b). +proof. +case: (coprime c a) => /= cop_c_a. +- by rewrite -!coprime_isgcdP Gauss_gcdr. +apply: contra cop_c_a => /coprimeP [u v] eq; apply/coprimeP. +by exists u (v * b); ring eq. +qed. + +(* -------------------------------------------------------------------- *) +lemma coprimeMl (c a b : t) : + coprime (a * b) c <=> (coprime a c /\ coprime b c). +proof. by rewrite coprimeC coprimeMr ![coprime c _]coprimeC. qed. + +(* -------------------------------------------------------------------- *) +lemma coprime_prod ['a] (P : 'a -> bool) (F : 'a -> t) (c : t) (cs : 'a list) : + (forall i, i \in cs => P i => coprime (F i) c) + => coprime (BR.BMul.big P F cs) c. +proof. +move=> @/BR.BMul.big; elim: cs => /= [|x xs ih]. (* FIXME *) +- by rewrite BR.BMul.big_nil coprime1r. +move=> cop; rewrite BR.BMul.big_cons; case: (P x); last smt(). +by move=> Px; apply/coprimeMl => /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_sum ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) : + (forall c, c \in cs => P c => a %| F c) + => a %| BR.BAdd.big P F cs. +proof. +elim: cs => [|c cs ih] hdvd @/BR.BAdd.big //=. (* FIXME *) +- by rewrite BR.BAdd.big_nil dvdr0. +rewrite BR.BAdd.big_cons; case: (P c) => Pc /=; last first. +- by apply/ih=> *; apply/hdvd => //#. +- rewrite dvdrD; first by apply: hdvd. + by apply/ih=> *; apply/hdvd => /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_prod ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) (x : 'a) : + x \in cs => P x => a %| F x => a %| BR.BMul.big P F cs. +proof. +move=> x_in_cs Px dvd_a_Fx @/BR.BMul.big. +move/perm_to_rem: x_in_cs => /BR.BMul.eq_big_perm ->. +by rewrite BR.BMul.big_cons Px /= dvdr_mulr. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrN (a b : t) : a %| b => a %| -b. +proof. by case=> c ->; exists (-c); rewrite mulNr. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrB (d a b : t) : d %| a => d %| b => d %| (a - b). +proof. by move=> ??; apply/dvdrD/dvdrN. qed. + +(* -------------------------------------------------------------------- *) +lemma crt (rs : (t * t) list) : + (forall i j, + 0 <= i < size rs => 0 <= j < size rs => i <> j => + coprime (nth witness rs i).`2 (nth witness rs j).`2) + => exists (x : t), all (fun (an : _ * _) => idgen [an.`2] (x - an.`1)) rs. +proof. +move=> hcop; pose k := size rs. +pose a i := (nth witness rs i).`1. +pose n i := (nth witness rs i).`2. +pose N i := BR.BMul.bigi ((<>) i) n 0 k. +have copN: forall i, 0 <= i < k => coprime (N i) (n i). +- move=> i rgi; apply: coprime_prod => j /mem_range /= [ge0_j ltj] ne_ij. + by (have := hcop i j _ _ ne_ij; ~-1: done); rewrite coprimeC. +pose P i (Mm : _ * _) := Mm.`1 * N i + Mm.`2 * n i = oner. +pose B i := choiceb (P i) witness. +pose M i := (B i).`1; pose m i := (B i).`2. +have hsol: forall i, 0 <= i < k => M i * N i + m i * n i = oner. +- move=> i rgi @/M @/n @/B; have := choicebP (P i) witness _; last done. + have := Bezout (N i) (n i) oner _; first by apply/coprime_isgcdP/copN. + by case=> Mi mi ?; exists (Mi, mi). +pose x := BR.BAdd.bigi predT (fun i => a i * M i * N i) 0 k. +exists x; apply/(@all_nthP _ _ witness) => i rgi /=. +rewrite -/(n i) -/(a i) /x /BR.BAdd.big (@BR.BAdd.bigD1 _ _ i) /=. +- by rewrite mem_range. - by apply: range_uniq. +rewrite addrAC &(@idealD (idgen [n i])); 1: solve; last first. (* FIXME *) +- apply/mem_idgen1_dvd/dvdr_sum=> j /mem_range rgj @/predC1 ne_ji /=. + by rewrite &(dvdr_mull) &(dvdr_prod i) ?mem_range. +have := hsol i rgi; move/(congr1 (( * ) (a i))) => /=. +rewrite mulrDr !mulrA eq_sym -subr_eq => <-. +by rewrite addrAC subrr /= mem_idgen1_dvd dvdrN dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrMl_coprime (a1 a2 b : t) : + coprime a1 a2 => a1 %| b => a2 %| b => a1 * a2 %| b. +proof. +move=> cop dvd1 dvd2; case/dvdrP: dvd1=> q ->>. +rewrite [_*a1]mulrC dvdr_mul //. +by move/coprimeC/Gauss_dvdl: cop => <-. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_prodl_coprime ['a] (F : 'a -> t) (cs : 'a list) (a : t) : + (forall i j, 0 <= i < size cs => 0 <= j < size cs => i <> j => + coprime (F (nth witness cs i)) (F (nth witness cs j))) + => all (fun b => b %| a) (map F cs) + => BR.BMul.big predT F cs %| a. +proof. +elim: cs => [|c cs ih] hcop hdvd /= @/BR.BMul.big. +- by rewrite BR.BMul.big_nil dvd1r. +rewrite BR.BMul.big_consT dvdrMl_coprime. +- apply/coprimeC/coprime_prod => b b_in_cs _. + have := hcop (1 + index b cs) 0 _ _ _ => /=; + ~-1: smt(index_ge0 size_ge0 index_mem). + by rewrite add1z_neq0 ?index_ge0 /= nth_index. +- by move: hdvd => /= [+ _]; apply. +- apply: ih; last by move: hdvd=> /= [_]; apply. + move=> i j rgi rgj ne_ij. +have /= := hcop (i + 1) (j + 1) _ _ _; ~-1: smt(). +by rewrite ![_+1]addrC !add1z_neq0 //#. +qed. + +(* -------------------------------------------------------------------- *) +lemma crt_uniq (rs : (t * t) list) (x1 x2 : t) : + (forall i j, + 0 <= i < size rs => 0 <= j < size rs => i <> j => + coprime (nth witness rs i).`2 (nth witness rs j).`2) + => all (fun (an : _ * _) => idgen [an.`2] (x1 - an.`1)) rs + => all (fun (an : _ * _) => idgen [an.`2] (x2 - an.`1)) rs + => idgen [BR.BMul.big predT (fun an : _ * _ => an.`2) rs] (x2 - x1). +proof. +move=> hcop sol1 sol2; rewrite mem_idgen1_dvd &(dvdr_prodl_coprime) //. +rewrite all_map /preim; apply/allP=> y y_rs /=. +have ->: x2 - x1 = x2 - y.`1 - (x1 - y.`1) by ring. +by apply/dvdrB; [ + move/allP/(_ _ y_rs): sol2 => /= + | move/allP/(_ _ y_rs): sol1 => /= + ]; move/mem_idgen1_dvd. +qed. + +(* -------------------------------------------------------------------- *) +lemma neotherian (sI : int -> (t -> bool)) : + (forall i j, 0 <= i <= j => sI i <= sI j) + => (forall i, 0 <= i => ideal (sI i)) + => exists (k : int), 0 <= k /\ (forall i, k <= i => sI k = sI i). +proof. +move=> mono idI; pose I (x : t) := exists k, 0 <= k /\ sI k x. +have: ideal I by (do! split); smt(). +move/principal/principalP=> [a] ^IE /fun_ext /(_ a). +rewrite mem_idgen1_gen eqT; case=> k [ge0k sIa]. +exists k; split=> // i le_ki; apply/predeq_leP. +split; first by apply/mono => //#. +move=> x sIx; have: I x by exists i => //#. +rewrite IE => /mem_idgen1[b ->]. +by apply: (@idealMl (sI k)) => //; apply: idI. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrW (P : t -> bool) : + (forall (a : t), (forall (b : t), b %| a => !(a %= b) => P b) => P a) + => forall a, P a. +proof. +suff hwf: + forall (X : t -> bool), (exists x, X x) => + exists x, X x /\ (forall y, X y => y %| x => x %= y). +- move=> ih a; apply: contraT => NPa; pose X a := !P a. + by have := hwf X _; [by exists a | smt()]. +move=> X [a Xa]; apply: contraT; rewrite negb_exists /=; apply/negP=> Nwf. +pose Q b c := X c /\ c %| b /\ !(b %= c). +have {Nwf} Nwf: forall b, X b => exists c, Q b c by smt(). +pose f x := choiceb (fun y => Q x y) witness. +pose s (i : int) := iter i f a. +have siS: forall i, 0 <= i => s (i + 1) = f (s i) by smt(iterS). +have: forall i, 0 <= i => X (s i). +- elim=> [|i ge0i ih] @/s /=; [by rewrite iter0 | rewrite iterS //]. + by have @/Q := choicebP (Q (iter i f a)) witness (Nwf _ ih). +move=> sX; (have: forall i, 0 <= i => Q (s i) (s (i + 1))) => [i ge0i|]. +- have := choicebP (Q (s i)) witness (Nwf _ (sX _ ge0i)). + by rewrite siS //; apply. +move=> {Nwf siS sX}; move: s => {f} s Qs. +(have := neotherian (fun i => idgen [s i]) _ _) => /=. +- move=> i j [ge0i ltij]; apply: le_idgen1_dvd. + rewrite (_ : j = i + (j - i)) 1:#ring. + have: 0 <= j - i by smt(). + elim: (j - i) => {j ltij} //= j ge0j ih. + by rewrite addrA (dvdr_trans _ _ ih) /#. +- by move=> i _; apply: ideal_idgen. +apply/negP; case=> [k] [ge0k] /(_ (k+1) _); first smt(). +by move/eqmodf_idP; have := Qs k; smt(). +qed. + +(* -------------------------------------------------------------------- *) +lemma irreducibleNP (x : t) : x <> zeror => !unit x => !irreducible x => + exists y z, + ( (y <> zeror /\ !unit y) + /\ (z <> zeror /\ !unit z)) + /\ (x = y * z). +proof. +move=> @/irreducible ^nz_x -> -> /=; rewrite negb_forall /=. +case=> a; case/negb_imply => dvd_ax /negb_or[Nunit_a ne_xa]. +case/dvdrP: dvd_ax => b ->>; exists b a => //=. +rewrite Nunit_a /=; move: nz_x; rewrite mulf_eq0. +case/negb_or=> -> -> /=; apply: contraLR ne_xa => /=. +by move/eqp_unit_mull => h; apply/eqpC/h. +qed. + +(* -------------------------------------------------------------------- *) +lemma isdecomp_cat (x y : t) (xs ys : t list) : + isdecomp x xs => isdecomp y ys => isdecomp (x * y) (xs ++ ys). +proof. +move=> xsE ysE @/isdecomp @/BR.BMul.big. (* FIXME *) +by rewrite BR.BMul.big_cat xsE ysE. +qed. + +(* -------------------------------------------------------------------- *) +lemma decomp (x : t) : x <> zeror => !unit x => + exists xs, all irreducible xs /\ isdecomp x xs. +proof. +elim/dvdrW: x => x ih; case: (irreducible x). +- by move=> irr_x _ _; exists [x]. +move=> + nz_x Nunit_x - /(irreducibleNP x nz_x Nunit_x). +case=> y z [#] nz_y ? nz_z ? ->>. +have := ih y _ _ _ _ => //; first by rewrite dvdr_mulr. +- rewrite mulrC; apply/negP => /eqmodfP[u]. + by case=> [unit_u /(@mulIf _ nz_y) ->>]. +have := ih z _ _ _ _ => //; first by rewrite dvdr_mull. +- by apply/negP => /eqmodfP[u] [unit_u /(@mulIf _ nz_z) ->>]. +case=> [ys] [irr_ys ysE] [zs] [irr_zs zsE]. +exists (zs ++ ys); rewrite all_cat !(irr_ys, irr_zs) /=. +by apply: isdecomp_cat. +qed. From 7ad5f04be1854cf509699e8c9626025f724a19c9 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 16:49:23 +0200 Subject: [PATCH 02/21] CommAlgebra: witness-level (comax) CRT layer Introduce comax x y = exists u v, u*x + v*y = oner and restate the CRT cluster against it, before the Euclidean structure: comax_Gauss, comaxMr/Ml/prod, dvdrMl_comax, dvdr_prodl_comax, crt_comax, crt_uniq_comax. These consume co-primality only through the Bezout witnesses, so instances can supply the witnesses directly (e.g. binomial moduli X^n - c1, X^n - c2, whose witnesses are constants) without going through gcds -- i.e. without the Euclide axiom. The generic divisibility lemmas the cluster relies on (dvdr_mul, dvdrD, dvdrN, dvdrB, dvd1r, dvdr_sum, dvdr_prod) move up above the Euclidean axioms, unchanged. comax_coprime is immediate in any domain; coprime_comax is Bezout (comax = coprime characterizes Bezout domains). crt and crt_uniq keep their statements and become corollaries of the witness-level versions. --- theories/algebra/CommAlgebra.ec | 290 +++++++++++++++++++++++--------- 1 file changed, 214 insertions(+), 76 deletions(-) diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec index 4743c4fa7..5e8026f11 100644 --- a/theories/algebra/CommAlgebra.ec +++ b/theories/algebra/CommAlgebra.ec @@ -92,6 +92,198 @@ qed. hint simplify [reduce] addi0. +(* -------------------------------------------------------------------- *) +lemma dvdr_mul (a b a' b' : t) : a %| b => a' %| b' => a * a' %| b * b'. +proof. +move=> /dvdrP[d ->] /dvdrP[d' ->]; rewrite mulrACA. +by apply/dvdrP; exists (d * d'). +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrD (d a b : t) : d %| a => d %| b => d %| (a + b). +proof. by move=> /dvdrP[ca ->] /dvdrP[cb ->]; rewrite -mulrDl dvdr_mull. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrN (a b : t) : a %| b => a %| -b. +proof. by case=> c ->; exists (-c); rewrite mulNr. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrB (d a b : t) : d %| a => d %| b => d %| (a - b). +proof. by move=> ??; apply/dvdrD/dvdrN. qed. + +(* -------------------------------------------------------------------- *) +lemma dvd1r (a : t) : oner %| a. +proof. by exists a. qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_sum ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) : + (forall c, c \in cs => P c => a %| F c) + => a %| BR.BAdd.big P F cs. +proof. +elim: cs => [|c cs ih] hdvd @/BR.BAdd.big //=. (* FIXME *) +- by rewrite BR.BAdd.big_nil dvdr0. +rewrite BR.BAdd.big_cons; case: (P c) => Pc /=; last first. +- by apply/ih=> *; apply/hdvd => //#. +- rewrite dvdrD; first by apply: hdvd. + by apply/ih=> *; apply/hdvd => /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_prod ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) (x : 'a) : + x \in cs => P x => a %| F x => a %| BR.BMul.big P F cs. +proof. +move=> x_in_cs Px dvd_a_Fx @/BR.BMul.big. +move/perm_to_rem: x_in_cs => /BR.BMul.eq_big_perm ->. +by rewrite BR.BMul.big_cons Px /= dvdr_mulr. +qed. + +(* ==================================================================== *) +(* Co-maximality, with explicit Bezout witnesses. The CRT cluster is *) +(* stated at this level: it consumes co-primality only through the *) +(* witnesses, so that instances can supply them directly, without any *) +(* recourse to gcds (e.g. binomial moduli X^n - c1, X^n - c2, whose *) +(* witnesses are constants). The Euclidean structure below closes the *) +(* gap in the other direction (coprime => comax, via Bezout). *) +(* ==================================================================== *) +op comax (x y : t) = exists u v, u * x + v * y = oner. + +(* -------------------------------------------------------------------- *) +lemma comaxC (x y : t) : comax x y <=> comax y x. +proof. by split; case=> u v h; exists v u; rewrite addrC. qed. + +(* -------------------------------------------------------------------- *) +lemma comaxr1 (x : t) : comax x oner. +proof. by exists zeror oner; rewrite mul0r mulr1 add0r. qed. + +(* -------------------------------------------------------------------- *) +lemma comax1r (y : t) : comax oner y. +proof. by rewrite comaxC comaxr1. qed. + +(* -------------------------------------------------------------------- *) +lemma comax_Gauss (a b c : t) : comax a b => a %| b * c => a %| c. +proof. +case=> u v huv hdvd. +have h1 : c * (u * a + v * b) = c by rewrite huv mulr1. +have -> : c = u * c * a + v * (b * c). +- by rewrite -{1}h1; ring. +apply/dvdrD. +- by apply/dvdr_mull/dvdrr. +- by apply/dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma comaxMr (a b c : t) : comax a b => comax a c => comax a (b * c). +proof. +case=> u1 v1 h1; case=> u2 v2 h2. +exists (u1 * u2 * a + u1 * v2 * c + v1 * b * u2) (v1 * v2). +have h : (u1 * a + v1 * b) * (u2 * a + v2 * c) = oner. +- by rewrite h1 h2 mulr1. +by rewrite -h; ring. +qed. + +(* -------------------------------------------------------------------- *) +lemma comaxMl (a b c : t) : comax a c => comax b c => comax (a * b) c. +proof. +move=> h1 h2; rewrite comaxC; apply comaxMr. +- by rewrite comaxC. +- by rewrite comaxC. +qed. + +(* -------------------------------------------------------------------- *) +lemma comax_prod ['a] (P : 'a -> bool) (F : 'a -> t) (c : t) (cs : 'a list) : + (forall i, i \in cs => P i => comax (F i) c) + => comax (BR.BMul.big P F cs) c. +proof. +elim: cs => [|x xs ih] hcm @/BR.BMul.big. +- by rewrite BR.BMul.big_nil comax1r. +rewrite BR.BMul.big_cons; case: (P x) => Px; last by apply/ih => /#. +apply/comaxMl. +- by apply/hcm. +- by apply/ih => /#. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdrMl_comax (a1 a2 b : t) : + comax a1 a2 => a1 %| b => a2 %| b => a1 * a2 %| b. +proof. +move=> cm dvd1 dvd2; case/dvdrP: dvd1=> q ->>. +rewrite [q * a1]mulrC dvdr_mul //. +apply (@comax_Gauss a2 a1 q). +- by rewrite comaxC. +- by rewrite mulrC. +qed. + +(* -------------------------------------------------------------------- *) +lemma dvdr_prodl_comax ['a] (F : 'a -> t) (cs : 'a list) (a : t) : + (forall i j, 0 <= i < size cs => 0 <= j < size cs => i <> j => + comax (F (nth witness cs i)) (F (nth witness cs j))) + => all (fun b => b %| a) (map F cs) + => BR.BMul.big predT F cs %| a. +proof. +elim: cs => [|c cs ih] hcm hdvd /= @/BR.BMul.big. +- by rewrite BR.BMul.big_nil dvd1r. +rewrite BR.BMul.big_consT dvdrMl_comax. +- apply/comaxC/comax_prod => b b_in_cs _. + have := hcm (1 + index b cs) 0 _ _ _ => /=; + ~-1: smt(index_ge0 size_ge0 index_mem). + by rewrite add1z_neq0 ?index_ge0 /= nth_index. +- by move: hdvd => /= [+ _]; apply. +- apply: ih; last by move: hdvd=> /= [_]; apply. + move=> i j rgi rgj ne_ij. + have /= := hcm (i + 1) (j + 1) _ _ _; ~-1: smt(). + by rewrite ![_+1]addrC !add1z_neq0 //#. +qed. + +(* -------------------------------------------------------------------- *) +lemma crt_comax (rs : (t * t) list) : + (forall i j, + 0 <= i < size rs => 0 <= j < size rs => i <> j => + comax (nth witness rs i).`2 (nth witness rs j).`2) + => exists (x : t), all (fun (an : _ * _) => idgen [an.`2] (x - an.`1)) rs. +proof. +move=> hcm; pose k := size rs. +pose a i := (nth witness rs i).`1. +pose n i := (nth witness rs i).`2. +pose N i := BR.BMul.bigi ((<>) i) n 0 k. +have cmN: forall i, 0 <= i < k => comax (N i) (n i). +- move=> i rgi; apply: comax_prod => j /mem_range /= [ge0_j ltj] ne_ij. + by (have := hcm i j _ _ ne_ij; ~-1: done); rewrite comaxC. +pose P i (Mm : _ * _) := Mm.`1 * N i + Mm.`2 * n i = oner. +pose B i := choiceb (P i) witness. +pose M i := (B i).`1; pose m i := (B i).`2. +have hsol: forall i, 0 <= i < k => M i * N i + m i * n i = oner. +- move=> i rgi @/M @/n @/B; have := choicebP (P i) witness _; last done. + by case: (cmN i rgi) => Mi mi ?; exists (Mi, mi). +pose x := BR.BAdd.bigi predT (fun i => a i * M i * N i) 0 k. +exists x; apply/(@all_nthP _ _ witness) => i rgi /=. +rewrite -/(n i) -/(a i) /x /BR.BAdd.big (@BR.BAdd.bigD1 _ _ i) /=. +- by rewrite mem_range. - by apply: range_uniq. +rewrite addrAC &(@idealD (idgen [n i])); 1: solve; last first. (* FIXME *) +- apply/mem_idgen1_dvd/dvdr_sum=> j /mem_range rgj @/predC1 ne_ji /=. + by rewrite &(dvdr_mull) &(dvdr_prod i) ?mem_range. +have := hsol i rgi; move/(congr1 (( * ) (a i))) => /=. +rewrite mulrDr !mulrA eq_sym -subr_eq => <-. +by rewrite addrAC subrr /= mem_idgen1_dvd dvdrN dvdr_mull. +qed. + +(* -------------------------------------------------------------------- *) +lemma crt_uniq_comax (rs : (t * t) list) (x1 x2 : t) : + (forall i j, + 0 <= i < size rs => 0 <= j < size rs => i <> j => + comax (nth witness rs i).`2 (nth witness rs j).`2) + => all (fun (an : _ * _) => idgen [an.`2] (x1 - an.`1)) rs + => all (fun (an : _ * _) => idgen [an.`2] (x2 - an.`1)) rs + => idgen [BR.BMul.big predT (fun an : _ * _ => an.`2) rs] (x2 - x1). +proof. +move=> hcm sol1 sol2; rewrite mem_idgen1_dvd &(dvdr_prodl_comax) //. +rewrite all_map /preim; apply/allP=> y y_rs /=. +have ->: x2 - x1 = x2 - y.`1 - (x1 - y.`1) by ring. +by apply/dvdrB; [ + move/allP/(_ _ y_rs): sol2 => /= + | move/allP/(_ _ y_rs): sol1 => /= + ]; move/mem_idgen1_dvd. +qed. + (* -------------------------------------------------------------------- *) op w : t -> int. @@ -114,6 +306,16 @@ op coprime (x y : t) = lemma coprimeC (x y : t) : coprime x y <=> coprime y x. proof. smt(). qed. +(* -------------------------------------------------------------------- *) +lemma comax_coprime (x y : t) : comax x y => coprime x y. +proof. +case=> u v huv d dx dy. +have hd : d %| oner. +- rewrite -huv; apply/dvdrD; by apply/dvdr_mull. +case: hd => c hc; apply/unitrP; exists c. +by rewrite -hc. +qed. + (* -------------------------------------------------------------------- *) lemma Ncoprime0 : coprime zeror zeror => false. proof. @@ -321,16 +523,17 @@ proof. split. qed. (* -------------------------------------------------------------------- *) -lemma isgcd00 d : isgcd zeror zeror d => d = zeror. -proof. done. qed. - -(* -------------------------------------------------------------------- *) -lemma dvdr_mul (a b a' b' : t) : a %| b => a' %| b' => a * a' %| b * b'. +lemma coprime_comax (x y : t) : coprime x y => comax x y. proof. -move=> /dvdrP[d ->] /dvdrP[d' ->]; rewrite mulrACA. -by apply/dvdrP; exists (d * d'). +move=> cop; have := Bezout x y oner _. +- by apply/coprime_isgcdP. +by case=> u v h; exists u v. qed. +(* -------------------------------------------------------------------- *) +lemma isgcd00 d : isgcd zeror zeror d => d = zeror. +proof. done. qed. + (* -------------------------------------------------------------------- *) lemma isgcd0r (a : t) : isgcd zeror a a. proof. @@ -376,10 +579,6 @@ proof. by move: a b d; apply/isgcdW. qed. lemma dvdr_isgcdr (a b d : t) : isgcd a b d => d %| b. proof. by move: a b d; apply/isgcdW. qed. -(* -------------------------------------------------------------------- *) -lemma dvdrD (d a b : t) : d %| a => d %| b => d %| (a + b). -proof. by move=> /dvdrP[ca ->] /dvdrP[cb ->]; rewrite -mulrDl dvdr_mull. qed. - (* -------------------------------------------------------------------- *) lemma isgcdMr (a b c : t) (da d : t) : isgcd (b * a) (c * a) da => isgcd b c d => da %= a * d. @@ -817,10 +1016,6 @@ proof. by move/coprimeC/coprime0r_unit. qed. lemma eqpC (x y : t) : (x %= y) <=> (y %= x). proof. by split=> /eqp_sym. qed. -(* -------------------------------------------------------------------- *) -lemma dvd1r (a : t) : oner %| a. -proof. by exists a. qed. - (* -------------------------------------------------------------------- *) lemma coprimeP (a b : t) : coprime a b <=> exists (u v : t), u * a + v * b = oner. @@ -884,36 +1079,6 @@ move=> cop; rewrite BR.BMul.big_cons; case: (P x); last smt(). by move=> Px; apply/coprimeMl => /#. qed. -(* -------------------------------------------------------------------- *) -lemma dvdr_sum ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) : - (forall c, c \in cs => P c => a %| F c) - => a %| BR.BAdd.big P F cs. -proof. -elim: cs => [|c cs ih] hdvd @/BR.BAdd.big //=. (* FIXME *) -- by rewrite BR.BAdd.big_nil dvdr0. -rewrite BR.BAdd.big_cons; case: (P c) => Pc /=; last first. -- by apply/ih=> *; apply/hdvd => //#. -- rewrite dvdrD; first by apply: hdvd. - by apply/ih=> *; apply/hdvd => /#. -qed. - -(* -------------------------------------------------------------------- *) -lemma dvdr_prod ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) (x : 'a) : - x \in cs => P x => a %| F x => a %| BR.BMul.big P F cs. -proof. -move=> x_in_cs Px dvd_a_Fx @/BR.BMul.big. -move/perm_to_rem: x_in_cs => /BR.BMul.eq_big_perm ->. -by rewrite BR.BMul.big_cons Px /= dvdr_mulr. -qed. - -(* -------------------------------------------------------------------- *) -lemma dvdrN (a b : t) : a %| b => a %| -b. -proof. by case=> c ->; exists (-c); rewrite mulNr. qed. - -(* -------------------------------------------------------------------- *) -lemma dvdrB (d a b : t) : d %| a => d %| b => d %| (a - b). -proof. by move=> ??; apply/dvdrD/dvdrN. qed. - (* -------------------------------------------------------------------- *) lemma crt (rs : (t * t) list) : (forall i j, @@ -921,30 +1086,8 @@ lemma crt (rs : (t * t) list) : coprime (nth witness rs i).`2 (nth witness rs j).`2) => exists (x : t), all (fun (an : _ * _) => idgen [an.`2] (x - an.`1)) rs. proof. -move=> hcop; pose k := size rs. -pose a i := (nth witness rs i).`1. -pose n i := (nth witness rs i).`2. -pose N i := BR.BMul.bigi ((<>) i) n 0 k. -have copN: forall i, 0 <= i < k => coprime (N i) (n i). -- move=> i rgi; apply: coprime_prod => j /mem_range /= [ge0_j ltj] ne_ij. - by (have := hcop i j _ _ ne_ij; ~-1: done); rewrite coprimeC. -pose P i (Mm : _ * _) := Mm.`1 * N i + Mm.`2 * n i = oner. -pose B i := choiceb (P i) witness. -pose M i := (B i).`1; pose m i := (B i).`2. -have hsol: forall i, 0 <= i < k => M i * N i + m i * n i = oner. -- move=> i rgi @/M @/n @/B; have := choicebP (P i) witness _; last done. - have := Bezout (N i) (n i) oner _; first by apply/coprime_isgcdP/copN. - by case=> Mi mi ?; exists (Mi, mi). -pose x := BR.BAdd.bigi predT (fun i => a i * M i * N i) 0 k. -exists x; apply/(@all_nthP _ _ witness) => i rgi /=. -rewrite -/(n i) -/(a i) /x /BR.BAdd.big (@BR.BAdd.bigD1 _ _ i) /=. -- by rewrite mem_range. - by apply: range_uniq. -rewrite addrAC &(@idealD (idgen [n i])); 1: solve; last first. (* FIXME *) -- apply/mem_idgen1_dvd/dvdr_sum=> j /mem_range rgj @/predC1 ne_ji /=. - by rewrite &(dvdr_mull) &(dvdr_prod i) ?mem_range. -have := hsol i rgi; move/(congr1 (( * ) (a i))) => /=. -rewrite mulrDr !mulrA eq_sym -subr_eq => <-. -by rewrite addrAC subrr /= mem_idgen1_dvd dvdrN dvdr_mull. +move=> hcop; apply: crt_comax => i j rgi rgj ne_ij. +by apply/coprime_comax/hcop. qed. (* -------------------------------------------------------------------- *) @@ -986,13 +1129,8 @@ lemma crt_uniq (rs : (t * t) list) (x1 x2 : t) : => all (fun (an : _ * _) => idgen [an.`2] (x2 - an.`1)) rs => idgen [BR.BMul.big predT (fun an : _ * _ => an.`2) rs] (x2 - x1). proof. -move=> hcop sol1 sol2; rewrite mem_idgen1_dvd &(dvdr_prodl_coprime) //. -rewrite all_map /preim; apply/allP=> y y_rs /=. -have ->: x2 - x1 = x2 - y.`1 - (x1 - y.`1) by ring. -by apply/dvdrB; [ - move/allP/(_ _ y_rs): sol2 => /= - | move/allP/(_ _ y_rs): sol1 => /= - ]; move/mem_idgen1_dvd. +move=> hcop sol1 sol2; apply: crt_uniq_comax => //. +move=> i j rgi rgj ne_ij; by apply/coprime_comax/hcop. qed. (* -------------------------------------------------------------------- *) From 2d510c35033a813b2a58da44b5d7880af051ae57 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 17:07:20 +0200 Subject: [PATCH 03/21] CommAlgebra: stack as Base / Euclidean; guard dvdw Base is the ideal-theoretic core over an abstract integral domain: divisibility kit and the witness-level (comax) CRT cluster, with no axiom beyond the ring structure. Euclidean includes Base and adds the weight function with its axioms, gcds, Bezout, coprimality, factorization, and the coprime-phrased CRT corollaries. Instances can thus enter at Base -- e.g. polynomial rings before any division theory is available -- by exhibiting Bezout witnesses directly. The parameterization follows the Poly.ec pattern (top-level type t, named parameter theory ID) rather than an anonymous IDomain clone: overriding an anonymous parameter subtheory referenced by the nested Ideal/BigComRing clones crashes the cloning machinery (ecThCloning.ml:472 assertion). dvdw was inconsistent as stated (y = zeror + dvdr0 + ge0_w + eq0_wP collapse the ring); it now requires both arguments nonzero. --- theories/algebra/CommAlgebra.ec | 37 ++++++++++++++++++++++++++++----- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec index 5e8026f11..c822ce38d 100644 --- a/theories/algebra/CommAlgebra.ec +++ b/theories/algebra/CommAlgebra.ec @@ -5,20 +5,30 @@ require (*--*) Ideal. pragma +implicits. +(* ==================================================================== *) +(* Ideal-theoretic core over an integral domain: divisibility, and the *) +(* CRT cluster against explicit Bezout witnesses (comax). No division *) +(* structure is assumed: instances enter here by supplying the ring *) +(* alone, and discharge comax hypotheses by exhibiting the witnesses. *) +(* ==================================================================== *) +abstract theory Base. + (* -------------------------------------------------------------------- *) -clone import IDomain. +type t. + +clone import IDomain as ID with type t <= t. (* -------------------------------------------------------------------- *) clone Ideal.Ideal as I with - type t <- IDomain.t, - theory IDomain <= IDomain. + type t <- t, + theory IDomain <= ID. (* -------------------------------------------------------------------- *) abbrev (+) = I.idD. (* -------------------------------------------------------------------- *) clone BigComRing as BR - with theory CR <= IDomain, + with theory CR <= ID, op BAdd.big ['a] <= I.BigDom.BAdd.big<:'a>, op BMul.big ['a] <= I.BigDom.BMul.big<:'a>. @@ -284,12 +294,27 @@ by apply/dvdrB; [ ]; move/mem_idgen1_dvd. qed. +end Base. + +(* ==================================================================== *) +(* Euclidean structure: a weight function with division. Provides gcds *) +(* (hence Bezout witnesses: coprime => comax), principality, and the *) +(* coprime-phrased CRT as corollaries of the witness-level cluster. *) +(* ==================================================================== *) +abstract theory Euclidean. + +(* -------------------------------------------------------------------- *) +clone include Base. + +import ID I. + (* -------------------------------------------------------------------- *) op w : t -> int. axiom ge0_w : forall x, 0 <= w x. axiom eq0_wP : forall x, w x = 0 <=> x = zeror. -axiom dvdw : forall (x y : t), x %| y => w x <= w y. +axiom dvdw : forall (x y : t), + x <> zeror => y <> zeror => x %| y => w x <= w y. axiom Euclide : forall x y, y <> zeror => @@ -1224,3 +1249,5 @@ case=> [ys] [irr_ys ysE] [zs] [irr_zs zsE]. exists (zs ++ ys); rewrite all_cat !(irr_ys, irr_zs) /=. by apply: isdecomp_cat. qed. + +end Euclidean. From d1603dc3bd616fdb8e4ed6c22c00df79cc54ad79 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 20:48:06 +0200 Subject: [PATCH 04/21] Poly: evaluation lemma library; tighten the peval definition peval was defined and never developed (its only stdlib occurrences were the definition and the root abbrev). Add the morphism kit at the PolyComRing level -- pevalE_ge (range-flexible form), pevalC, peval0, pevalD, pevalN, pevalB, pevalMX, pevalX, pevalZ, pevalM, peval_big -- together with the polyL structure lemmas polyL_nil and polyL_cons that the list inductions rely on. The definition now sums over 0 <= i < deg p: under the deg convention the previous bound deg p + 1 included a guaranteed-zero last term. --- theories/algebra/Poly.ec | 111 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 110 insertions(+), 1 deletion(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 750e62e7a..2827611c2 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -724,7 +724,7 @@ import BigPoly. (* -------------------------------------------------------------------- *) op peval (p : poly) (a : coeff) = - BCA.bigi predT (fun i => p.[i] * exp a i) 0 (deg p + 1). + BCA.bigi predT (fun i => p.[i] * exp a i) 0 (deg p). (* -------------------------------------------------------------------- *) abbrev root p a = peval p a = Coeff.zeror. @@ -778,6 +778,115 @@ apply/poly_eqP=> c ge0_c; rewrite polyLE; case: (c < n). by rewrite nth_out // size_map size_range /#. qed. +(* -------------------------------------------------------------------- *) +lemma polyL_nil : polyL [<:coeff>] = poly0. +proof. by apply poly_eqP => i ge0; rewrite polyLE poly0E. qed. + +lemma polyL_cons (c : coeff) (xs : coeff list) : + polyL (c :: xs) = polyC c + polyL xs * X. +proof. +apply poly_eqP => i ge0. +rewrite polyLE polyDE polyCE polyMXE polyLE. +case: (i = 0) => [->|nz] /=. +- by rewrite nth_neg // Coeff.addr0. +by rewrite Coeff.add0r /= ifF //. +qed. + +(* -------------------------------------------------------------------- *) +lemma pevalE_ge (p : poly) (a : coeff) (n : int) : deg p <= n => + peval p a = BCA.bigi predT (fun i => p.[i] * Coeff.exp a i) 0 n. +proof. +move=> @/peval /lez_eqVlt [<<-//|hlt]. +rewrite (BCA.big_cat_int (deg p) 0 n) ~-1:#smt:(ge0_deg). +rewrite [BCA.bigi _ _ _ n](_ : _ = zeror) ?addr0 //. +rewrite BCA.big1_seq //= => i /mem_range ?. +by rewrite gedeg_coeff 1:/# mul0r. +qed. + +lemma pevalC (c : coeff) (a : coeff) : peval (polyC c) a = c. +proof. +rewrite (pevalE_ge (polyC c) a 1) 1:degC_le BCA.big_int1 /=. +by rewrite polyCE /= expr0 mulr1. +qed. + +lemma peval0 (a : coeff) : peval poly0 a = zeror. +proof. by rewrite pevalC. qed. + +lemma pevalD (p q : poly) (a : coeff) : + peval (p + q) a = peval p a + peval q a. +proof. +pose n := max (deg p) (deg q). +rewrite (pevalE_ge (p + q) a n) 1:#smt:(degD). +rewrite (pevalE_ge p a n) 1:/# (pevalE_ge q a n) 1:/#. +rewrite -BCA.big_split /= &(BCA.eq_big_int) /=. +by move=> i rgi /=; rewrite polyDE Coeff.mulrDl. +qed. + +lemma pevalN (p : poly) (a : coeff) : peval (- p) a = - peval p a. +proof. +have hd : deg (- p) <= deg p by rewrite degN. +rewrite (pevalE_ge (- p) a (deg p)) 1:hd. +rewrite (pevalE_ge p a (deg p)) 1://. +rewrite BCA.sumrN /= &(BCA.eq_big_int). +by move=> i rgi /=; rewrite polyNE Coeff.mulNr. +qed. + +lemma pevalB (p q : poly) (a : coeff) : + peval (p - q) a = peval p a - peval q a. +proof. by rewrite pevalD pevalN. qed. + +lemma pevalMX (p : poly) (a : coeff) : peval (p * X) a = peval p a * a. +proof. +have hd : deg (p * X) <= deg p + 1. +- case: (p = poly0) => [->>|nz]. + - by rewrite mul0r // #smt:(ge0_deg). + have := degM_le p X nz nz_polyX. + by rewrite degX /#. +rewrite (pevalE_ge (p * X) a (deg p + 1)) 1:hd. +rewrite (pevalE_ge p a (deg p)) 1://. +rewrite BCA.big_int_recl 1:#smt:(ge0_deg) /=. +rewrite polyMXE lt0_coeff 1:// Coeff.mul0r Coeff.add0r. +rewrite BCA.mulr_suml &(BCA.eq_big_int) /=. +by move=> i [??] /=; rewrite polyMXE exprSr //= #ring. +qed. + +lemma pevalX (a : coeff) : peval X a = a. +proof. by rewrite -[X]mul1r pevalMX pevalC mul1r. qed. + +lemma pevalZ (c : coeff) (p : poly) (a : coeff) : + peval (c ** p) a = c * peval p a. +proof. +have hd : deg (c ** p) <= deg p by apply degZ_le. +rewrite (pevalE_ge (c ** p) a (deg p)) 1:hd. +rewrite (pevalE_ge p a (deg p)) 1://. +rewrite BCA.mulr_sumr &(BCA.eq_big_int) /=. +by move=> i rgi; rewrite polyZE mulrA. +qed. + +lemma pevalM (p q : poly) (a : coeff) : + peval (p * q) a = peval p a * peval q a. +proof. +have main : forall (xs : coeff list) (r : poly), + peval (polyL xs * r) a = peval (polyL xs) a * peval r a. +- elim=> [|c xs ih] r. + - by rewrite polyL_nil mul0r peval0 Coeff.mul0r. + rewrite polyL_cons mulrDl pevalD -scalepE pevalZ. + rewrite [polyL xs * _ * _]mulrAC pevalMX ih. + by rewrite pevalD pevalC pevalMX #ring. +have [xs [_ ->]] := surj_polyL p (deg p) _; 1: by done. +by apply main. +qed. + +lemma peval_big ['a] (P : 'a -> bool) (F : 'a -> poly) (s : 'a list) (a : coeff) : + peval (BigPoly.PCA.big P F s) a + = BCA.big P (fun x => peval (F x) a) s. +proof. +elim: s => [|x s ih]. +- by rewrite PCA.big_nil BCA.big_nil peval0. +rewrite BigPoly.PCA.big_cons BCA.big_cons. +by case: (P x) => hP; rewrite ?pevalD ih. +qed. + (* -------------------------------------------------------------------- *) lemma finite_for_poly_ledeg n p s : is_finite_for p s From 169664380403d56b68e791ceed299449d28b8f54 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 20:48:21 +0200 Subject: [PATCH 05/21] Poly, ZModP: keep instance members as aliases; export IDPoly IDPoly and ZModpField were cloned with <- bindings, inlining the type and operators: the resulting theories lack their own t/zeror/... and cannot be passed where an IDomain-shaped theory parameter is expected (structural matching fails with unknown symbols). Switch to <=, which keeps the members as aliases, as ZModpRing and the PolyComRing inner instance already do; and clone-export IDPoly so that instances of the IDomain-level Poly theory expose its names unqualified, mirroring the ComRing instance. --- theories/algebra/Poly.ec | 20 ++++++++++---------- theories/algebra/ZModP.ec | 16 ++++++++-------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 2827611c2..d018c599d 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -988,16 +988,16 @@ op polyV (p : poly) = if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p. (* -------------------------------------------------------------------- *) -clone import Ring.IDomain as IDPoly with - type t <- poly , - op zeror <- poly0, - op oner <- poly1, - op ( + ) <- polyD, - op [ - ] <- polyN, - op ( * ) <- polyM, - op invr <- polyV, - op exp <- PolyComRing.exp, - pred unit <- unitp +clone export Ring.IDomain as IDPoly with + type t <= poly , + op zeror <= poly0, + op oner <= poly1, + op ( + ) <= polyD, + op [ - ] <= polyN, + op ( * ) <= polyM, + op invr <= polyV, + op exp <= PolyComRing.exp, + pred unit <= unitp proof * diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index df0e3127f..2d7e57ff8 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -303,14 +303,14 @@ by move: nz_x; rewrite -asint_eq zeroE pmod_small // rg_asint. qed. clone import Ring.Field as ZModpField with - type t <- zmod, - op zeror <- zero, - op oner <- one, - op ( + ) <- ( + ), - op [ - ] <- ([-]), - op ( * ) <- ( * ), - op invr <- inv, - op exp <- ZModpRing.exp + type t <= zmod, + op zeror <= zero, + op oner <= one, + op ( + ) <= ( + ), + op [ - ] <= ([-]), + op ( * ) <= ( * ), + op invr <= inv, + op exp <= ZModpRing.exp proof * remove abbrev (-) remove abbrev (/). From fdd2dcb8540ec6fae1c1ba6804e0de583abb4e7c Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 23:25:39 +0200 Subject: [PATCH 06/21] Poly: evaluation of polynomial products peval_prod, the multiplicative companion of peval_big: evaluating a PCM product of polynomials is the BCM product of the evaluations. --- theories/algebra/Poly.ec | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index d018c599d..2846349ce 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -887,6 +887,16 @@ rewrite BigPoly.PCA.big_cons BCA.big_cons. by case: (P x) => hP; rewrite ?pevalD ih. qed. +lemma peval_prod ['a] (P : 'a -> bool) (F : 'a -> poly) (s : 'a list) (a : coeff) : + peval (BigPoly.PCM.big P F s) a + = BCM.big P (fun x => peval (F x) a) s. +proof. +elim: s => [|x s ih]. +- by rewrite PCM.big_nil BCM.big_nil pevalC. +rewrite BigPoly.PCM.big_cons BCM.big_cons. +by case: (P x) => hP; rewrite ?pevalM ih. +qed. + (* -------------------------------------------------------------------- *) lemma finite_for_poly_ledeg n p s : is_finite_for p s From bfd7ee8202c964e349e3c5bfe1bdb07a999c7498 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 23:26:35 +0200 Subject: [PATCH 07/21] Poly: rename peval_big to peval_sum Aligns with peval_prod: peval_sum/peval_prod for PCA/PCM bigs. --- theories/algebra/Poly.ec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 2846349ce..06016ea2c 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -877,7 +877,7 @@ have [xs [_ ->]] := surj_polyL p (deg p) _; 1: by done. by apply main. qed. -lemma peval_big ['a] (P : 'a -> bool) (F : 'a -> poly) (s : 'a list) (a : coeff) : +lemma peval_sum ['a] (P : 'a -> bool) (F : 'a -> poly) (s : 'a list) (a : coeff) : peval (BigPoly.PCA.big P F s) a = BCA.big P (fun x => peval (F x) a) s. proof. From f3fbf4ea1dcfd09ab09eed5dd256529709be62f5 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 23:49:11 +0200 Subject: [PATCH 08/21] Poly: products of monic linear factors mprod rs = prod_(r in rs) (X - C r) as a PCM big, with the unfolding lemmas, factorization at a member root (mprod_mem_factor, by perm_to_rem), vanishing at member roots (mprod_root), and the degree computation deg_mprod = 1 + size rs -- the degM_proper side condition is discharged by monicity (lc_XC), no domain assumption on the coefficients. --- theories/algebra/Poly.ec | 57 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 06016ea2c..cb1b73279 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -897,6 +897,63 @@ rewrite BigPoly.PCM.big_cons BCM.big_cons. by case: (P x) => hP; rewrite ?pevalM ih. qed. +(* -------------------------------------------------------------------- *) +(* Products of monic linear factors *) +op mprod (rs : coeff list) : poly = + PCM.big predT (fun r => X - polyC r) rs. + +lemma mprod_nil : mprod [] = poly1. +proof. by rewrite /mprod PCM.big_nil. qed. + +lemma mprod_cons (r : coeff) (rs : coeff list) : + mprod (r :: rs) = (X - polyC r) * mprod rs. +proof. by rewrite /mprod PCM.big_consT. qed. + +lemma mprod_cat (rs1 rs2 : coeff list) : + mprod (rs1 ++ rs2) = mprod rs1 * mprod rs2. +proof. by rewrite /mprod PCM.big_cat. qed. + +lemma mprod_mem_factor (rs : coeff list) (r : coeff) : + r \in rs => exists q, mprod rs = (X - polyC r) * q. +proof. +move=> hmem; exists (mprod (rem r rs)). +rewrite /mprod (PCM.eq_big_perm _ _ _ _ (perm_to_rem _ _ hmem)). +by rewrite PCM.big_consT. +qed. + +lemma mprod_root (rs : coeff list) (a : coeff) : + a \in rs => root (mprod rs) a. +proof. +move=> hin; have [q ->] := mprod_mem_factor rs a hin. +by rewrite pevalM pevalB pevalX pevalC Coeff.subrr Coeff.mul0r. +qed. + +lemma lc_XC (r : coeff) : lc (X - polyC r) = oner. +proof. +rewrite (_ : X - polyC r = X + (- polyC r)) 1:// lcDl. +- by rewrite degN; smt(degC_le degX). +by rewrite lcX. +qed. + +lemma deg_XC (r : coeff) : deg (X - polyC r) = 2. +proof. +rewrite (_ : X - polyC r = X + (- polyC r)) 1:// degDl. +- by rewrite degN; smt(degC_le degX). +by rewrite degX. +qed. + +lemma deg_mprod (rs : coeff list) : deg (mprod rs) = 1 + size rs. +proof. +elim: rs => [|r rs ih]. +- by rewrite mprod_nil deg1. +rewrite mprod_cons degM_proper. +- rewrite lc_XC Coeff.mul1r. + apply /negP => h0. + have : mprod rs = poly0 by rewrite -lc_eq0 h0. + by rewrite -deg_eq0 ih; smt(size_ge0). +by rewrite deg_XC ih /= /#. +qed. + (* -------------------------------------------------------------------- *) lemma finite_for_poly_ledeg n p s : is_finite_for p s From d263dec143ebfbf7d023cd79fb36865388db209b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 17 Jul 2026 23:53:08 +0200 Subject: [PATCH 09/21] Poly: mprod does not vanish outside its roots peval_mprod_out, in the IDomain-level theory: evaluating a product of monic linear factors outside the root list is nonzero (coefficient mulf_eq0). --- theories/algebra/Poly.ec | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index cb1b73279..f1c17225c 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -1147,4 +1147,17 @@ proof. rewrite /polyV; case: (deg p = 1); last done. by case/deg_eq1=> c [nz_c ->>]; rewrite !degC polyCE /= invr_eq0. qed. + +(* -------------------------------------------------------------------- *) +lemma peval_mprod_out (rs : coeff list) (a : coeff) : + ! (a \in rs) => peval (mprod rs) a <> IDCoeff.zeror. +proof. +elim: rs => [|r rs ih] hnin. +- rewrite mprod_nil pevalC. + by apply IDCoeff.oner_neq0. +rewrite mprod_cons pevalM pevalB pevalX pevalC. +apply/negP => /IDCoeff.mulf_eq0 [h0|h0]. +- by move: h0; rewrite IDCoeff.subr_eq0; smt(). +by move: h0; smt(). +qed. end Poly. From 3c6febead474f6ca30792cf3b4de2280f19bbb17 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 00:06:05 +0200 Subject: [PATCH 10/21] Poly: simplify the monic-linear-factor lemmas degBl/lcBl (degree and leading coefficient through subtraction of a lower-degree polynomial); degXBC/lcXBC replace deg_XC/lc_XC, stated with the early deg/lc lemmas and proved without smt; deg_mprod and peval_mprod_out streamlined accordingly (mulf_neq0). --- theories/algebra/Poly.ec | 57 ++++++++++++++++++++-------------------- 1 file changed, 29 insertions(+), 28 deletions(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index f1c17225c..431527e02 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -402,18 +402,37 @@ apply: degP=> //. by apply/ltrW/(ltr_le_trans _ _ _ le_pq). qed. +lemma degDr p q : deg p < deg q => deg (p + q) = deg q. +proof. by move/degDl; rewrite addrC. qed. + +lemma degBl p q : deg q < deg p => deg (p - q) = deg p. +proof. by move=> ?; rewrite degDl ?degN. qed. + lemma lcDl p q : deg q < deg p => lc (p + q) = lc p. proof. move=> ^lt_pq /degDl ->; rewrite polyDE. by rewrite addrC gedeg_coeff ?add0r //#. qed. -lemma degDr p q : deg p < deg q => deg (p + q) = deg q. -proof. by move/degDl; rewrite addrC. qed. +lemma lcBl p q : deg q < deg p => lc (p - q) = lc p. +proof. by move=> ?; rewrite lcDl ?degN. qed. lemma lcDr p q : deg q < deg p => lc (p + q) = lc p. proof. by move/lcDl; rewrite addrC. qed. +(* -------------------------------------------------------------------- *) +lemma degXBC (r : coeff) : deg (X - polyC r) = 2. +proof. +rewrite degDl ?degN. +- by rewrite degX &(ler_lt_trans _ _ _ (degC_le _)). +- by rewrite degX. +qed. + +lemma lcXBC (r : coeff) : lc (X - polyC r) = oner. +proof. +by rewrite lcBl ?lcX // degX &(ler_lt_trans _ _ _ (degC_le _)). +qed. + (* -------------------------------------------------------------------- *) lemma polyMEw M p q k : (k <= M)%Int => (p * q).[k] = BCA.bigi predT (fun i => p.[i] * q.[k-i]) 0 (M+1). @@ -928,30 +947,14 @@ move=> hin; have [q ->] := mprod_mem_factor rs a hin. by rewrite pevalM pevalB pevalX pevalC Coeff.subrr Coeff.mul0r. qed. -lemma lc_XC (r : coeff) : lc (X - polyC r) = oner. -proof. -rewrite (_ : X - polyC r = X + (- polyC r)) 1:// lcDl. -- by rewrite degN; smt(degC_le degX). -by rewrite lcX. -qed. - -lemma deg_XC (r : coeff) : deg (X - polyC r) = 2. -proof. -rewrite (_ : X - polyC r = X + (- polyC r)) 1:// degDl. -- by rewrite degN; smt(degC_le degX). -by rewrite degX. -qed. - lemma deg_mprod (rs : coeff list) : deg (mprod rs) = 1 + size rs. proof. -elim: rs => [|r rs ih]. -- by rewrite mprod_nil deg1. +elim: rs => [|r rs ih]; first by rewrite mprod_nil deg1. rewrite mprod_cons degM_proper. -- rewrite lc_XC Coeff.mul1r. - apply /negP => h0. - have : mprod rs = poly0 by rewrite -lc_eq0 h0. +- rewrite lcXBC mul1r; apply/negP=> h. + have: mprod rs = poly0 by rewrite -lc_eq0 h. by rewrite -deg_eq0 ih; smt(size_ge0). -by rewrite deg_XC ih /= /#. +by rewrite degXBC ih. qed. (* -------------------------------------------------------------------- *) @@ -1152,12 +1155,10 @@ qed. lemma peval_mprod_out (rs : coeff list) (a : coeff) : ! (a \in rs) => peval (mprod rs) a <> IDCoeff.zeror. proof. -elim: rs => [|r rs ih] hnin. -- rewrite mprod_nil pevalC. - by apply IDCoeff.oner_neq0. +elim: rs => [|r rs ih] /=. +- by rewrite mprod_nil pevalC &(IDCoeff.oner_neq0). +move/negb_or => [nz_ar a_notin_rs]. rewrite mprod_cons pevalM pevalB pevalX pevalC. -apply/negP => /IDCoeff.mulf_eq0 [h0|h0]. -- by move: h0; rewrite IDCoeff.subr_eq0; smt(). -by move: h0; smt(). +by rewrite &(IDCoeff.mulf_neq0) -1:ih // subr_eq0. qed. end Poly. From 9b347d003a3a162cdc1235e3b3418460531238cf Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 00:14:06 +0200 Subject: [PATCH 11/21] Poly: PolyField, polynomials over a field; Lagrange interpolation A third floor over PolyComRing / Poly, with Field coefficients. First content: Lagrange interpolation over a uniq root list -- the basis lag (scaled monic products), its evaluation lemmas, interp as a PCA sum realizing any assignment of values at the roots, with degree at most the number of roots. --- theories/algebra/Poly.ec | 83 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 431527e02..185ebdd3f 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -1162,3 +1162,86 @@ rewrite mprod_cons pevalM pevalB pevalX pevalC. by rewrite &(IDCoeff.mulf_neq0) -1:ih // subr_eq0. qed. end Poly. + +(* ==================================================================== *) +abstract theory PolyField. +type coeff. + +clone import Field as FCoeff with type t <= coeff. + +clone include Poly with + type coeff <- coeff, + theory IDCoeff <- FCoeff. + +(* -------------------------------------------------------------------- *) +(* Lagrange interpolation over a uniq root list: any assignment of *) +(* values at the roots is realized by a polynomial of degree at most *) +(* the number of roots *) +op lag (rs : coeff list) (r : coeff) : poly = + polyC (FCoeff.invr (peval (mprod (rem r rs)) r)) * mprod (rem r rs). + +lemma lag_eval_same (rs : coeff list) (r : coeff) : + uniq rs => r \in rs => peval (lag rs r) r = FCoeff.oner. +proof. +move=> hu hmem. +rewrite /lag pevalM pevalC. +apply FCoeff.mulVf. +apply peval_mprod_out. +rewrite (rem_filter r rs hu) mem_filter /predC1. +by smt(). +qed. + +lemma lag_eval_other (rs : coeff list) (r r' : coeff) : + uniq rs => r' \in rs => r' <> r => peval (lag rs r) r' = FCoeff.zeror. +proof. +move=> hu hm hne. +rewrite /lag pevalM. +rewrite (mprod_root (rem r rs) r'). +- rewrite (rem_filter r rs hu) mem_filter /predC1. + by smt(). +by rewrite FCoeff.mulr0. +qed. + +lemma deg_lag (rs : coeff list) (r : coeff) : + uniq rs => r \in rs => deg (lag rs r) <= size rs. +proof. +move=> hu hm. +rewrite /lag -scalepE. +have := degZ_le (FCoeff.invr (peval (mprod (rem r rs)) r)) (mprod (rem r rs)). +rewrite deg_mprod size_rem 1://. +by smt(). +qed. + +(* -------------------------------------------------------------------- *) +op interp (rs : coeff list) (f : coeff -> coeff) : poly = + BigPoly.PCA.big predT (fun r => polyC (f r) * lag rs r) rs. + +lemma interp_evalP (rs : coeff list) (f : coeff -> coeff) (r0 : coeff) : + uniq rs => r0 \in rs => peval (interp rs f) r0 = f r0. +proof. +move=> hu hm. +rewrite /interp peval_sum. +rewrite (BigCf.BCA.eq_big_perm _ _ _ _ (perm_to_rem _ _ hm)). +rewrite BigCf.BCA.big_cons /predT /=. +rewrite pevalM pevalC lag_eval_same 1,2:// FCoeff.mulr1. +rewrite BigCf.BCA.big1_seq /=. +- move=> r hr. + have := hr; rewrite (rem_filter r0 rs hu) mem_filter /predC1 => -[hne hmem2]. + rewrite /root pevalM pevalC (lag_eval_other rs r r0) 1:// 1:// 1:/#. + by rewrite FCoeff.mulr0. +by rewrite FCoeff.addr0. +qed. + +lemma deg_interp (rs : coeff list) (f : coeff -> coeff) : + uniq rs => deg (interp rs f) <= size rs. +proof. +move=> hu. +rewrite /interp BigPoly.PCA.big_seq. +apply BigPoly.deg_sum; 1: smt(size_ge0). +move=> r /= hr. +rewrite -scalepE. +have h1 := degZ_le (f r) (lag rs r). +have h2 := deg_lag rs r hu hr. +by smt(). +qed. +end PolyField. From b55d7a624929628ac7a823f1c5b69af93df2cf55 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 00:33:32 +0200 Subject: [PATCH 12/21] Poly: package Lagrange interpolation in a sub-theory; tidy proofs PolyField.Lagrange holds lag/interp and their lemmas; PolyField imports BigCf/BigPoly so the proofs drop the qualified coefficient and bigop names, and the scripts are shortened (&-combinators, ler_trans chains instead of smt). --- theories/algebra/Poly.ec | 122 ++++++++++++++++++--------------------- 1 file changed, 55 insertions(+), 67 deletions(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 185ebdd3f..afe9c83c9 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -1173,75 +1173,63 @@ clone include Poly with type coeff <- coeff, theory IDCoeff <- FCoeff. +import BigCf BigPoly. + (* -------------------------------------------------------------------- *) (* Lagrange interpolation over a uniq root list: any assignment of *) (* values at the roots is realized by a polynomial of degree at most *) (* the number of roots *) -op lag (rs : coeff list) (r : coeff) : poly = - polyC (FCoeff.invr (peval (mprod (rem r rs)) r)) * mprod (rem r rs). - -lemma lag_eval_same (rs : coeff list) (r : coeff) : - uniq rs => r \in rs => peval (lag rs r) r = FCoeff.oner. -proof. -move=> hu hmem. -rewrite /lag pevalM pevalC. -apply FCoeff.mulVf. -apply peval_mprod_out. -rewrite (rem_filter r rs hu) mem_filter /predC1. -by smt(). -qed. - -lemma lag_eval_other (rs : coeff list) (r r' : coeff) : - uniq rs => r' \in rs => r' <> r => peval (lag rs r) r' = FCoeff.zeror. -proof. -move=> hu hm hne. -rewrite /lag pevalM. -rewrite (mprod_root (rem r rs) r'). -- rewrite (rem_filter r rs hu) mem_filter /predC1. - by smt(). -by rewrite FCoeff.mulr0. -qed. - -lemma deg_lag (rs : coeff list) (r : coeff) : - uniq rs => r \in rs => deg (lag rs r) <= size rs. -proof. -move=> hu hm. -rewrite /lag -scalepE. -have := degZ_le (FCoeff.invr (peval (mprod (rem r rs)) r)) (mprod (rem r rs)). -rewrite deg_mprod size_rem 1://. -by smt(). -qed. - -(* -------------------------------------------------------------------- *) -op interp (rs : coeff list) (f : coeff -> coeff) : poly = - BigPoly.PCA.big predT (fun r => polyC (f r) * lag rs r) rs. - -lemma interp_evalP (rs : coeff list) (f : coeff -> coeff) (r0 : coeff) : - uniq rs => r0 \in rs => peval (interp rs f) r0 = f r0. -proof. -move=> hu hm. -rewrite /interp peval_sum. -rewrite (BigCf.BCA.eq_big_perm _ _ _ _ (perm_to_rem _ _ hm)). -rewrite BigCf.BCA.big_cons /predT /=. -rewrite pevalM pevalC lag_eval_same 1,2:// FCoeff.mulr1. -rewrite BigCf.BCA.big1_seq /=. -- move=> r hr. - have := hr; rewrite (rem_filter r0 rs hu) mem_filter /predC1 => -[hne hmem2]. - rewrite /root pevalM pevalC (lag_eval_other rs r r0) 1:// 1:// 1:/#. - by rewrite FCoeff.mulr0. -by rewrite FCoeff.addr0. -qed. - -lemma deg_interp (rs : coeff list) (f : coeff -> coeff) : - uniq rs => deg (interp rs f) <= size rs. -proof. -move=> hu. -rewrite /interp BigPoly.PCA.big_seq. -apply BigPoly.deg_sum; 1: smt(size_ge0). -move=> r /= hr. -rewrite -scalepE. -have h1 := degZ_le (f r) (lag rs r). -have h2 := deg_lag rs r hu hr. -by smt(). -qed. +theory Lagrange. + op lag (rs : coeff list) (r : coeff) : poly = + polyC (invr (peval (mprod (rem r rs)) r)) * mprod (rem r rs). + + lemma lag_eval_same (rs : coeff list) (r : coeff) : + uniq rs => r \in rs => peval (lag rs r) r = FCoeff.oner. + proof. + move=> hu hmem @/lag; rewrite pevalM pevalC. + rewrite &(mulVf) &(peval_mprod_out). + by rewrite rem_filter // mem_filter. + qed. + + lemma lag_eval_other (rs : coeff list) (r r' : coeff) : + uniq rs => r' \in rs => r' <> r + => peval (lag rs r) r' = FCoeff.zeror. + proof. + move=> hu hm hne @/lag; rewrite pevalM. + rewrite (mprod_root (rem r rs) r'). + - by rewrite rem_filter // mem_filter. + - by rewrite mulr0. + qed. + + lemma deg_lag (rs : coeff list) (r : coeff) : + uniq rs => r \in rs => deg (lag rs r) <= size rs. + proof. + move=> hu hm @/lag; rewrite -scalepE. + apply/(ler_trans _ _ _ (degZ_le _ _)). + by rewrite deg_mprod size_rem. + qed. + + (* -------------------------------------------------------------------- *) + op interp (rs : coeff list) (f : coeff -> coeff) : poly = + BigPoly.PCA.big predT (fun r => polyC (f r) * lag rs r) rs. + + lemma interp_evalP (rs : coeff list) (f : coeff -> coeff) (r0 : coeff) : + uniq rs => r0 \in rs => peval (interp rs f) r0 = f r0. + proof. + move=> hu hm @/interp; rewrite peval_sum. + rewrite (BCA.eq_big_perm _ _ _ _ (perm_to_rem _ _ hm)). + rewrite BCA.big_consT /= pevalM pevalC. + rewrite lag_eval_same ~-1:// mulr1 BCA.big1_seq /= ?addr0 //. + move=> r; rewrite rem_filter // mem_filter // => -[hne hmem2]. + by rewrite pevalM pevalC (lag_eval_other rs r r0) ~-1://# mulr0. + qed. + + lemma deg_interp (rs : coeff list) (f : coeff -> coeff) : + uniq rs => deg (interp rs f) <= size rs. + proof. + move=> hu @/interp; rewrite PCA.big_seq &(deg_sum) //=. + move=> r hr; rewrite -scalepE. + by apply/(ler_trans _ _ _ (degZ_le _ _))/deg_lag. + qed. +end Lagrange. end PolyField. From 4d3f5882ddeeb5d1e78c57dd4b6028905e51b856 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 01:10:28 +0200 Subject: [PATCH 13/21] CommAlgebra: Base owns its big operators and pushes them into Ideal BR is declared before the Ideal clone and substituted for its BigDom with <-, so the nested copy vanishes and instances only ever substitute top-level theories (ID, BR). This replaces the previous op-level aliasing of BR onto I.BigDom, and retires the FIXME unfoldings that aliasing required in the proofs. --- theories/algebra/CommAlgebra.ec | 55 +++++++++++++++++---------------- 1 file changed, 28 insertions(+), 27 deletions(-) diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec index c822ce38d..b8b73bf0a 100644 --- a/theories/algebra/CommAlgebra.ec +++ b/theories/algebra/CommAlgebra.ec @@ -19,18 +19,19 @@ type t. clone import IDomain as ID with type t <= t. (* -------------------------------------------------------------------- *) -clone Ideal.Ideal as I with - type t <- t, - theory IDomain <= ID. +(* The big operators are owned here and pushed down into the Ideal *) +(* clone, so that instances only ever substitute top-level theories. *) +clone BigComRing as BR with + theory CR <= ID. (* -------------------------------------------------------------------- *) -abbrev (+) = I.idD. +clone Ideal.Ideal as I with + type t <- t, + theory IDomain <- ID, + theory BigDom <- BR. (* -------------------------------------------------------------------- *) -clone BigComRing as BR - with theory CR <= ID, - op BAdd.big ['a] <= I.BigDom.BAdd.big<:'a>, - op BMul.big ['a] <= I.BigDom.BMul.big<:'a>. +abbrev (+) = I.idD. (* -------------------------------------------------------------------- *) import I. @@ -130,7 +131,7 @@ lemma dvdr_sum ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) : (forall c, c \in cs => P c => a %| F c) => a %| BR.BAdd.big P F cs. proof. -elim: cs => [|c cs ih] hdvd @/BR.BAdd.big //=. (* FIXME *) +elim: cs => [|c cs ih] hdvd. - by rewrite BR.BAdd.big_nil dvdr0. rewrite BR.BAdd.big_cons; case: (P c) => Pc /=; last first. - by apply/ih=> *; apply/hdvd => //#. @@ -142,7 +143,7 @@ qed. lemma dvdr_prod ['a] (P : 'a -> bool) (F : 'a -> t) (cs : 'a list) (a : t) (x : 'a) : x \in cs => P x => a %| F x => a %| BR.BMul.big P F cs. proof. -move=> x_in_cs Px dvd_a_Fx @/BR.BMul.big. +move=> x_in_cs Px dvd_a_Fx. move/perm_to_rem: x_in_cs => /BR.BMul.eq_big_perm ->. by rewrite BR.BMul.big_cons Px /= dvdr_mulr. qed. @@ -204,7 +205,7 @@ lemma comax_prod ['a] (P : 'a -> bool) (F : 'a -> t) (c : t) (cs : 'a list) : (forall i, i \in cs => P i => comax (F i) c) => comax (BR.BMul.big P F cs) c. proof. -elim: cs => [|x xs ih] hcm @/BR.BMul.big. +elim: cs => [|x xs ih] hcm. - by rewrite BR.BMul.big_nil comax1r. rewrite BR.BMul.big_cons; case: (P x) => Px; last by apply/ih => /#. apply/comaxMl. @@ -230,7 +231,7 @@ lemma dvdr_prodl_comax ['a] (F : 'a -> t) (cs : 'a list) (a : t) : => all (fun b => b %| a) (map F cs) => BR.BMul.big predT F cs %| a. proof. -elim: cs => [|c cs ih] hcm hdvd /= @/BR.BMul.big. +elim: cs => [|c cs ih] hcm hdvd /=. - by rewrite BR.BMul.big_nil dvd1r. rewrite BR.BMul.big_consT dvdrMl_comax. - apply/comaxC/comax_prod => b b_in_cs _. @@ -266,7 +267,7 @@ have hsol: forall i, 0 <= i < k => M i * N i + m i * n i = oner. by case: (cmN i rgi) => Mi mi ?; exists (Mi, mi). pose x := BR.BAdd.bigi predT (fun i => a i * M i * N i) 0 k. exists x; apply/(@all_nthP _ _ witness) => i rgi /=. -rewrite -/(n i) -/(a i) /x /BR.BAdd.big (@BR.BAdd.bigD1 _ _ i) /=. +rewrite -/(n i) -/(a i) /x (@BR.BAdd.bigD1 _ _ i) /=. - by rewrite mem_range. - by apply: range_uniq. rewrite addrAC &(@idealD (idgen [n i])); 1: solve; last first. (* FIXME *) - apply/mem_idgen1_dvd/dvdr_sum=> j /mem_range rgj @/predC1 ne_ji /=. @@ -440,8 +441,8 @@ apply/predeq_leP; split=> z @/idD. by rewrite !nth_cat -!addrA /= eqx ltzNge lez_addr ge0i. - case/idgenP=> cs [sz_cs ->]. pose csx := take (size xs) cs; pose csy := drop (size xs) cs. - pose x := BigDom.BAdd.bigi predT (fun (i : int) => csx.[i] * xs.[i]) 0 (size xs). - pose y := BigDom.BAdd.bigi predT (fun (i : int) => csy.[i] * ys.[i]) 0 (size ys). + pose x := BR.BAdd.bigi predT (fun (i : int) => csx.[i] * xs.[i]) 0 (size xs). + pose y := BR.BAdd.bigi predT (fun (i : int) => csy.[i] * ys.[i]) 0 (size ys). exists x y; rewrite size_cat; split. - by split; [exists csx | exists csy]. rewrite (@BR.BAdd.big_cat_int (size xs)) ~-1:#smt:(size_ge0); congr. @@ -683,13 +684,13 @@ qed. (* -------------------------------------------------------------------- *) lemma isdecomp_nil (x : t) : isdecomp x [] <=> x = oner. -proof. by rewrite /isdecomp /BR.BMul.big BR.BMul.big_nil. qed. (* FIXME *) +proof. by rewrite /isdecomp BR.BMul.big_nil. qed. (* -------------------------------------------------------------------- *) lemma isdecompM (x : t) (y : t) (ys : t list) : isdecomp y ys => isdecomp (x * y) (x :: ys). proof. -by move=> -> @/isdecomp; rewrite /BR.BMul.big BR.BMul.big_consT. (* FIXME *) +by move=> -> @/isdecomp; rewrite BR.BMul.big_consT. qed. (* -------------------------------------------------------------------- *) @@ -697,7 +698,7 @@ lemma isdecomp_cons (x : t) (y : t) (ys : t list) : isdecomp x (y :: ys) => exists z, x = y * z /\ isdecomp z ys. proof. move=> ->; pose z := BR.BMul.big predT idfun ys. -by exists z; rewrite /BR.BMul.big BR.BMul.big_consT. (* FIXME *) +by exists z; rewrite BR.BMul.big_consT. qed. (* -------------------------------------------------------------------- *) @@ -721,7 +722,7 @@ move=> irr_x irr_xs hdecomp; suff: exists x', x' \in xs /\ x %= x'. - case=> x' [x'_in_xs /eqmodfP [u] [unit_u ->>]]. exists (invr u) (rem x' xs); rewrite mulrA mulVr //= invrK. rewrite unitrV unit_u /= perm_to_rem //=. - move: hdecomp => @/isdecomp @/BR.BMul.big. + move: hdecomp => @/isdecomp. rewrite (@BR.BMul.eq_big_perm _ _ _ _ (perm_to_rem x'_in_xs)). (* FIXME *) rewrite BR.BMul.big_consT /= -mulrA mulrCA &(mulfI). by apply: irdc_neq0; apply: irdc_Ml irr_x. @@ -730,8 +731,8 @@ elim: xs x irr_x y irr_xs hdecomp => [|v vs ih] x irr_x y /=. case=> irr_v irr_vs hdecomp ; case: (x %= v)=> [eq_xv|ne_xv]. - by exists v. have cop_xv: coprime x v by apply: irdc_coprime. -move: (hdecomp) => @/isdecomp; rewrite /BR.BMul.big. -rewrite BR.BMul.big_consT /=; pose z := BigDom.BMul.big _ _ _. +move: (hdecomp) => @/isdecomp. +rewrite BR.BMul.big_consT /=; pose z := BR.BMul.big _ _ _. move=> eq; have [dvdx dvdv]: x %| v * z /\ v %| x * y. - split; apply/dvdrP. - by exists y; rewrite [_*x]mulrC &(eq_sym). @@ -943,7 +944,7 @@ lemma decomp_uniq (z1 z2 : t) (xs1 xs2 : t list) : proof. elim: xs1 z1 z2 xs2 => [|x1 xs1 ih] z1 z2 xs2 /=. - move=> irdc_xs2 eq1x dcp2 eqz; have ->>: z1 = oner. - - by rewrite eq1x /(BR.BMul.big) BR.BMul.big_nil. + - by rewrite eq1x BR.BMul.big_nil. suff -> /=: xs2 = [] by exists [] => /=; rewrite mkseq0. case: xs2 irdc_xs2 dcp2 => //= x2 xs2; case=> + _. move/irdc_Nunit; apply: contra => /isdecomp_cons. @@ -961,10 +962,10 @@ wlog: xs2 irdc_xs2 dcp_xs2 eq_xs2 / (xs2 = (u * (invr w * x1)) :: ys). - by do! apply/irdc_Ml => //; apply/unitrV. move=> ?; move/allP: irdc_xs2; apply. by move/perm_eq_mem: eq_xs2 => -> /=; right. - - rewrite /isdecomp /(BR.BMul.big) BR.BMul.big_consT /=. + - rewrite /isdecomp BR.BMul.big_consT /=. apply/(mulrI (w * invr u) _). - by apply/unitrM; split=> //; apply/unitrV. - rewrite -[_ * BigDom.BMul.big _ _ _]mulrA; congr. + rewrite -[_ * BR.BMul.big _ _ _]mulrA; congr. rewrite [u*_]mulrC -!mulrA; do 2! congr. apply/(mulrI (invr u)); first by apply/unitrV. by rewrite mulrA dcp_ys mulrAC mulVr. @@ -1098,7 +1099,7 @@ lemma coprime_prod ['a] (P : 'a -> bool) (F : 'a -> t) (c : t) (cs : 'a list) : (forall i, i \in cs => P i => coprime (F i) c) => coprime (BR.BMul.big P F cs) c. proof. -move=> @/BR.BMul.big; elim: cs => /= [|x xs ih]. (* FIXME *) +elim: cs => /= [|x xs ih]. - by rewrite BR.BMul.big_nil coprime1r. move=> cop; rewrite BR.BMul.big_cons; case: (P x); last smt(). by move=> Px; apply/coprimeMl => /#. @@ -1131,7 +1132,7 @@ lemma dvdr_prodl_coprime ['a] (F : 'a -> t) (cs : 'a list) (a : t) : => all (fun b => b %| a) (map F cs) => BR.BMul.big predT F cs %| a. proof. -elim: cs => [|c cs ih] hcop hdvd /= @/BR.BMul.big. +elim: cs => [|c cs ih] hcop hdvd /=. - by rewrite BR.BMul.big_nil dvd1r. rewrite BR.BMul.big_consT dvdrMl_coprime. - apply/coprimeC/coprime_prod => b b_in_cs _. @@ -1228,7 +1229,7 @@ qed. lemma isdecomp_cat (x y : t) (xs ys : t list) : isdecomp x xs => isdecomp y ys => isdecomp (x * y) (xs ++ ys). proof. -move=> xsE ysE @/isdecomp @/BR.BMul.big. (* FIXME *) +move=> xsE ysE @/isdecomp. by rewrite BR.BMul.big_cat xsE ysE. qed. From bbb6cb12115303cc70bed8c0d0351e27b9ab315d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 02:46:55 +0200 Subject: [PATCH 14/21] Ring, ZModP: delta-only mixins for IDomain and Field (pilot) IDomainMixin and FieldMixin take their parent ComRing as a named parameter (referenced, not copied). IDomainMixin carries mulf_eq0 and the domain lemma library. FieldMixin is a factory: its single axiom is that units are exactly the nonzero elements; mulf_eq0 is derived generically (retiring ZModP's 'FIXME: should be generic') and its nested Dom is a fully realized IDomainMixin over the same parent, so consumers expecting the domain layer accept F.Dom. ZModP pilots the architecture: ZModpFieldMx is a FieldMixin over ZModpRing realized by the single lemma unitE -- versus the bundled ZModpField clone (kept for compatibility during migration), which re-clones Ring.Field and re-realizes nine ComRing axioms by delegation. One ring library on zmod; the field level a pure delta. --- theories/algebra/Ring.ec | 101 ++++++++++++++++++++++++++++++++++++++ theories/algebra/ZModP.ec | 10 ++++ 2 files changed, 111 insertions(+) diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec index 41fd91356..30c5ccff0 100644 --- a/theories/algebra/Ring.ec +++ b/theories/algebra/Ring.ec @@ -858,6 +858,107 @@ abstract theory Field. end Field. +(* -------------------------------------------------------------------- *) +(* Refinements as delta-only mixins: the parent ComRing is a named *) +(* parameter, referenced -- not copied. One library per level. *) +abstract theory IDomainMixin. + type t. + + clone import ComRing as R with type t <= t. + + axiom mulf_eq0: + forall (x y : t), x * y = zeror <=> x = zeror \/ y = zeror. + + lemma mulf_neq0 (x y : t): x <> zeror => y <> zeror => x * y <> zeror. + proof. by move=> nz_x nz_y; apply/negP; rewrite mulf_eq0 /#. qed. + + lemma expf_eq0 x n : (exp x n = zeror) <=> (n <> 0 /\ x = zeror). + proof. + elim/intwlog: n => [n| |n ge0_n ih]. + + by rewrite exprN invr_eq0 /#. + + by rewrite expr0 oner_neq0. + by rewrite exprS // mulf_eq0 ih addz1_neq0 ?andKb. + qed. + + lemma mulfI (x : t): x <> zeror => injective (( * ) x). + proof. + move=> ne0_x y y'; rewrite -(opprK (x * y')) -mulrN -addr_eq0. + by rewrite -mulrDr mulf_eq0 ne0_x /= addr_eq0 opprK. + qed. + + lemma mulIf x: x <> zeror => injective (fun y => y * x). + proof. by move=> nz_x y z; rewrite -!(@mulrC x); exact: mulfI. qed. + + lemma sqrf_eq1 x : (exp x 2 = oner) <=> (x = oner \/ x = -oner). + proof. by rewrite -subr_eq0 subr_sqr_1 mulf_eq0 subr_eq0 addr_eq0. qed. + + lemma lregP x : lreg x <=> x <> zeror. + proof. by split=> [/lreg_neq0//|/mulfI]. qed. + + lemma eqr_div (x1 y1 x2 y2 : t) : unit y1 => unit y2 => + (x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1). + proof. + move=> Nut1 Nut2; rewrite -{1}(@mulrK y2 _ x1) //. + rewrite -{1}(@mulrK y1 _ x2) // -!mulrA (@mulrC (invr y1)) !mulrA. + split=> [|->] //; + (have nz_Vy1: unit (invr y1) by rewrite unitrV); + (have nz_Vy2: unit (invr y2) by rewrite unitrV). + by move/(mulIr _ nz_Vy1)/(mulIr _ nz_Vy2). + qed. +end IDomainMixin. + +(* -------------------------------------------------------------------- *) +abstract theory FieldMixin. + type t. + + clone import ComRing as R with type t <= t. + + axiom unitfP : forall (x : t), unit x <=> x <> zeror. + + lemma mulf_eq0 (x y : t) : x * y = zeror <=> x = zeror \/ y = zeror. + proof. + split=> [hxy|]; last by case=> ->; rewrite ?(mul0r, mulr0). + case: (x = zeror) => //= nz_x. + have ux : unit x by rewrite unitfP. + by rewrite -(mul1r y) -(mulVr _ ux) -mulrA hxy mulr0. + qed. + + clone IDomainMixin as Dom with + type t <= t, theory R <= R + proof mulf_eq0 by exact mulf_eq0. + + lemma mulfV (x : t): x <> zeror => x * (invr x) = oner. + proof. by move=> nz_x; apply/mulrV; rewrite unitfP. qed. + + lemma mulVf (x : t): x <> zeror => (invr x) * x = oner. + proof. by move=> nz_x; apply/mulVr; rewrite unitfP. qed. + + lemma divff (x : t): x <> zeror => x / x = oner. + proof. by move=> nz_x; apply/divrr; rewrite unitfP. qed. + + lemma invfM (x y : t) : invr (x * y) = invr x * invr y. + proof. + case: (x = zeror) => [->|nz_x]; first by rewrite !(mul0r, invr0). + case: (y = zeror) => [->|nz_y]; first by rewrite !(mulr0, invr0). + by rewrite invrM ?unitfP // mulrC. + qed. + + lemma invf_div x y : invr (x / y) = y / x. + proof. by rewrite invfM invrK mulrC. qed. + + lemma eqf_div (x1 y1 x2 y2 : t) : y1 <> zeror => y2 <> zeror => + (x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1). + proof. by move=> nz_1 nz_2; apply: Dom.eqr_div; rewrite unitfP. qed. + + lemma expfM x y n : exp (x * y) n = exp x n * exp y n. + proof. + elim/intwlog: n => [n h | | n ge0_n ih]. + + by rewrite -(@oppzK n) !(@exprN _ (-n)) h invfM. + + by rewrite !expr0 mulr1. + + by rewrite !exprS // mulrCA -!mulrA -ih mulrCA. + qed. +end FieldMixin. + (* --------------------------------------------------------------------- *) abstract theory Additive. diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index 2d7e57ff8..55dd9664a 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -344,6 +344,16 @@ qed. abbrev exp = ZModpRing.exp. +(* -------------------------------------------------------------------- *) +(* The same field structure as a delta-only mixin over ZModpRing: one *) +(* axiom (units are the nonzero elements), everything else derived *) +(* generically -- including mulf_eq0. The bundled ZModpField clone *) +(* above is kept for compatibility during the migration. *) +clone Ring.FieldMixin as ZModpFieldMx with + type t <= zmod, + theory R <= ZModpRing + proof unitfP by exact unitE. + (* -------------------------------------------------------------------- *) instance field with zmod op rzero = ZModField.zero From e6b9ba168a10bbde3397f06ef611279b5441953c Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 02:50:14 +0200 Subject: [PATCH 15/21] Ring, ZModP: reference-bundles for domains and fields IDomainBundle and FieldBundle package one slot per structure level (carrier, ComRing, mixin), coherently threaded, with no library of their own: consumers declare a single bundle parameter and instances substitute a single theory. A FieldBundle yields an IDomainBundle by construction through the factory's Dom. ZModpFieldBd is the zmod instance. --- theories/algebra/Ring.ec | 16 ++++++++++++++++ theories/algebra/ZModP.ec | 6 ++++++ 2 files changed, 22 insertions(+) diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec index 30c5ccff0..ec235ed70 100644 --- a/theories/algebra/Ring.ec +++ b/theories/algebra/Ring.ec @@ -959,6 +959,22 @@ abstract theory FieldMixin. qed. end FieldMixin. +(* -------------------------------------------------------------------- *) +(* Bundles: references only, one slot per level, no library of their *) +(* own. Consumers declare ONE bundle parameter; instances substitute *) +(* ONE theory. *) +abstract theory IDomainBundle. + type t. + clone import ComRing as R with type t <= t. + clone import IDomainMixin as Dom with type t <= t, theory R <= R. +end IDomainBundle. + +abstract theory FieldBundle. + type t. + clone import ComRing as R with type t <= t. + clone import FieldMixin as F with type t <= t, theory R <= R. +end FieldBundle. + (* --------------------------------------------------------------------- *) abstract theory Additive. diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index 55dd9664a..d844971e5 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -354,6 +354,12 @@ clone Ring.FieldMixin as ZModpFieldMx with theory R <= ZModpRing proof unitfP by exact unitE. +(* the field, as a single substitutable bundle *) +clone Ring.FieldBundle as ZModpFieldBd with + type t <= zmod, + theory R <= ZModpRing, + theory F <= ZModpFieldMx. + (* -------------------------------------------------------------------- *) instance field with zmod op rzero = ZModField.zero From 93e2b90c1daa4a7912c812f32b8520f1d16dd56f Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 10:17:34 +0200 Subject: [PATCH 16/21] Poly: mixin architecture for the IDomain and Field levels The Poly theory now takes its coefficients as CR : ComRing plus CoeffDom : IDomainMixin, realizes PolyComRing's unit/invr definitionally in the include (discharging the three unit axioms, previously left unproven and cleared), and grows the domain level as a delta-only IDomainMixin (IDPoly) over the one PolyComRing object: no duplicate ring object, no clear. PolyField takes the coefficient field as a single FieldBundle parameter K, pierced slot-by-slot into Poly. mul_lc/degM_le/degM_proper move above the inner ring clone (which they never needed) so the include's realize obligations can use them. --- theories/algebra/Poly.ec | 167 +++++++++++++++++---------------------- 1 file changed, 73 insertions(+), 94 deletions(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index afe9c83c9..5a279366f 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -516,32 +516,11 @@ qed. lemma onep_neq0 : poly1 <> poly0. proof. by apply/negP => /poly_eqP /(_ 0); rewrite !polyCE /= oner_neq0. qed. -clone export Ring.ComRing as PolyComRing with - type t <= poly , - op zeror <= poly0, - op oner <= poly1, - op ( + ) <= polyD, - op [ - ] <= polyN, - op ( * ) <= polyM - - proof addrA by apply ZPoly.addrA - proof addrC by apply ZPoly.addrC - proof add0r by apply ZPoly.add0r - proof addNr by apply ZPoly.addNr - proof mulrA by apply mulpA - proof mulrC by apply mulpC - proof mul1r by apply mul1p - proof mulrDl by apply mulpDl - proof oner_neq0 by apply onep_neq0 - - remove abbrev (-) - remove abbrev (/). - (* -------------------------------------------------------------------- *) lemma mul_lc p q : lc p * lc q = (p * q).[deg p + deg q - 2]. proof. -case: (p = poly0) => [->|nz_p]; first by rewrite !(mul0r, poly0E). -case: (q = poly0) => [->|nz_q]; first by rewrite !(mulr0, poly0E). +case: (p = poly0) => [->|nz_p]; first by rewrite mul0p !(mul0r, poly0E). +case: (q = poly0) => [->|nz_q]; first by rewrite mulpC mul0p !(mulr0, poly0E). have ->: deg p + deg q - 2 = (deg p - 1) + (deg q - 1) by ring. pose cp := deg p - 1; pose cq := deg q - 1. rewrite polyME (BCA.bigD1 _ _ cp) ?range_uniq //=. @@ -578,6 +557,27 @@ apply: contraR nz_lc; rewrite eqr_le degM_le //=. by rewrite lerNgt /= => lt_pq; rewrite mul_lc gedeg_coeff //#. qed. +clone export Ring.ComRing as PolyComRing with + type t <= poly , + op zeror <= poly0, + op oner <= poly1, + op ( + ) <= polyD, + op [ - ] <= polyN, + op ( * ) <= polyM + + proof addrA by apply ZPoly.addrA + proof addrC by apply ZPoly.addrC + proof add0r by apply ZPoly.add0r + proof addNr by apply ZPoly.addNr + proof mulrA by apply mulpA + proof mulrC by apply mulpC + proof mul1r by apply mul1p + proof mulrDl by apply mulpDl + proof oner_neq0 by apply onep_neq0 + + remove abbrev (-) + remove abbrev (/). + (* -------------------------------------------------------------------- *) lemma lcM_proper p q : lc p * lc q <> Coeff.zeror => lc (p * q) = lc p * lc q. @@ -1029,105 +1029,82 @@ end PolyComRing. abstract theory Poly. type coeff. -clone import IDomain as IDCoeff with type t <= coeff. +clone import ComRing as CR with type t <= coeff. + +clone import IDomainMixin as CoeffDom with + type t <= coeff, theory R <= CR. clone include PolyComRing with type coeff <- coeff, - theory Coeff <- IDCoeff, + theory Coeff <- CR, op PolyComRing.invr (p : poly) = - (if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p). - -clear [PolyComRing.* PolyComRing.AddMonoid.* PolyComRing.MulMonoid.*]. - -import BigCf. + (if deg p = 1 then polyC (CR.invr p.[0]) else p), + pred PolyComRing.unit (p : poly) = + (deg p = 1 /\ CR.unit p.[0]) + proof *. (* -------------------------------------------------------------------- *) -lemma degM p q : p <> poly0 => q <> poly0 => - deg (polyM p q) = deg p + deg q - 1. -proof. -rewrite -!lc_eq0 -!lregP => reg_p reg_q. -by rewrite &(degM_proper) mulf_eq0 negb_or -!lregP. -qed. - -(* -------------------------------------------------------------------- *) -pred unitp (p : poly) = - deg p = 1 /\ IDCoeff.unit p.[0]. - -(* -------------------------------------------------------------------- *) -op polyV (p : poly) = - if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p. - -(* -------------------------------------------------------------------- *) -clone export Ring.IDomain as IDPoly with - type t <= poly , - op zeror <= poly0, - op oner <= poly1, - op ( + ) <= polyD, - op [ - ] <= polyN, - op ( * ) <= polyM, - op invr <= polyV, - op exp <= PolyComRing.exp, - pred unit <= unitp - - proof * - - remove abbrev (-) - remove abbrev (/). - -realize addrA by apply PolyComRing.addrA . -realize addrC by apply PolyComRing.addrC . -realize add0r by apply PolyComRing.add0r . -realize addNr by apply PolyComRing.addNr . -realize mulrA by apply PolyComRing.mulrA . -realize mulrC by apply PolyComRing.mulrC . -realize mul1r by apply PolyComRing.mul1r . -realize mulrDl by apply PolyComRing.mulrDl . -realize oner_neq0 by apply PolyComRing.oner_neq0. - -(* -------------------------------------------------------------------- *) -realize mulVr. +realize PolyComRing.mulVr. proof. move=> p inv_p; apply/poly_eqP=> c /ler_eqVlt [<<-|]. -+ rewrite polyCE /= polyME /= BCA.big_int1 /= /polyV. - by case: inv_p => -> inv_p0 /=; rewrite polyCE /= mulVr. ++ rewrite polyCE /= polyME /= BigCf.BCA.big_int1 /= /PolyComRing.invr. + by case: inv_p => -> inv_p0 /=; rewrite polyCE /= CR.mulVr. + move=> gt0_c; rewrite polyME polyCE gtr_eqF //=. - rewrite BCA.big_seq BCA.big1 //= => i; rewrite mem_range. - case: inv_p => @/polyV ^ degp -> inv_p0 [+ lt_i_Sc] - /ler_eqVlt [<<-|] /=. + rewrite BigCf.BCA.big_seq BigCf.BCA.big1 //= => i; rewrite mem_range. + case: inv_p => @/PolyComRing.invr ^ degp -> inv_p0 [+ lt_i_Sc] - /ler_eqVlt [<<-|] /=. - by rewrite (gedeg_coeff _ c) -1:mulr0 // degp /#. - move=> gt0_i; rewrite (gedeg_coeff _ i) -1:mul0r //. by apply/(ler_trans _ _ _ (degC_le _)) => /#. qed. (* -------------------------------------------------------------------- *) -realize unitout. +realize PolyComRing.unitout. proof. -move=> p @/unitp @/polyV; case: (deg p = 1) => //=. +move=> p @/PolyComRing.unit @/PolyComRing.invr; case: (deg p = 1) => //=. move=> dp_eq1 unitN_p0; apply/poly_eqP => c ge0_c. case: (c < 1) => [lt1_c|/lerNgt ge1_c]; last first. - rewrite !(@gedeg_coeff _ c) 2:dp_eq1 //. by apply/(ler_trans _ _ _ _ ge1_c)/degC_le. -- suff ->: c = 0 by rewrite polyCE /= invr_out. +- suff ->: c = 0 by rewrite polyCE /= CR.invr_out. by rewrite eqr_le ge0_c /= -ltz1. qed. (* -------------------------------------------------------------------- *) -realize unitP. +realize PolyComRing.unitP. proof. +have degMP: forall (p q : poly), p <> poly0 => q <> poly0 => + deg (polyM p q) = deg p + deg q - 1. ++ move=> p q; rewrite -!lc_eq0 -!CoeffDom.lregP => reg_p reg_q. + by rewrite &(degM_proper) CoeffDom.mulf_eq0 negb_or -!CoeffDom.lregP. move=> p q ^pMqE /(congr1 deg); rewrite deg1. move/(congr1 ((+) 1)) => /=; rewrite addrC; move: pMqE. case: (deg p = 0) => [/deg_eq0->|nz_p]. - by rewrite mulpC mul0p eq_sym onep_neq0. case: (deg q = 0) => [/deg_eq0->|nz_q]. - by rewrite mul0p eq_sym onep_neq0. -rewrite degM -1?deg_eq0 // => ME eq. +rewrite degMP -1?deg_eq0 // => ME eq. have {eq}[]: deg p = 1 /\ deg q = 1 by smt(ge0_deg). move/deg_eq1=> [cp [nz_cp ->>]]; move/deg_eq1=> [cq [nz_cq ->>]]. move/poly_eqP: ME => /(_ 0 _) //; rewrite polyCE /=. -rewrite polyME BCA.big_int1 /= => /IDCoeff.unitP @/unitp -> /=. +rewrite polyME BigCf.BCA.big_int1 /= => /CR.unitP @/PolyComRing.unit -> /=. by rewrite deg_eq1; exists cp. qed. +import BigCf. + +(* -------------------------------------------------------------------- *) +lemma degM p q : p <> poly0 => q <> poly0 => + deg (polyM p q) = deg p + deg q - 1. +proof. +rewrite -!lc_eq0 -!lregP => reg_p reg_q. +by rewrite &(degM_proper) mulf_eq0 negb_or -!lregP. +qed. + (* -------------------------------------------------------------------- *) +clone export IDomainMixin as IDPoly with + type t <= poly, theory R <= PolyComRing + proof *. + realize mulf_eq0. proof. move=> p q; split=> [|[] ->]; last 2 by rewrite (mulr0, mul0r). @@ -1145,21 +1122,21 @@ by rewrite lcM_proper // mulf_eq0 !lc_eq0 !(nz_p, nz_q). qed. (* -------------------------------------------------------------------- *) -lemma degV (p : poly) : deg (polyV p) = deg p. +lemma degV (p : poly) : deg (invr p) = deg p. proof. -rewrite /polyV; case: (deg p = 1); last done. +rewrite /PolyComRing.invr; case: (deg p = 1); last done. by case/deg_eq1=> c [nz_c ->>]; rewrite !degC polyCE /= invr_eq0. qed. (* -------------------------------------------------------------------- *) lemma peval_mprod_out (rs : coeff list) (a : coeff) : - ! (a \in rs) => peval (mprod rs) a <> IDCoeff.zeror. + ! (a \in rs) => peval (mprod rs) a <> CR.zeror. proof. elim: rs => [|r rs ih] /=. -- by rewrite mprod_nil pevalC &(IDCoeff.oner_neq0). +- by rewrite mprod_nil pevalC &(CR.oner_neq0). move/negb_or => [nz_ar a_notin_rs]. rewrite mprod_cons pevalM pevalB pevalX pevalC. -by rewrite &(IDCoeff.mulf_neq0) -1:ih // subr_eq0. +by rewrite &(CoeffDom.mulf_neq0) -1:ih // subr_eq0. qed. end Poly. @@ -1167,12 +1144,14 @@ end Poly. abstract theory PolyField. type coeff. -clone import Field as FCoeff with type t <= coeff. +clone import FieldBundle as K with type t <= coeff. clone include Poly with - type coeff <- coeff, - theory IDCoeff <- FCoeff. + type coeff <- coeff, + theory CR <- K.R, + theory CoeffDom <- K.F.Dom. +import K.R K.F. import BigCf BigPoly. (* -------------------------------------------------------------------- *) @@ -1184,7 +1163,7 @@ theory Lagrange. polyC (invr (peval (mprod (rem r rs)) r)) * mprod (rem r rs). lemma lag_eval_same (rs : coeff list) (r : coeff) : - uniq rs => r \in rs => peval (lag rs r) r = FCoeff.oner. + uniq rs => r \in rs => peval (lag rs r) r = K.R.oner. proof. move=> hu hmem @/lag; rewrite pevalM pevalC. rewrite &(mulVf) &(peval_mprod_out). @@ -1193,7 +1172,7 @@ theory Lagrange. lemma lag_eval_other (rs : coeff list) (r r' : coeff) : uniq rs => r' \in rs => r' <> r - => peval (lag rs r) r' = FCoeff.zeror. + => peval (lag rs r) r' = K.R.zeror. proof. move=> hu hm hne @/lag; rewrite pevalM. rewrite (mprod_root (rem r rs) r'). From 538159e001d8a2704c050f79438ef32819b5547e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 10:17:34 +0200 Subject: [PATCH 17/21] ZModP: remove the bundled ZModpField clone The field level keeps the one ring object (ZModpRing) and gets its field structure from the ZModpFieldMx mixin / ZModpFieldBd bundle. The old Ring.Field clone's import role is preserved by importing ZModpRing and the mixin at the same spot, so downstream vocabulary is unchanged; exp_mod bridges its one unit side-goal with unitE (the style exp_pow already used). Field-requesting consumers (DHIES, SchnorrPK, elgamal, cramer-shoup, UC/dh_enc) clone the field bundle; Group's g_neq0 hint becomes oner_neq0. --- examples/SchnorrPK.ec | 4 +- examples/UC/dh_enc.ec | 4 +- examples/cramer-shoup/cramer_shoup.ec | 8 +-- examples/elgamal.ec | 6 +-- theories/algebra/Group.ec | 2 +- theories/algebra/ZModP.ec | 77 +++++++-------------------- theories/crypto/assumptions/DHIES.ec | 4 +- 7 files changed, 33 insertions(+), 72 deletions(-) diff --git a/examples/SchnorrPK.ec b/examples/SchnorrPK.ec index 811049608..ed9c3630e 100644 --- a/examples/SchnorrPK.ec +++ b/examples/SchnorrPK.ec @@ -15,7 +15,7 @@ clone G.PowZMod as GP with clone GP.FDistr as FD. -clone GP.ZModE.ZModpField as ZPF. +clone GP.ZModE.ZModpFieldBd as ZPF. import G GP GP.ZModE FD. @@ -145,7 +145,7 @@ section SchnorrPKSecurity. auto; rewrite /R /R_DL /oget => &hr /> hne 2!-> /=. rewrite expM !expB accepting_transcript_1 accepting_transcript_2. rewrite invM (mulcC m{hr}) -mulcA (mulcA m{hr}) mulcV mulcA mulc1 -expB -expM. - by rewrite ZPF.divrr ?ZPF.subr_eq0 // exp1. + by rewrite ZPF.F.divff ?ZPF.R.subr_eq0 // exp1. qed. (* Special honest verifier zero knowledge *) diff --git a/examples/UC/dh_enc.ec b/examples/UC/dh_enc.ec index ef2bd6d93..750ae5969 100644 --- a/examples/UC/dh_enc.ec +++ b/examples/UC/dh_enc.ec @@ -328,7 +328,7 @@ require DiffieHellman. clone DiffieHellman as DH. import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE. -clone DH.GP.ZModE.ZModpField as ZPF. +clone DH.GP.ZModE.ZModpFieldBd as ZPF. (* Such statements make no sense when we don't restrict to a complexity class @@ -897,7 +897,7 @@ wp;call (_: ={glob HybFChan.F2Auth.F2Auth, ); last first. (* Init *) -by auto => /> &2; rewrite expM /= -expM ZPF.mulrC expM. +by auto => /> &2; rewrite expM /= -expM ZPF.R.mulrC expM. (* Now the call *) + by proc;inline *; auto => /> /#. + by sim />. diff --git a/examples/cramer-shoup/cramer_shoup.ec b/examples/cramer-shoup/cramer_shoup.ec index f852e4bcb..cb9055a89 100644 --- a/examples/cramer-shoup/cramer_shoup.ec +++ b/examples/cramer-shoup/cramer_shoup.ec @@ -9,7 +9,7 @@ require DiffieHellman. clone DiffieHellman as DH. import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE. -clone DH.GP.ZModE.ZModpField as ZPF. +clone DH.GP.ZModE.ZModpFieldBd as ZPF. lemma gt1_q : 1 < order by smt(ge2_p). @@ -576,7 +576,7 @@ section Security_Aux. move=> kL _ xL _ x2L _ yL _ y2L _ zL _ resu bL _. have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring. have H2 : (-uL) * wL + u'L * wL <> zero. - + rewrite H1 ZPF.mulf_eq0 negb_or HwL /=. + + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL /=. by move: Hu'L;apply: contra => H;ring H. split => [? _ | _ ]; 1: by field. move=> z2L _; split => [ | _]; 1: by field. @@ -605,7 +605,7 @@ section Security_Aux. move=> kL _ yL _ y2L _ zL _ r'L _ xL _. have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring. have H2 : (-uL) * wL + u'L * wL <> zero. - + rewrite H1 ZPF.mulf_eq0 negb_or HwL /=. + + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL /=. by move: Hu'L;apply: contra => H;ring H. split => [? _ | _ ]; 1: by field. move=> z2L _; split => [ | _]; 1: by field. @@ -751,7 +751,7 @@ section Security_Aux. move=> yL _ y2L _ zL _ r'L _ xL _ rL _. have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring. have H2 : (-uL) * wL + u'L * wL <> zero. - + rewrite H1 ZPF.mulf_eq0 negb_or HwL0 /=. + + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL0 /=. by move: HuL;apply: contra => H;ring H. split => [ | _ /#]. rewrite log_bij !(logg1, logrzM, logDr); field. diff --git a/examples/elgamal.ec b/examples/elgamal.ec index 2dd1e2204..222b8d972 100644 --- a/examples/elgamal.ec +++ b/examples/elgamal.ec @@ -11,7 +11,7 @@ pragma +implicits. clone DiffieHellman as DH. import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE. -clone DH.GP.ZModE.ZModpField as ZPF. +clone DH.GP.ZModE.ZModpFieldBd as ZPF. (** Construction: a PKE **) type pkey = group. @@ -107,8 +107,8 @@ section Security. (fun z, z - loge (if b then m1 else m0){2}). auto; call (_:true). auto; progress. - - by rewrite ZPF.addrAC -ZPF.addrA ZPF.subrr ZPF.addr0. - - by rewrite -ZPF.addrA ZPF.subrr ZPF.addr0. + - by rewrite ZPF.R.addrAC -ZPF.R.addrA ZPF.R.subrr ZPF.R.addr0. + - by rewrite -ZPF.R.addrA ZPF.R.subrr ZPF.R.addr0. - by rewrite expD expgK. qed. diff --git a/theories/algebra/Group.ec b/theories/algebra/Group.ec index f22be893f..c770d35a1 100644 --- a/theories/algebra/Group.ec +++ b/theories/algebra/Group.ec @@ -568,7 +568,7 @@ lemma div_def (a b : group): g ^ (loge a - loge b) = a / b by rewrite log_bij logDrN loggK. lemma g_neq0 : g ^ zero <> g - by rewrite -{2}[g]exp1 -pow_bij; smt(ZModpField.unitr1). + by rewrite -{2}[g]exp1 -pow_bij; smt(ZModpRing.oner_neq0). lemma mulN (x : group) : x * inv x = g ^ zero by rewrite mulcV -(exp0 g). diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index d844971e5..752d7bb78 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -302,54 +302,15 @@ apply/mulmV; first by apply/prime_p. by move: nz_x; rewrite -asint_eq zeroE pmod_small // rg_asint. qed. -clone import Ring.Field as ZModpField with - type t <= zmod, - op zeror <= zero, - op oner <= one, - op ( + ) <= ( + ), - op [ - ] <= ([-]), - op ( * ) <= ( * ), - op invr <= inv, - op exp <= ZModpRing.exp - proof * - remove abbrev (-) - remove abbrev (/). - -realize addrA. proof. by apply/ZModule.addrA. qed. -realize addrC. proof. by apply/ZModule.addrC. qed. -realize add0r. proof. by apply/ZModule.add0r. qed. -realize addNr. proof. by apply/ZModule.addNr. qed. -realize mulrA. proof. by apply/ComRing.mulrA. qed. -realize mulrC. proof. by apply/ComRing.mulrC. qed. -realize mul1r. proof. by apply/ComRing.mul1r. qed. -realize mulrDl. proof. by apply/ComRing.mulrDl. qed. -realize oner_neq0. proof. by apply/ComRing.oner_neq0. qed. - -realize mulVr. -proof. by move=> x nz_x; rewrite &(ComRing.mulVr) unitE. qed. - -realize unitP. -proof. by move=> x y h; rewrite -unitE &(ComRing.unitP _ y). qed. - -realize unitout. -proof. by move=> x; rewrite -unitE &(ComRing.unitout). qed. - -realize mulf_eq0. -proof. (* FIXME: should be generic *) -move=> x y; case: (x = zero) => //= [->|]; first by rewrite ZModpRing.mul0r. -move=> nz_x; split=> [|->]; last by rewrite ZModpRing.mulr0. -move=> h; apply: (ZModpRing.mulrI x); last by rewrite ZModpRing.mulr0. -by rewrite unitE. -qed. +import ZModpRing. abbrev exp = ZModpRing.exp. (* -------------------------------------------------------------------- *) -(* The same field structure as a delta-only mixin over ZModpRing: one *) -(* axiom (units are the nonzero elements), everything else derived *) -(* generically -- including mulf_eq0. The bundled ZModpField clone *) -(* above is kept for compatibility during the migration. *) -clone Ring.FieldMixin as ZModpFieldMx with +(* The field structure as a delta-only mixin over ZModpRing: one axiom *) +(* (units are the nonzero elements), everything else derived *) +(* generically -- including mulf_eq0. *) +clone import Ring.FieldMixin as ZModpFieldMx with type t <= zmod, theory R <= ZModpRing proof unitfP by exact unitE. @@ -370,19 +331,19 @@ instance field with zmod op inv = ZModField.inv op expr = ZModpRing.exp - proof oner_neq0 by apply/ZModpField.oner_neq0 - proof addr0 by apply/ZModpField.addr0 - proof addrA by apply/ZModpField.addrA - proof addrC by apply/ZModpField.addrC - proof addrN by apply/ZModpField.addrN - proof mulr1 by apply/ZModpField.mulr1 - proof mulrA by apply/ZModpField.mulrA - proof mulrC by apply/ZModpField.mulrC - proof mulrDl by apply/ZModpField.mulrDl - proof mulrV by apply/ZModpField.mulrV - proof expr0 by apply/ZModpField.expr0 - proof exprS by apply/ZModpField.exprS - proof exprN by (move=> ?? _; apply/ZModpField.exprN). + proof oner_neq0 by apply/ZModpRing.oner_neq0 + proof addr0 by apply/ZModpRing.addr0 + proof addrA by apply/ZModpRing.addrA + proof addrC by apply/ZModpRing.addrC + proof addrN by apply/ZModpRing.addrN + proof mulr1 by apply/ZModpRing.mulr1 + proof mulrA by apply/ZModpRing.mulrA + proof mulrC by apply/ZModpRing.mulrC + proof mulrDl by apply/ZModpRing.mulrDl + proof mulrV by apply/ZModpFieldMx.mulfV + proof expr0 by apply/ZModpRing.expr0 + proof exprS by apply/ZModpRing.exprS + proof exprN by (move=> ?? _; apply/ZModpRing.exprN). (* -------------------------------------------------------------------- *) lemma exp_inzmod m n : @@ -449,7 +410,7 @@ proof. rewrite -(invrK (exp (inzmod _) _)); apply congr1. rewrite -exprN -(mul1r (exp _ _)). rewrite -(expr1z (- n %/ k)) -eq_exp_one -exprM mulrN Ring.IntID.mulrC -exprD. - + apply/negP => eq_inzmod_zero; move: eq_inzmod_zero eq_exp_one => ->. + + rewrite unitE; apply/negP => eq_inzmod_zero; move: eq_inzmod_zero eq_exp_one => ->. by rewrite expr0z neqk0 /= eq_sym oner_neq0. by rewrite -opprD -divz_eq inzmod_exp oppr_ge0 ltzW //= ltrNge. qed. diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec index e8c6830e4..819bb2a53 100644 --- a/theories/crypto/assumptions/DHIES.ec +++ b/theories/crypto/assumptions/DHIES.ec @@ -20,7 +20,7 @@ theory DHIES. type range <- K, op q_ror <- q_lor. - clone GP.ZModE.ZModpField as ZPF. + clone GP.ZModE.ZModpFieldBd as ZPF. type group = ODH.G.group. type exp = ODH.GP.exp. @@ -546,7 +546,7 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1 move: (assoc_some _ _ _ H20) => /mapP [v [? /= [[H22 H23] H24]]]. rewrite H24 H23 -H22. move: (H4 _ _ H18) => ->; congr. - by rewrite -!GP.expM ZPF.mulrC. + by rewrite -!GP.expM ZPF.R.mulrC. by wp; skip; rewrite /inv /=; clear inv => />; smt(). + proc; inline*. sp 1 1 ; if; first by rewrite /inv. From 5734cf68ff1e754bf5f68ef019df25bbd7b28ca5 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 10:41:38 +0200 Subject: [PATCH 18/21] Ideal, CommAlgebra: mixin parameters; BigPoly's CR slot as alias Ideal.Ideal and CommAlgebra.Base now take R : ComRing plus Dom : IDomainMixin instead of a fresh IDomain object: Ideal's op-by-op push-down into IdealComRing (with its twelve delegated realizes and clear) collapses to the single substitution theory IComRing <- R. Base keeps owning BR and pushes R/Dom/BR into its Ideal clone. Poly's BigPoly binds its CR slot with <= instead of <-, keeping the alias navigable so BigPoly is substitutable from outside. With this, the previously-blocked instantiation goes through as one coherent substitution -- clone CommAlgebra.Base as ZqCA with type t <= ZqP.poly, theory R <= ZqP.PolyComRing, theory Dom <= ZqP.IDPoly, theory BR <= ZqP.BigPoly { rename "BAdd" as "PCA" "BMul" as "PCM" }. -- and the bigop sharing ZqCA.BR.BMul.big = ZqP.BigPoly.PCM.big is definitional (closed by reflexivity). --- theories/algebra/CommAlgebra.ec | 16 ++++++++------ theories/algebra/Ideal.ec | 37 +++++---------------------------- theories/algebra/Poly.ec | 2 +- 3 files changed, 16 insertions(+), 39 deletions(-) diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec index b8b73bf0a..fbc8e4343 100644 --- a/theories/algebra/CommAlgebra.ec +++ b/theories/algebra/CommAlgebra.ec @@ -16,19 +16,23 @@ abstract theory Base. (* -------------------------------------------------------------------- *) type t. -clone import IDomain as ID with type t <= t. +clone import Ring.ComRing as R with type t <= t. + +clone import Ring.IDomainMixin as Dom with + type t <= t, theory R <= R. (* -------------------------------------------------------------------- *) (* The big operators are owned here and pushed down into the Ideal *) (* clone, so that instances only ever substitute top-level theories. *) clone BigComRing as BR with - theory CR <= ID. + theory CR <= R. (* -------------------------------------------------------------------- *) clone Ideal.Ideal as I with - type t <- t, - theory IDomain <- ID, - theory BigDom <- BR. + type t <- t, + theory R <- R, + theory Dom <- Dom, + theory BigDom <- BR. (* -------------------------------------------------------------------- *) abbrev (+) = I.idD. @@ -307,7 +311,7 @@ abstract theory Euclidean. (* -------------------------------------------------------------------- *) clone include Base. -import ID I. +import R Dom I. (* -------------------------------------------------------------------- *) op w : t -> int. diff --git a/theories/algebra/Ideal.ec b/theories/algebra/Ideal.ec index f232a4a46..3d8f640fe 100644 --- a/theories/algebra/Ideal.ec +++ b/theories/algebra/Ideal.ec @@ -558,41 +558,14 @@ end IdealComRing. abstract theory Ideal. type t. -clone import IDomain with type t <- t. +clone import Ring.ComRing as R with type t <= t. -clear [IDomain.* IDomain.AddMonoid.* IDomain.MulMonoid.*]. +clone import Ring.IDomainMixin as Dom with + type t <= t, theory R <= R. clone include IdealComRing with - type t <- t, - pred IComRing.unit <- IDomain.unit, - op IComRing.zeror <- IDomain.zeror, - op IComRing.oner <- IDomain.oner, - op IComRing.( + ) <- IDomain.( + ), - op IComRing.([-]) <- IDomain.([-]), - op IComRing.( * ) <- IDomain.( * ), - op IComRing.invr <- IDomain.invr, - op IComRing.intmul <- IDomain.intmul, - op IComRing.ofint <- IDomain.ofint, - op IComRing.exp <- IDomain.exp, - op IComRing.lreg <- IDomain.lreg - - proof IComRing.* - - remove abbrev IComRing.(-) - remove abbrev IComRing.(/). - -realize IComRing.addrA by apply: IDomain.addrA . -realize IComRing.addrC by apply: IDomain.addrC . -realize IComRing.add0r by apply: IDomain.add0r . -realize IComRing.addNr by apply: IDomain.addNr . -realize IComRing.oner_neq0 by apply: IDomain.oner_neq0. -realize IComRing.mulrA by apply: IDomain.mulrA . -realize IComRing.mulrC by apply: IDomain.mulrC . -realize IComRing.mul1r by apply: IDomain.mul1r . -realize IComRing.mulrDl by apply: IDomain.mulrDl . -realize IComRing.mulVr by apply: IDomain.mulVr . -realize IComRing.unitP by apply: IDomain.unitP . -realize IComRing.unitout by apply: IDomain.unitout . + type t <- t, + theory IComRing <- R. lemma eqmodfP x y : (x %= y) <=> (exists u, unit u /\ x = u * y). proof. diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 5a279366f..d3f30fd20 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -689,7 +689,7 @@ qed. (* -------------------------------------------------------------------- *) theory BigPoly. -clone include BigComRing with theory CR <- PolyComRing +clone include BigComRing with theory CR <= PolyComRing remove abbrev CR.(-) remove abbrev CR.(/) From 95b5855d72e5b3dd360797123ee96c25fe9381a7 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 18 Jul 2026 23:24:24 +0200 Subject: [PATCH 19/21] CommAlgebra: generic congruence modulo an element (eqm) Base gets the modulus-parametric congruence eqm m x y, an abbreviation for m %| (x - y) (so it converts freely with the divisibility form), together with its kit: eqmP (Bezout-witness form), eqm_refl/sym/trans, eqm_eq, eqm_mod0, the ring-operation congruences eqmD/N/B/M, and the CRT-tree descend eqm_mulm. This is the generic content of the peqm kit that lived in the ML-DSA development. --- theories/algebra/CommAlgebra.ec | 71 +++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec index fbc8e4343..c4df46ba7 100644 --- a/theories/algebra/CommAlgebra.ec +++ b/theories/algebra/CommAlgebra.ec @@ -152,6 +152,77 @@ move/perm_to_rem: x_in_cs => /BR.BMul.eq_big_perm ->. by rewrite BR.BMul.big_cons Px /= dvdr_mulr. qed. +(* ==================================================================== *) +(* Congruence modulo an element: the modulus-parametric equality *) +(* eqm m x y, i.e. m %| (x - y). An abbreviation, so hypotheses and *) +(* goals convert freely with the divisibility form. *) +(* ==================================================================== *) +abbrev eqm (m x y : t) = m %| (x - y). + +lemma eqmP (m x y : t) : eqm m x y <=> exists h, x - y = h * m. +proof. by apply: dvdrP. qed. + +(* -------------------------------------------------------------------- *) +lemma eqm_refl (m x : t) : eqm m x x. +proof. by rewrite subrr dvdr0. qed. + +(* -------------------------------------------------------------------- *) +lemma eqm_sym (m x y : t) : eqm m x y => eqm m y x. +proof. by move=> h; rewrite -opprB dvdrN. qed. + +(* -------------------------------------------------------------------- *) +lemma eqm_trans (m y x z : t) : eqm m x y => eqm m y z => eqm m x z. +proof. +move=> h1 h2; have ->: x - z = (x - y) + (y - z). +- by rewrite addrA subrK. +by apply dvdrD. +qed. + +(* -------------------------------------------------------------------- *) +lemma eqm_eq (m x y : t) : x = y => eqm m x y. +proof. by move=> ->; apply eqm_refl. qed. + +(* the modulus is congruent to zero *) +lemma eqm_mod0 (m : t) : eqm m m zeror. +proof. by rewrite subr0 dvdrr. qed. + +(* -------------------------------------------------------------------- *) +lemma eqmD (m x1 x2 y1 y2 : t) : + eqm m x1 x2 => eqm m y1 y2 => eqm m (x1 + y1) (x2 + y2). +proof. +move=> h1 h2; have ->: x1 + y1 - (x2 + y2) = (x1 - x2) + (y1 - y2). +- by rewrite opprD addrACA. +by apply dvdrD. +qed. + +(* -------------------------------------------------------------------- *) +lemma eqmN (m x y : t) : eqm m x y => eqm m (- x) (- y). +proof. +move=> h; have ->: - x - - y = - (x - y). +- by rewrite opprK opprB addrC. +by apply dvdrN. +qed. + +(* -------------------------------------------------------------------- *) +lemma eqmB (m x1 x2 y1 y2 : t) : + eqm m x1 x2 => eqm m y1 y2 => eqm m (x1 - y1) (x2 - y2). +proof. by move=> h1 h2; apply eqmD => //; apply eqmN. qed. + +(* -------------------------------------------------------------------- *) +lemma eqmM (m x1 x2 y1 y2 : t) : + eqm m x1 x2 => eqm m y1 y2 => eqm m (x1 * y1) (x2 * y2). +proof. +move=> h1 h2; have ->: x1 * y1 - x2 * y2 = x1 * (y1 - y2) + (x1 - x2) * y2. +- by rewrite mulrBr mulrBl addrA subrK. +by apply dvdrD; [apply dvdr_mull | apply dvdr_mulr]. +qed. + +(* restriction to a factor of the modulus: the CRT-tree "descend" *) +lemma eqm_mulm (m1 m2 x y : t) : eqm (m1 * m2) x y => eqm m1 x y. +proof. +by move=> h; apply (dvdr_trans (m1 * m2)) => //; apply/dvdr_mulr/dvdrr. +qed. + (* ==================================================================== *) (* Co-maximality, with explicit Bezout witnesses. The CRT cluster is *) (* stated at this level: it consumes co-primality only through the *) From 1c083196c094c66355f21582410b9efce01dd5b6 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 19 Jul 2026 15:40:28 +0200 Subject: [PATCH 20/21] Packed theory aliases: theory A = T1 + ... + Tn Generalize the single-target theory alias (Th_alias) to an ordered list of targets. A packed alias merges the targets' members under one name, as a pure view: every entry keeps its original path, so resolution always yields the aliased objects -- no copies, no proof obligations, and no duplicated theory objects. Name clashes across targets behave like imports (type-directed, ambiguous otherwise). Packed targets are restricted to sibling theories, so the alias's components can be reconstructed purely from the enclosing theory when it is required (this implements the FIXME:ALIAS in the member-lookup tables, for single-target aliases too). Rebinding is idempotent, as aliases are rebound on every import of the enclosing theory. In clone replay, alias items now apply rename clauses to the alias name and push the substitution through the target paths (fixing two latent bugs of the single-target replay: renames were ignored and the item was re-added with unsubstituted targets). --- src/ecCommands.ml | 2 +- src/ecEnv.ml | 98 +++++++++++++++++++++++++++++++----- src/ecEnv.mli | 2 +- src/ecParser.mly | 2 +- src/ecParsetree.ml | 2 +- src/ecPrinting.ml | 5 +- src/ecScope.ml | 31 +++++++++--- src/ecScope.mli | 2 +- src/ecSubst.ml | 2 +- src/ecTheory.ml | 2 +- src/ecTheory.mli | 2 +- src/ecTheoryReplay.ml | 15 +++--- tests/theory-alias-packed.ec | 51 +++++++++++++++++++ 13 files changed, 181 insertions(+), 35 deletions(-) create mode 100644 tests/theory-alias-packed.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 3e08fb640..7afa09463 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -662,7 +662,7 @@ and process_th_clone (scope : EcScope.scope) thcl = EcScope.Cloning.clone scope (Pragma.get ()).pm_check thcl (* -------------------------------------------------------------------- *) -and process_th_alias (scope : EcScope.scope) (thcl : psymbol * pqsymbol) = +and process_th_alias (scope : EcScope.scope) (thcl : psymbol * pqsymbol list) = EcScope.check_state `InTop "theory alias" scope; EcScope.Theory.alias scope thcl diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 62b8bf4af..5a735e93a 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -312,6 +312,29 @@ let empty_mc params = { mc_components = MMsym.empty; } +(* -------------------------------------------------------------------- *) +(* Merge the members of [mc2] into [mc1]. Entries keep their original + * paths; bindings of [mc2] shadow same-named bindings of [mc1] (the + * most recently merged component wins, as with imports). *) +let mc_merge (mc1 : mc) (mc2 : mc) = + let merge m1 m2 = + MMsym.fold + (fun x vs acc -> List.fold_right (fun v acc -> MMsym.add x v acc) vs acc) + m2 m1 in + + { mc_parameters = mc1.mc_parameters; + mc_modules = merge mc1.mc_modules mc2.mc_modules; + mc_modsigs = merge mc1.mc_modsigs mc2.mc_modsigs; + mc_tydecls = merge mc1.mc_tydecls mc2.mc_tydecls; + mc_operators = merge mc1.mc_operators mc2.mc_operators; + mc_axioms = merge mc1.mc_axioms mc2.mc_axioms; + mc_theories = merge mc1.mc_theories mc2.mc_theories; + mc_variables = merge mc1.mc_variables mc2.mc_variables; + mc_functions = merge mc1.mc_functions mc2.mc_functions; + mc_typeclasses= merge mc1.mc_typeclasses mc2.mc_typeclasses; + mc_rwbase = merge mc1.mc_rwbase mc2.mc_rwbase; + mc_components = merge mc1.mc_components mc2.mc_components; } + (* -------------------------------------------------------------------- *) let empty_norm_cache = { norm_mp = Mm.empty; @@ -1153,9 +1176,37 @@ module MC = struct | Th_baserw (x, _) -> (add2mc _up_rwbase x (expath x) mc, None) - | Th_alias _ -> - (* FIXME:ALIAS *) - (mc, None) + | Th_alias (name, targets) -> begin + (* Alias entries resolve to their targets. A single-target + * alias is a pure component redirection; a packed alias + * (several targets) gets a merged component built from the + * sibling targets (enforced in [EcScope.Theory.alias]), + * whose entries keep the targets' paths. *) + match targets with + | [target] -> + (_up_mc ~name false mc (IPPath target), None) + + | targets -> + let mc_of_target (target : path) = + let tname = EcPath.basename target in + let tcth = + List.find_map_opt + (fun item -> + match item.ti_item with + | Th_theory (x, tcth) when x = tname -> Some tcth + | _ -> None) + cth.cth_items in + (* enforced by [EcScope.Theory.alias] *) + let tcth = oget tcth in + let ((_, tmc), _) = mc_of_theory_r subscope (tname, tcth) in + tmc in + + let merged = + List.fold_left mc_merge (empty_mc None) + (List.map mc_of_target targets) in + let mc = _up_mc false mc (IPPath (expath name)) in + (mc, Some ((name, merged), [])) + end | Th_export _ | Th_addrw _ | Th_instance _ @@ -3512,18 +3563,39 @@ module Theory = struct Option.get (Mp.find_opt p env.env_thenvs) (* ------------------------------------------------------------------ *) - let rebind_alias (name : symbol) (path : path) (env : env) = - let th = by_path path env in - let src = EcPath.pqname (root env) name in - let env = MC.import_theory ~name path th env in - let env = MC.import_mc ~name (IPPath path) env in - let env = { env with env_albase = Mp.add path src env.env_albase } in - env + let rebind_alias (name : symbol) (paths : path list) (env : env) = + match paths with + | [path] -> + let th = by_path path env in + let src = EcPath.pqname (root env) name in + let env = MC.import_theory ~name path th env in + let env = MC.import_mc ~name (IPPath path) env in + let env = { env with env_albase = Mp.add path src env.env_albase } in + env + + | paths -> + (* Packed alias: merge the targets' components under the alias + * name. Entries keep their original paths, so resolution + * always yields the aliased objects -- no copies. Contrary to + * [MC.bind_mc], rebinding must be idempotent: the alias is + * rebound on every import of the enclosing theory. *) + let mc_of (p : path) = + oget (Mip.find_opt (IPPath p) env.env_comps) in + let merged = + List.fold_left mc_merge (empty_mc None) (List.map mc_of paths) in + let apath = IPPath (EcPath.pqname (root env) name) in + { env with + env_current = MC._up_mc true env.env_current apath; + env_comps = + Mip.change + (fun mc -> Some (MC._up_mc true (oget mc) apath)) + (IPPath (root env)) + (Mip.add apath merged env.env_comps); } (* ------------------------------------------------------------------ *) - let alias ?(import = true) (name : symbol) (path : path) (env : env) = - let env = if import then rebind_alias name path env else env in - { env with env_item = mkitem ~import (Th_alias (name, path)) :: env.env_item } + let alias ?(import = true) (name : symbol) (paths : path list) (env : env) = + let env = if import then rebind_alias name paths env else env in + { env with env_item = mkitem ~import (Th_alias (name, paths)) :: env.env_item } (* ------------------------------------------------------------------ *) let aliases (env : env) = diff --git a/src/ecEnv.mli b/src/ecEnv.mli index debf6ce40..b54104b1d 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -326,7 +326,7 @@ module Theory : sig -> EcTheory.thmode -> env -> compiled_theory option - val alias : ?import:bool -> symbol -> path -> env -> env + val alias : ?import:bool -> symbol -> path list -> env -> env val aliases : env -> path Mp.t end diff --git a/src/ecParser.mly b/src/ecParser.mly index 9552a74a1..044529dab 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3938,7 +3938,7 @@ realize: (* Theory aliasing *) theory_alias: (* FIXME: THEORY ALIAS -> S/R conflict *) -| THEORY name=uident EQ target=uqident { (name, target) } +| THEORY name=uident EQ targets=plist1(uqident, PLUS) { (name, targets) } (* -------------------------------------------------------------------- *) (* Printing *) diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 2a70a2e92..9abb35e5c 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1501,7 +1501,7 @@ type global_action = | GthImport of pqsymbol list | GthExport of pqsymbol list | GthClone of theory_cloning - | GthAlias of (psymbol * pqsymbol) + | GthAlias of (psymbol * pqsymbol list) | GModImport of pmsymbol located list | GsctOpen of osymbol_r | GsctClose of osymbol_r diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 3fd831673..c274de77e 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3953,8 +3953,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = Format.fprintf fmt "%abind circuit %a \"%s\"." pp_locality lc (pp_opname ppe) cr.operator cr.name end - | EcTheory.Th_alias (name, target) -> - Format.fprintf fmt "theory %s = %a." name (pp_thname ~alias:false ppe) target + | EcTheory.Th_alias (name, targets) -> + Format.fprintf fmt "theory %s = %a." name + (pp_list " +@ " (pp_thname ~alias:false ppe)) targets (* -------------------------------------------------------------------- *) and pp_th_item ppe p fmt item = diff --git a/src/ecScope.ml b/src/ecScope.ml index 8f0e27f87..00d31f99e 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2065,12 +2065,31 @@ module Theory = struct let required scope = scope.sc_required (* -------------------------------------------------------------------- *) - let alias (scope : scope) ((name, target) : psymbol * pqsymbol) = - let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in - let thpath, _ = ofdfl (fun () -> - hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target) - ) thpath in - let item = EcTheory.mkitem ~import:true (Th_alias (unloc name, thpath)) in + let alias (scope : scope) ((name, targets) : psymbol * pqsymbol list) = + let resolve (target : pqsymbol) = + let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in + let thpath, _ = ofdfl (fun () -> + hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target) + ) thpath in + thpath in + + let thpaths = List.map resolve targets in + + (* Packed aliases (more than one target) merge the targets' members + * under one name. Restrict the targets to sibling sub-theories of + * the current scope, so that the components of the alias can be + * reconstructed purely from the enclosing theory (see + * [EcEnv.MC.mc_of_theory_r]). *) + if List.length thpaths > 1 then begin + let root = EcEnv.root (env scope) in + List.iter2 (fun target thpath -> + if EcPath.prefix thpath <> Some root then + hierror ~loc:(loc target) + "packed theory aliases must reference sibling theories") + targets thpaths + end; + + let item = EcTheory.mkitem ~import:true (Th_alias (unloc name, thpaths)) in { scope with sc_env = EcSection.add_item item scope.sc_env } end diff --git a/src/ecScope.mli b/src/ecScope.mli index d73ed66d7..b1bc588b4 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -219,7 +219,7 @@ module Theory : sig (* [alias scope (name, thname)] create a theory alias [name] to * [thname] *) - val alias : scope -> psymbol * pqsymbol -> scope + val alias : scope -> psymbol * pqsymbol list -> scope end (* -------------------------------------------------------------------- *) diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 6dbf75ad4..c48da1503 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1201,7 +1201,7 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = Th_crbinding (subst_crbinding s bd, lc) | Th_alias (name, target) -> - Th_alias (name, subst_path s target) + Th_alias (name, List.map (subst_path s) target) (* -------------------------------------------------------------------- *) and subst_theory (s : subst) (items : theory) = diff --git a/src/ecTheory.ml b/src/ecTheory.ml index e4e5125da..4076d9d21 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -32,7 +32,7 @@ and theory_item_r = | Th_reduction of reduction_rule | Th_crbinding of crbinding * is_local | Th_auto of auto_rule - | Th_alias of (symbol * path) (* FIXME: currently, only theories *) + | Th_alias of (symbol * path list) (* FIXME: currently, only theories *) and thsource = { ths_base : EcPath.path; diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 4305ad157..7f5180892 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -29,7 +29,7 @@ and theory_item_r = | Th_reduction of reduction_rule | Th_crbinding of crbinding * is_local | Th_auto of auto_rule - | Th_alias of (symbol * path) + | Th_alias of (symbol * path list) and thsource = { ths_base : EcPath.path; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 380bc501d..35c016e85 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -1265,16 +1265,19 @@ and replay_crbinding (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bindi (* -------------------------------------------------------------------- *) and replay_alias - (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, target) + (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, targets) = let scenv = ove.ovre_hooks.henv scope in let env = EcSection.env scenv in - let p = EcSubst.subst_path subst target in + let targets = List.map (EcSubst.subst_path subst) targets in + let subst, name = rename ove subst (`Theory, name) in - if is_none (EcEnv.Theory.by_path_opt p env) then + if List.for_all + (fun p -> is_some (EcEnv.Theory.by_path_opt p env)) targets + then + let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, targets)) in (subst, ops, proofs, scope) else - let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, target)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) @@ -1328,8 +1331,8 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) = | Th_instance _ -> (subst, ops, proofs, scope) - | Th_alias (name, target) -> - replay_alias ove (subst, ops, proofs, scope) (item.ti_import, name, target) + | Th_alias (name, targets) -> + replay_alias ove (subst, ops, proofs, scope) (item.ti_import, name, targets) | Th_crbinding (binding, lc) when not hidden -> replay_crbinding ove (subst, ops, proofs, scope) (item.ti_import, binding, lc) diff --git a/tests/theory-alias-packed.ec b/tests/theory-alias-packed.ec new file mode 100644 index 000000000..799b74b80 --- /dev/null +++ b/tests/theory-alias-packed.ec @@ -0,0 +1,51 @@ +require import AllCore. + +theory T1. + op o1 : int = 1. + op shared : int = 10. + lemma L1 : o1 = 1. proof. by []. qed. +end T1. + +theory T2. + op o2 : int = 2. + op shared : int = 20. + lemma L2 : o2 = 2. proof. by []. qed. +end T2. + +(* top-level packed alias *) +theory A = T1 + T2. + +lemma test1 : A.o1 = 1. proof. by apply A.L1. qed. +lemma test2 : A.o2 = 2. proof. by apply A.L2. qed. + +(* name clashes across targets are ambiguous, as with imports; + resolution is by type when types differ *) + +(* single-target alias still works *) +theory B = T1. +lemma test_single : B.o1 = 1. proof. by apply B.L1. qed. + +(* enclosing theory: exercises the mc_of_theory_r (require/close) path *) +theory Outer. + theory S1. op a : int = 3. lemma La : a = 3. proof. by []. qed. end S1. + theory S2. op b : int = 4. lemma Lb : b = 4. proof. by []. qed. end S2. + theory P = S1 + S2. +end Outer. + +lemma test3 : Outer.P.a + Outer.P.b = 7. +proof. by rewrite Outer.P.La Outer.P.Lb. qed. + +(* the GFq pattern: alias inside an abstract theory, cloned with rename *) +abstract theory AT. + type t. + op v : t. + theory U1. op c : int = 5. lemma Lc : c = 5. proof. by []. qed. end U1. + theory U2. op d : int = 6. lemma Ld : d = 6. proof. by []. qed. end U2. + theory F = U1 + U2. +end AT. + +clone AT as ATI with type t <- int, op v <- 0 + rename "F" as "G". + +lemma test4 : ATI.G.c = 5. proof. by apply ATI.G.Lc. qed. +lemma test5 : ATI.G.d = 6. proof. by apply ATI.G.Ld. qed. From 7ae031cc3a28f337dfbe8ef67fc2b52a3d9ad724 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 19 Jul 2026 15:40:28 +0200 Subject: [PATCH 21/21] ZModP: restore the flat ZModpField namespace as a packed alias theory ZModpField = ZModpRing + ZModpFieldMx: the classical qualified names (ZModpField.mulrC, .mulVf, ...) resolve to the one ring object and the field mixin. Consumers that renamed or referenced the old bundled ZModpField (e.g. ML-KEM's GFq: rename "ZModpField" as "ZqField") work unchanged, without re-minting a duplicate field object. Statements are the targets': lemmas with a unit premise carry the ring's unit predicate (bridge with unitE where the old definitional reading was used). --- theories/algebra/ZModP.ec | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec index 752d7bb78..c1659f7f2 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -321,6 +321,11 @@ clone Ring.FieldBundle as ZModpFieldBd with theory R <= ZModpRing, theory F <= ZModpFieldMx. +(* the classical flat field namespace, as a packed alias: every member + resolves to the one ring object (ZModpRing) or to the field mixin + (ZModpFieldMx) -- no duplicated objects *) +theory ZModpField = ZModpRing + ZModpFieldMx. + (* -------------------------------------------------------------------- *) instance field with zmod op rzero = ZModField.zero