From 4f614aef608c75da721b7154b2776967f731fa53 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 21 Aug 2024 11:37:01 +0200 Subject: [PATCH] stdlib: basic commutative algebra --- theories/algebra/CommAlgebra.ec | 775 ++++++++++++++++++++++++++++++++ 1 file changed, 775 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 0000000000..1f4d0d90cc --- /dev/null +++ b/theories/algebra/CommAlgebra.ec @@ -0,0 +1,775 @@ +(* -------------------------------------------------------------------- *) +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 apply: map_inj_in_uniq => //#. + - 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. 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.