diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-02-22 18:32:19 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | 40161086cdd8f0f04c1389f6ddad5d376f92138f (patch) | |
tree | 69bf08be5019c0baf0e50bc20a2e13b56140abf8 | |
parent | 2a321d84d1eceffbe35538c6f7fff2974e034e50 (diff) |
PrimeFieldTheorems: inv for isomorphic fields
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Algebra/Ring.v | 82 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 56 |
3 files changed, 110 insertions, 29 deletions
diff --git a/_CoqProject b/_CoqProject index 1e5bddeed..4b1b68cc9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -92,7 +92,6 @@ src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v -src/ModularArithmetic/Tutorial.v src/ModularArithmetic/ZBounded.v src/ModularArithmetic/ZBoundedZ.v src/ModularArithmetic/BarrettReduction/Z.v diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 640b12ed9..5c1cb1603 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -133,11 +133,15 @@ Section Homomorphism. intros. rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity. Qed. + + Global Instance monoid_homomorphism_mul : + Monoid.is_homomorphism (phi:=phi) (OP:=MUL) (op:=mul) (EQ:=EQ) (eq:=eq). + Proof. split; destruct phi_homom; assumption || exact _. Qed. End Homomorphism. (* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *) Ltac push_homomorphism phi := - let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in + let H := constr:(_ : @is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) as _push_homomrphism_0; pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) @@ -154,7 +158,7 @@ Ltac push_homomorphism phi := clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m. Ltac pull_homomorphism phi := - let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in + let H := constr:(_ : @is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H) as _pull_homomrphism_0; pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H) @@ -176,31 +180,55 @@ Ltac pull_homomorphism phi := (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m)); clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m. -Lemma isomorphism_to_subring_ring - {T EQ ZERO ONE OPP ADD SUB MUL} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } - {Proper_OPP:Proper(EQ==>EQ)OPP} - {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} - {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} - {Proper_MUL:Proper(EQ==>EQ==>EQ)MUL} - {R eq zero one opp add sub mul} {ringR:@ring R eq zero one opp add sub mul} - {phi} - {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} - {phi_opp : forall a, eq (phi (OPP a)) (opp (phi a))} - {phi_add : forall a b, eq (phi (ADD a b)) (add (phi a) (phi b))} - {phi_sub : forall a b, eq (phi (SUB a b)) (sub (phi a) (phi b))} - {phi_mul : forall a b, eq (phi (MUL a b)) (mul (phi a) (phi b))} - {phi_zero : eq (phi ZERO) zero} - {phi_one : eq (phi ONE) one} - : @ring T EQ ZERO ONE OPP ADD SUB MUL. -Proof. - repeat split; eauto with core typeclass_instances; intros; - eapply eq_phi_EQ; - repeat rewrite ?phi_opp, ?phi_add, ?phi_sub, ?phi_mul, ?phi_inv, ?phi_zero, ?phi_one; - auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)), - (associative (op := mul)), (commutative (op := add)), (left_identity (op := mul)), (right_identity (op := mul)), - left_inverse, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)), ring_sub_definition. -Qed. + +Section Isomorphism. + Context {F EQ ZERO ONE OPP ADD SUB MUL} {ringF:@ring F EQ ZERO ONE OPP ADD SUB MUL}. + Context {H} {eq : H -> H -> Prop} {zero one : H} {opp : H -> H} {add sub mul : H -> H -> H} {inv : H -> H} {div : H -> H -> H}. + Context {phi:F->H} {phi':H->F}. + Local Infix "=" := EQ. Local Infix "=" := EQ : type_scope. + Context (phi'_phi_id : forall A, phi' (phi A) = A) + (phi'_eq : forall a b, EQ (phi' a) (phi' b) <-> eq a b) + {phi'_zero : phi' zero = ZERO} + {phi'_one : phi' one = ONE} + {phi'_opp : forall a, phi' (opp a) = OPP (phi' a)} + (phi'_add : forall a b, phi' (add a b) = ADD (phi' a) (phi' b)) + (phi'_sub : forall a b, phi' (sub a b) = SUB (phi' a) (phi' b)) + (phi'_mul : forall a b, phi' (mul a b) = MUL (phi' a) (phi' b)). + + Lemma ring_by_isomorphism + : @ring H eq zero one opp add sub mul + /\ @is_homomorphism F EQ ONE ADD MUL H eq one add mul phi + /\ @is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'. + Proof. + repeat match goal with + | [ H : field |- _ ] => destruct H; try clear H + | [ H : commutative_ring |- _ ] => destruct H; try clear H + | [ H : ring |- _ ] => destruct H; try clear H + | [ H : abelian_group |- _ ] => destruct H; try clear H + | [ H : group |- _ ] => destruct H; try clear H + | [ H : monoid |- _ ] => destruct H; try clear H + | [ H : is_commutative |- _ ] => destruct H; try clear H + | [ H : is_left_distributive |- _ ] => destruct H; try clear H + | [ H : is_right_distributive |- _ ] => destruct H; try clear H + | [ H : is_zero_neq_one |- _ ] => destruct H; try clear H + | [ H : is_associative |- _ ] => destruct H; try clear H + | [ H : is_left_identity |- _ ] => destruct H; try clear H + | [ H : is_right_identity |- _ ] => destruct H; try clear H + | [ H : Equivalence _ |- _ ] => destruct H; try clear H + | [ H : is_left_inverse |- _ ] => destruct H; try clear H + | [ H : is_right_inverse |- _ ] => destruct H; try clear H + | _ => intro + | _ => split + | [ H : eq _ _ |- _ ] => apply phi'_eq in H + | [ |- eq _ _ ] => apply phi'_eq + | [ H : (~eq _ _)%type |- _ ] => pose proof (fun pf => H (proj1 (@phi'_eq _ _) pf)); clear H + | [ H : EQ _ _ |- _ ] => rewrite H + | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_phi_id by reflexivity + | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_phi_id in H by reflexivity + | _ => solve [ eauto ] + end. + Qed. +End Isomorphism. Section TacticSupportCommutative. Context {T eq zero one opp add sub mul} `{@commutative_ring T eq zero one opp add sub mul}. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 6f2970814..1e9b86552 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -237,4 +237,58 @@ Module F. } Qed. End SquareRootsPrime5Mod8. -End F. + + Module Iso. + Section IsomorphicRings. + Context {q:positive} {prime_q:prime q} {two_lt_q:2 < Z.pos q}. + Context + {H : Type} {eq : H -> H -> Prop} {zero one : H} + {opp : H -> H} {add sub mul : H -> H -> H} + {phi : F q -> H} {phi' : H -> F q} + {phi'_phi : forall A : F q, Logic.eq (phi' (phi A)) A} + {phi'_iff : forall a b : H, iff (Logic.eq (phi' a) (phi' b)) (eq a b)} + {phi'_zero : Logic.eq (phi' zero) F.zero} {phi'_one : Logic.eq (phi' one) F.one} + {phi'_opp : forall a : H, Logic.eq (phi' (opp a)) (F.opp (phi' a))} + {phi'_add : forall a b : H, Logic.eq (phi' (add a b)) (F.add (phi' a) (phi' b))} + {phi'_sub : forall a b : H, Logic.eq (phi' (sub a b)) (F.sub (phi' a) (phi' b))} + {phi'_mul : forall a b : H, Logic.eq (phi' (mul a b)) (F.mul (phi' a) (phi' b))} + {P:Type} {pow : H -> P -> H} {NtoP:N->P} + {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}. + Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)). + Definition div x y := mul (inv y) x. + + Lemma ring : + @Algebra.ring H eq zero one opp add sub mul + /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi + /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. + Proof. eapply @Ring.ring_by_isomorphism; assumption || exact _. Qed. + Local Instance _iso_ring : Algebra.ring := proj1 ring. + Local Instance _iso_hom1 : Ring.is_homomorphism := proj1 (proj2 ring). + Local Instance _iso_hom2 : Ring.is_homomorphism := proj2 (proj2 ring). + + Let inv_proof : forall a : H, phi' (inv a) = F.inv (phi' a). + Proof. + intros. + cbv [inv]. rewrite (Fq_inv_fermat(q:=q)(two_lt_q:=two_lt_q)). + rewrite <-Z_nat_N at 1 2. + rewrite (ScalarMult.homomorphism_scalarmult(phi:=phi')(MUL_is_scalarmult:=pow_is_scalarmult)(mul_is_scalarmult:=F.pow_is_scalarmult)). + reflexivity. + assumption. + Qed. + + Let div_proof : forall a b : H, phi' (mul (inv b) a) = phi' a / phi' b. + Proof. + intros. + rewrite phi'_mul, inv_proof, Algebra.field_div_definition, Algebra.commutative. + reflexivity. + Qed. + + Lemma field_and_iso : + @Algebra.field H eq zero one opp add sub mul inv div + /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi + /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. + Proof. eapply @Field.field_and_homomorphism_from_redundant_representation; + assumption || exact _ || exact inv_proof || exact div_proof. Qed. + End IsomorphicRings. + End Iso. +End F.
\ No newline at end of file |