diff --git a/examples/SchnorrPK.ec b/examples/SchnorrPK.ec index 8110496083..ed9c3630e6 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 ef2bd6d935..750ae59690 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 f852e4bcbb..cb9055a894 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 2dd1e2204d..222b8d9725 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/src/ecCommands.ml b/src/ecCommands.ml index 3e08fb640d..7afa094639 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 62b8bf4afb..5a735e93a6 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 debf6ce401..b54104b1da 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 9552a74a1b..044529dabf 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 2a70a2e927..9abb35e5cf 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 3fd8316737..c274de77eb 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 8f0e27f872..00d31f99e5 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 d73ed66d7f..b1bc588b44 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 6dbf75ad42..c48da15036 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 e4e5125da6..4076d9d214 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 4305ad1571..7f51808923 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 380bc501db..35c016e85f 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 0000000000..799b74b80d --- /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. diff --git a/theories/algebra/CommAlgebra.ec b/theories/algebra/CommAlgebra.ec new file mode 100644 index 0000000000..c4df46ba70 --- /dev/null +++ b/theories/algebra/CommAlgebra.ec @@ -0,0 +1,1329 @@ +(* -------------------------------------------------------------------- *) +require import AllCore StdOrder Finite IntDiv IntMin List Ring Bigalg. +require (*--*) Ideal. +(* - *) import IntOrder. + +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. + +(* -------------------------------------------------------------------- *) +type 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 <= R. + +(* -------------------------------------------------------------------- *) +clone Ideal.Ideal as I with + type t <- t, + theory R <- R, + theory Dom <- Dom, + theory BigDom <- BR. + +(* -------------------------------------------------------------------- *) +abbrev (+) = I.idD. + +(* -------------------------------------------------------------------- *) +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. + +(* -------------------------------------------------------------------- *) +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. +- 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. +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 *) +(* 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. +- 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 /=. +- 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.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. + +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 R Dom 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 <> zeror => y <> zeror => 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 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. +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 := 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. + - 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 coprime_comax (x y : t) : coprime x y => comax x y. +proof. +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. +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 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_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_consT. +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_consT. +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. + 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_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). + - 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_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_consT /=. + apply/(mulrI (w * invr u) _). + - by apply/unitrM; split=> //; apply/unitrV. + 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. + - 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 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. +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 => /#. +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; apply: crt_comax => i j rgi rgj ne_ij. +by apply/coprime_comax/hcop. +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 /=. +- 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; apply: crt_uniq_comax => //. +move=> i j rgi rgj ne_ij; by apply/coprime_comax/hcop. +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. +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. + +end Euclidean. diff --git a/theories/algebra/Group.ec b/theories/algebra/Group.ec index f22be893fb..c770d35a13 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/Ideal.ec b/theories/algebra/Ideal.ec index f232a4a46b..3d8f640fe9 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 750e62e7a9..d3f30fd200 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). @@ -497,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 //=. @@ -559,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. @@ -670,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.(/) @@ -724,7 +743,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 +797,166 @@ 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_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. +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 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. + +(* -------------------------------------------------------------------- *) +(* 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 deg_mprod (rs : coeff list) : deg (mprod rs) = 1 + size rs. +proof. +elim: rs => [|r rs ih]; first by rewrite mprod_nil deg1. +rewrite mprod_cons degM_proper. +- 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 degXBC ih. +qed. + (* -------------------------------------------------------------------- *) lemma finite_for_poly_ledeg n p s : is_finite_for p s @@ -850,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. - -(* -------------------------------------------------------------------- *) -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]. + (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 *. (* -------------------------------------------------------------------- *) -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 - - 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). @@ -966,9 +1122,93 @@ 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 <> CR.zeror. +proof. +elim: rs => [|r rs ih] /=. +- 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 &(CoeffDom.mulf_neq0) -1:ih // subr_eq0. +qed. end Poly. + +(* ==================================================================== *) +abstract theory PolyField. +type coeff. + +clone import FieldBundle as K with type t <= coeff. + +clone include Poly with + type coeff <- coeff, + theory CR <- K.R, + theory CoeffDom <- K.F.Dom. + +import K.R K.F. +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 *) +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 = K.R.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' = K.R.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. diff --git a/theories/algebra/Ring.ec b/theories/algebra/Ring.ec index 41fd91356a..ec235ed707 100644 --- a/theories/algebra/Ring.ec +++ b/theories/algebra/Ring.ec @@ -858,6 +858,123 @@ 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. + +(* -------------------------------------------------------------------- *) +(* 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 df0e3127f9..c1659f7f29 100644 --- a/theories/algebra/ZModP.ec +++ b/theories/algebra/ZModP.ec @@ -302,48 +302,30 @@ 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 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. + +(* the field, as a single substitutable bundle *) +clone Ring.FieldBundle as ZModpFieldBd with + type t <= zmod, + 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 @@ -354,19 +336,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 : @@ -433,7 +415,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 e8c6830e4b..819bb2a534 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.