From e8fab6b839e19da231333ca8173bbb2a3d8a4033 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 11 Feb 2017 21:59:58 -0500 Subject: split the algebra library; use fsatz more --- src/Algebra/Field.v | 481 +++++++++++++++++++++++++++++++++++++++++++ src/Algebra/Group.v | 247 ++++++++++++++++++++++ src/Algebra/IntegralDomain.v | 155 ++++++++++++++ src/Algebra/Monoid.v | 60 ++++++ src/Algebra/Ring.v | 369 +++++++++++++++++++++++++++++++++ src/Algebra/ScalarMult.v | 90 ++++++++ src/Algebra/ZToRing.v | 150 -------------- 7 files changed, 1402 insertions(+), 150 deletions(-) create mode 100644 src/Algebra/Field.v create mode 100644 src/Algebra/Group.v create mode 100644 src/Algebra/IntegralDomain.v create mode 100644 src/Algebra/Monoid.v create mode 100644 src/Algebra/Ring.v create mode 100644 src/Algebra/ScalarMult.v delete mode 100644 src/Algebra/ZToRing.v (limited to 'src/Algebra') diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v new file mode 100644 index 000000000..ddd2737a3 --- /dev/null +++ b/src/Algebra/Field.v @@ -0,0 +1,481 @@ +Require Import Crypto.Util.Relations Crypto.Util.Tactics. +Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. +Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain. +Require Coq.setoid_ring.Field_theory. + +Section Field. + Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + + Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one. + Proof. + intros. rewrite commutative. auto using left_multiplicative_inverse. + Qed. + + Lemma left_inv_unique x ix : ix * x = one -> ix = inv x. + Proof. + intro Hix. + assert (ix*x*inv x = inv x). + - rewrite Hix, left_identity; reflexivity. + - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial. + intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix. + apply (zero_neq_one(eq:=eq)). assumption. + Qed. + Definition inv_unique := left_inv_unique. + + Lemma right_inv_unique x ix : x * ix = one -> ix = inv x. + Proof. rewrite commutative. apply left_inv_unique. Qed. + + Lemma div_one x : div x one = x. + Proof. + rewrite field_div_definition. + rewrite <-(inv_unique 1 1); apply monoid_is_right_identity. + Qed. + + Lemma mul_cancel_l_iff : forall x y, y <> 0 -> + (x * y = y <-> x = one). + Proof. + intros. + split; intros. + + rewrite <-(right_multiplicative_inverse y) by assumption. + rewrite <-H1 at 1; rewrite <-associative. + rewrite right_multiplicative_inverse by assumption. + rewrite right_identity. + reflexivity. + + rewrite H1; apply left_identity. + Qed. + + Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq. + Proof. + constructor. + { apply Ring.ring_theory_for_stdlib_tactic. } + { intro H01. symmetry in H01. auto using (zero_neq_one(eq:=eq)). } + { apply field_div_definition. } + { apply left_multiplicative_inverse. } + Qed. + + Context (eq_dec:DecidableRel eq). + + Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul. + Proof. + split. intros x y Hxy. + eapply not_not; try typeclasses eauto; []; intuition idtac; eapply (zero_neq_one(eq:=eq)). + transitivity ((inv y * (inv x * x)) * y). + - rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity. + - rewrite left_multiplicative_inverse, right_identity, left_multiplicative_inverse by trivial. + reflexivity. + Qed. + + Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul. + Proof. + split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero. + Qed. +End Field. + +Lemma isomorphism_to_subfield_field + {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} + {Equivalence_EQ: @Equivalence T EQ} + {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} + {Proper_INV:Proper(EQ==>EQ)INV} + {Proper_DIV:Proper(EQ==>EQ==>EQ)DIV} + {R eq zero one opp add sub mul inv div} {fieldR:@field R eq zero one opp add sub mul inv div} + {phi} + {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} + {neq_zero_one : (not (EQ ZERO ONE))} + {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_inv : forall a, eq (phi (INV a)) (inv (phi a))} + {phi_div : forall a b, eq (phi (DIV a b)) (div (phi a) (phi b))} + {phi_zero : eq (phi ZERO) zero} + {phi_one : eq (phi ONE) one} + : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV. +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, ?phi_inv, ?phi_div; + auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)), + (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)), + (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)), + (ring_sub_definition(sub:=sub)), field_div_definition. + apply left_multiplicative_inverse; rewrite <-phi_zero; auto. +Qed. + +Lemma Proper_ext : forall {A} (f g : A -> A) eq, Equivalence eq -> + (forall x, eq (g x) (f x)) -> Proper (eq==>eq) f -> Proper (eq==>eq) g. +Proof. + repeat intro. + transitivity (f x); auto. + transitivity (f y); auto. + symmetry; auto. +Qed. + +Lemma Proper_ext2 : forall {A} (f g : A -> A -> A) eq, Equivalence eq -> + (forall x y, eq (g x y) (f x y)) -> Proper (eq==>eq ==>eq) f -> Proper (eq==>eq==>eq) g. +Proof. + repeat intro. + transitivity (f x x0); auto. + transitivity (f y y0); match goal with H : Proper _ f |- _=> try apply H end; auto. + symmetry; auto. +Qed. + +Lemma equivalent_operations_field + {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} + {EQ_equivalence : Equivalence EQ} + {zero one opp add sub mul inv div} + {fieldR:@field T EQ zero one opp add sub mul inv div} + {EQ_opp : forall a, EQ (OPP a) (opp a)} + {EQ_inv : forall a, EQ (INV a) (inv a)} + {EQ_add : forall a b, EQ (ADD a b) (add a b)} + {EQ_sub : forall a b, EQ (SUB a b) (sub a b)} + {EQ_mul : forall a b, EQ (MUL a b) (mul a b)} + {EQ_div : forall a b, EQ (DIV a b) (div a b)} + {EQ_zero : EQ ZERO zero} + {EQ_one : EQ ONE one} + : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV. +Proof. + repeat (exact _||intro||split); rewrite_hyp ->?*; try reflexivity; + auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)), + (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)), + (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)), + (ring_sub_definition(sub:=sub)), field_div_definition; + try solve [(eapply Proper_ext2 || eapply Proper_ext); + eauto using group_inv_Proper, monoid_op_Proper, ring_mul_Proper, ring_sub_Proper, + field_inv_Proper, field_div_Proper]. + + apply left_multiplicative_inverse. + symmetry in EQ_zero. rewrite EQ_zero. assumption. + + eapply field_is_zero_neq_one; eauto; rewrite_hyp <-?*; reflexivity. +Qed. + +Section Homomorphism. + Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. + Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}. + Context {phi:F->K}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}. + + Lemma homomorphism_multiplicative_inverse + : forall x, not (EQ x ZERO) + -> phi (INV x) = inv (phi x). + Proof. + intros. + eapply inv_unique. + rewrite <-Ring.homomorphism_mul. + rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one. + Qed. + + Lemma homomorphism_multiplicative_inverse_complete + { EQ_dec : DecidableRel EQ } + : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x)) + -> phi (INV x) = inv (phi x). + Proof. + intros x ?; destruct (dec (EQ x ZERO)); auto using homomorphism_multiplicative_inverse. + Qed. + + Lemma homomorphism_div + : forall x y, not (EQ y ZERO) + -> phi (DIV x y) = div (phi x) (phi y). + Proof. + intros. rewrite !field_div_definition. + rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse; + (eauto || reflexivity). + Qed. + + Lemma homomorphism_div_complete + { EQ_dec : DecidableRel EQ } + : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y)) + -> phi (DIV x y) = div (phi x) (phi y). + Proof. + intros. rewrite !field_div_definition. + rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete; + (eauto || reflexivity). + Qed. +End Homomorphism. + +Section Homomorphism_rev. + Context {F EQ ZERO ONE OPP ADD SUB MUL INV DIV} {fieldF:@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. + 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)) + {phi'_inv : forall a, phi' (inv a) = INV (phi' a)} + (phi'_div : forall a b, phi' (div a b) = DIV (phi' a) (phi' b)). + + Lemma field_and_homomorphism_from_redundant_representation + : @field H eq zero one opp add sub mul inv div + /\ @Ring.is_homomorphism F EQ ONE ADD MUL H eq one add mul phi + /\ @Ring.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_multiplicative_inverse |- _ ] => 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'_inv, ?phi'_div, ?phi'_phi_id by reflexivity + | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id in H by reflexivity + | _ => solve [ eauto ] + end. + Qed. +End Homomorphism_rev. + +Ltac guess_field := + match goal with + | |- ?eq _ _ => constr:(_:Algebra.field (eq:=eq)) + | |- not (?eq _ _) => constr:(_:Algebra.field (eq:=eq)) + | [H: ?eq _ _ |- _ ] => constr:(_:Algebra.field (eq:=eq)) + | [H: not (?eq _ _) |- _] => constr:(_:Algebra.field (eq:=eq)) + end. + +Ltac goal_to_field_equality fld := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + match goal with + | [ |- eq _ _] => idtac + | [ |- not (eq ?x ?y) ] => apply not_exfalso; intro; goal_to_field_equality fld + | _ => exfalso; + match goal with + | H: not (eq _ _) |- _ => apply not_exfalso in H; apply H + | _ => apply (field_is_zero_neq_one(field:=fld)) + end + end. + +Ltac _introduce_inverse fld d d_nz := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in + let one := match type of fld with Algebra.field(one:=?one) => one end in + let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in + match goal with [H: eq (mul d _) one |- _ ] => fail 1 | _ => idtac end; + let d_i := fresh "i" in + unique pose proof (right_multiplicative_inverse(H:=fld) _ d_nz); + set (inv d) as d_i in *; + clearbody d_i. + +Ltac inequalities_to_inverse_equations fld := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let div := match type of fld with Algebra.field(div:=?div) => div end in + let sub := match type of fld with Algebra.field(sub:=?sub) => sub end in + repeat match goal with + | [H: not (eq _ _) |- _ ] => + lazymatch type of H with + | not (eq ?d zero) => _introduce_inverse fld d H + | not (eq zero ?d) => _introduce_inverse fld d (symmetry(R:=fun a b => not (eq a b)) H) + | not (eq ?x ?y) => _introduce_inverse fld (sub x y) (Ring.neq_sub_neq_zero _ _ H) + end + end. + +Ltac _nonzero_tac fld := + solve [trivial | IntegralDomain.solve_constant_nonzero | goal_to_field_equality fld; nsatz; IntegralDomain.solve_constant_nonzero]. + +Ltac _inverse_to_equation_by fld d tac := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let one := match type of fld with Algebra.field(one:=?one) => one end in + let mul := match type of fld with Algebra.field(mul:=?mul) => mul end in + let div := match type of fld with Algebra.field(div:=?div) => div end in + let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in + let d_nz := fresh "nz" in + assert (not (eq d zero)) as d_nz by tac; + lazymatch goal with + | H: eq (mul ?di d) one |- _ => rewrite <-!(left_inv_unique(H:=fld) _ _ H) in * + | H: eq (mul d ?di) one |- _ => rewrite <-!(right_inv_unique(H:=fld) _ _ H) in * + | _ => _introduce_inverse constr:(fld) constr:(d) d_nz + end; + clear d_nz. + +Ltac inverses_to_equations_by fld tac := + let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in + let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in + let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in + repeat match goal with + | |- context[inv ?d] => _inverse_to_equation_by fld d tac + | H: context[inv ?d] |- _ => _inverse_to_equation_by fld d tac + end. + +Ltac divisions_to_inverses fld := + rewrite ?(field_div_definition(field:=fld)) in *. + +Ltac fsatz := + let fld := guess_field in + goal_to_field_equality fld; + inequalities_to_inverse_equations fld; + divisions_to_inverses fld; + inverses_to_equations_by fld ltac:(solve_debugfail ltac:(_nonzero_tac fld)); + nsatz; + solve_debugfail ltac:(IntegralDomain.solve_constant_nonzero). + +Module _fsatz_test. + Section _test. + Context {F eq zero one opp add sub mul inv div} + {fld:@Algebra.field F eq zero one opp add sub mul inv div} + {eq_dec:DecidableRel eq}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + + Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. + Proof. fsatz. Qed. + + Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c). + Proof. fsatz. Qed. + + Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. + Proof. fsatz. Qed. + + Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c). + Proof. fsatz. Qed. + + Lemma zero_neq_one : 0 <> 1. + Proof. fsatz. Qed. + + Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False. + Proof. fsatz. Qed. + + Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False. + Proof. fsatz. Qed. + + Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1. + Proof. fsatz. Qed. + Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed. + Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed. + Import BinNums. + + Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}. + + Local Notation two := (one+one) (only parsing). + Local Notation three := (one+one+one) (only parsing). + Local Notation seven := (three+three+one) (only parsing). + Local Notation nine := (three+three+three) (only parsing). + + Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two). + Proof. fsatz. Qed. + + Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False. + Proof. fsatz. Qed. + End _test. +End _fsatz_test. + +Section ExtraLemmas. + Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}. + Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + + Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y. + Proof. intros; fsatz. Qed. + + Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. + Proof. intros; fsatz. Qed. + + Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False. + Proof. + intros; setoid_subst z; eauto using only_two_square_roots'. + Qed. + + Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y. + Proof. + intro H. + destruct (dec (eq x y)); [ left; assumption | right ]. + destruct (dec (eq x (opp y))); [ assumption | exfalso ]. + eapply only_two_square_roots'; eassumption. + Qed. + + Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y. + Proof. + intros; setoid_subst z; eauto using only_two_square_roots'_choice. + Qed. +End ExtraLemmas. + +(** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *) +Ltac pose_proof_only_two_square_roots x y H eq opp mul := + not constr_eq x y; + lazymatch x with + | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul + | _ + => lazymatch y with + | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul + | _ + => match goal with + | [ H' : eq x y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq x (opp y) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq y (opp x) |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp x) y |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (opp y) x |- _ ] + => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T + | [ H' : eq (mul x x) (mul y y) |- _ ] + => pose proof (only_two_square_roots'_choice x y H') as H + | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ] + => pose proof (only_two_square_roots_choice x y z H0 H1) as H + end + end + end. +Ltac reduce_only_two_square_roots x y eq opp mul := + let H := fresh in + pose_proof_only_two_square_roots x y H eq opp mul; + destruct H; + try setoid_subst y. +(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *) +Ltac post_clean_only_two_square_roots x y := + try (unfold not in *; + match goal with + | [ H : (?T -> False)%type, H' : ?T |- _ ] => exfalso; apply H; exact H' + | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity + end); + try setoid_subst x; try setoid_subst y. +Ltac only_two_square_roots_step eq opp mul := + match goal with + | [ H : not (eq ?x (opp ?y)) |- _ ] + (* this one comes first, because it the procedure is asymmetric + with respect to [x] and [y], and this order is more likely to + lead to solving goals by contradiction. *) + => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ] + => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y + end. +Ltac only_two_square_roots := + let fld := guess_field in + lazymatch type of fld with + | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => repeat only_two_square_roots_step eq opp mul + end. \ No newline at end of file diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v new file mode 100644 index 000000000..e4d38e243 --- /dev/null +++ b/src/Algebra/Group.v @@ -0,0 +1,247 @@ +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. + +Section BasicProperties. + Context {T eq op id inv} `{@group T eq op id inv}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "*" := op. + Local Infix "=" := eq : eq_scope. + Local Open Scope eq_scope. + + Lemma cancel_left : forall z x y, z*x = z*y <-> x = y. + Proof. eauto using Monoid.cancel_left, left_inverse. Qed. + Lemma cancel_right : forall z x y, x*z = y*z <-> x = y. + Proof. eauto using Monoid.cancel_right, right_inverse. Qed. + Lemma inv_inv x : inv(inv(x)) = x. + Proof. eauto using Monoid.inv_inv, left_inverse. Qed. + Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id. + Proof. eauto using Monoid.inv_op, left_inverse. Qed. + + Lemma inv_unique x ix : ix * x = id -> ix = inv x. + Proof. + intro Hix. + cut (ix*x*inv x = inv x). + - rewrite <-associative, right_inverse, right_identity; trivial. + - rewrite Hix, left_identity; reflexivity. + Qed. + + Lemma move_leftL x y : inv y * x = id -> x = y. + Proof. + intro; rewrite <- (inv_inv y), (inv_unique x (inv y)), inv_inv by assumption; reflexivity. + Qed. + + Lemma move_leftR x y : x * inv y = id -> x = y. + Proof. + intro; rewrite (inv_unique (inv y) x), inv_inv by assumption; reflexivity. + Qed. + + Lemma move_rightR x y : id = y * inv x -> x = y. + Proof. + intro; rewrite <- (inv_inv x), (inv_unique (inv x) y), inv_inv by (symmetry; assumption); reflexivity. + Qed. + + Lemma move_rightL x y : id = inv x * y -> x = y. + Proof. + intro; rewrite <- (inv_inv x), (inv_unique y (inv x)), inv_inv by (symmetry; assumption); reflexivity. + Qed. + + Lemma inv_op x y : inv (x*y) = inv y*inv x. + Proof. + symmetry. etransitivity. + 2:eapply inv_unique. + 2:eapply inv_op_ext. + reflexivity. + Qed. + + Lemma inv_id : inv id = id. + Proof. symmetry. eapply inv_unique, left_identity. Qed. + + Lemma inv_nonzero_nonzero : forall x, x <> id -> inv x <> id. + Proof. + intros ? Hx Ho. + assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity). + rewrite Ho, right_identity in Hxo. intuition. + Qed. + + Lemma neq_inv_nonzero : forall x, x <> inv x -> x <> id. + Proof. + intros ? Hx Hi; apply Hx. + rewrite Hi. + symmetry; apply inv_id. + Qed. + + Lemma inv_neq_nonzero : forall x, inv x <> x -> x <> id. + Proof. + intros ? Hx Hi; apply Hx. + rewrite Hi. + apply inv_id. + Qed. + + Lemma inv_zero_zero : forall x, inv x = id -> x = id. + Proof. + intros. + rewrite <-inv_id, <-H0. + symmetry; apply inv_inv. + Qed. + + Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c. + Proof. + split; intro Hx; rewrite Hx || rewrite <-Hx; + rewrite <-!associative, ?left_inverse, ?right_inverse, right_identity; + reflexivity. + Qed. + + Section ZeroNeqOne. + Context {one} `{is_zero_neq_one T eq id one}. + Lemma opp_one_neq_zero : inv one <> id. + Proof. apply inv_nonzero_nonzero, one_neq_zero. Qed. + Lemma zero_neq_opp_one : id <> inv one. + Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed. + End ZeroNeqOne. +End BasicProperties. + +Section Homomorphism. + Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}. + Context {H eq op id inv} {groupH:@group H eq op id inv}. + Context {phi:G->H}`{homom:@Monoid.is_homomorphism G EQ OP H eq op phi}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + + Lemma homomorphism_id : phi ID = id. + Proof. + assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by + (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity). + rewrite cancel_left in Hii; exact Hii. + Qed. + + Lemma homomorphism_inv x : phi (INV x) = inv (phi x). + Proof. + apply inv_unique. + rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. + Qed. + + Section ScalarMultHomomorphism. + Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }. + Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }. + Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P). + Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed. + + Import ScalarMult. + Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P). + Proof. + induction n; intros. + { rewrite !scalarmult_0_l, inv_id; reflexivity. } + { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. + rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. } + Qed. + End ScalarMultHomomorphism. +End Homomorphism. + +Section Homomorphism_rev. + Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}. + Context {H} {eq : H -> H -> Prop} {op : H -> H -> H} {id : H} {inv : H -> H}. + Context {phi:G->H} {phi':H->G}. + 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'_op : forall a b, phi' (op a b) = OP (phi' a) (phi' b)) + {phi'_inv : forall a, phi' (inv a) = INV (phi' a)} + {phi'_id : phi' id = ID}. + + Local Instance group_from_redundant_representation + : @group H eq op id inv. + Proof. + repeat match goal with + | [ H : group |- _ ] => destruct H; try clear H + | [ H : monoid |- _ ] => 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 _ _ |- _ ] => rewrite H + | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id by reflexivity + | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity + | _ => solve [ eauto ] + end. + Qed. + + Definition homomorphism_from_redundant_representation + : @Monoid.is_homomorphism G EQ OP H eq op phi. + Proof. + split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy. + Qed. +End Homomorphism_rev. + +Section GroupByHomomorphism. + Lemma surjective_homomorphism_from_group + {G EQ OP ID INV} {groupG:@group G EQ OP ID INV} + {H eq op id inv} + {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} } + {Proper_op:Proper(eq==>eq==>eq)op} + {Proper_inv:Proper(eq==>eq)inv} + {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph} + {surj:forall h, eq (phi (iph h)) h} + {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} + {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} + {phi_id : eq (phi ID) id} + : @group H eq op id inv. + Proof. + repeat split; eauto with core typeclass_instances; intros; + repeat match goal with + |- context[?x] => + match goal with + | |- context[iph x] => fail 1 + | _ => unify x id; fail 1 + | _ => is_var x; rewrite <- (surj x) + end + end; + repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id; + f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse. + Qed. + + Lemma isomorphism_to_subgroup_group + {G EQ OP ID INV} + {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } + {Proper_OP:Proper(EQ==>EQ==>EQ)OP} + {Proper_INV:Proper(EQ==>EQ)INV} + {H eq op id inv} {groupG:@group H eq op id inv} + {phi} + {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} + {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} + {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} + {phi_id : eq (phi ID) id} + : @group G EQ OP ID INV. + Proof. + repeat split; eauto with core typeclass_instances; intros; + eapply eq_phi_EQ; + repeat rewrite ?phi_op, ?phi_inv, ?phi_id; + auto using associative, left_identity, right_identity, left_inverse, right_inverse. + Qed. +End GroupByHomomorphism. + +Section HomomorphismComposition. + Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}. + Context {H eq op id inv} {groupH:@group H eq op id inv}. + Context {K eqK opK idK invK} {groupK:@group K eqK opK idK invK}. + Context {phi:G->H} {phi':H->K} + {Hphi:@Monoid.is_homomorphism G EQ OP H eq op phi} + {Hphi':@Monoid.is_homomorphism H eq op K eqK opK phi'}. + Lemma is_homomorphism_compose + {phi'':G->K} + (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x)) + : @Monoid.is_homomorphism G EQ OP K eqK opK phi''. + Proof. + split; repeat intro; rewrite <- !Hphi''. + { rewrite !Monoid.homomorphism; reflexivity. } + { apply Hphi', Hphi; assumption. } + Qed. + + Global Instance is_homomorphism_compose_refl + : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x)) + := is_homomorphism_compose (fun x => reflexivity _). +End HomomorphismComposition. \ No newline at end of file diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v new file mode 100644 index 000000000..96a4cf06b --- /dev/null +++ b/src/Algebra/IntegralDomain.v @@ -0,0 +1,155 @@ +Require Import Crypto.Util.Tactics. +Require Import Crypto.Algebra Crypto.Algebra.Ring. + +Module IntegralDomain. + Section IntegralDomain. + Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}. + + Lemma nonzero_product_iff_nonzero_factors : + forall x y : T, ~ eq (mul x y) zero <-> ~ eq x zero /\ ~ eq y zero. + Proof. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed. + + Global Instance Integral_domain : + @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops + Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring. + Proof. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed. + End IntegralDomain. + + Module _LargeCharacteristicReflective. + Section ReflectiveNsatzSideConditionProver. + Import BinInt BinNat BinPos. + Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted. + Context {R eq zero one opp add sub mul} + {ring:@Algebra.ring R eq zero one opp add sub mul} + {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. + + Inductive coef := + | Coef_one + | Coef_opp (_:coef) + | Coef_add (_ _:coef) + | Coef_mul (_ _:coef). + Fixpoint denote (c:coef) : R := + match c with + | Coef_one => one + | Coef_opp c => opp (denote c) + | Coef_add c1 c2 => add (denote c1) (denote c2) + | Coef_mul c1 c2 => mul (denote c1) (denote c2) + end. + Fixpoint CtoZ (c:coef) : Z := + match c with + | Coef_one => Z.one + | Coef_opp c => Z.opp (CtoZ c) + | Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2) + | Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2) + end. + Local Notation of_Z := (@Ring.of_Z R zero one opp add). + + Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c. + Proof. + induction c; simpl CtoZ; simpl denote; + repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity. + Qed. + + Section WithChar. + Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C). + Fixpoint is_nonzero (c:coef) : bool := + match c with + | Coef_opp c => is_nonzero c + | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2) + | _ => + match CtoZ c with + | Z0 => false + | Zpos p => N.leb (N.pos p) C + | Zneg p => N.leb (N.pos p) C + end + end. + Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. + Proof. + induction c; + repeat match goal with + | _ => progress unfold Algebra.char_gt, Ring.char_gt in * + | _ => progress (unfold is_nonzero in *; fold is_nonzero in * ) + | _ => progress change (denote (Coef_opp c)) with (opp (denote c)) in * + | _ => progress change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * + | _ => rewrite N.leb_le in * + | _ => rewrite <-Pos2Z.opp_pos in * + | H:@Logic.eq Z (CtoZ ?x) ?y |- _ => rewrite <-(CtoZ_correct x), H + | H: Logic.eq match ?x with _ => _ end true |- _ => destruct x eqn:? + | H:_ |- _ => unique pose proof (proj1 (Bool.andb_true_iff _ _) H) + | H:_/\_|- _ => unique pose proof (proj1 H) + | H:_/\_|- _ => unique pose proof (proj2 H) + | H: _ |- _ => unique pose proof (z_nonzero_correct _ H) + | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor + | |- opp _ <> zero => eapply Ring.opp_nonzero_nonzero + | _ => rewrite <-!Znat.N2Z.inj_pos + | |- _ => solve [eauto using N_one_le_pos | discriminate] + | _ => progress Ring.push_homomorphism constr:(of_Z) + end. + Qed. + End WithChar. + End ReflectiveNsatzSideConditionProver. + + Ltac reify one opp add mul x := + match x with + | one => constr:(Coef_one) + | opp ?a => + let a := reify one opp add mul a in + constr:(Coef_opp a) + | add ?a ?b => + let a := reify one opp add mul a in + let b := reify one opp add mul b in + constr:(Coef_add a b) + | mul ?a ?b => + let a := reify one opp add mul a in + let b := reify one opp add mul b in + constr:(Coef_mul a b) + end. + End _LargeCharacteristicReflective. + + Ltac solve_constant_nonzero := + match goal with (* TODO: change this match to a typeclass resolution *) + | |- not (?eq ?x _) => + let cg := constr:(_:Ring.char_gt (eq:=eq) _) in + match type of cg with + @Ring.char_gt ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C => + let x' := _LargeCharacteristicReflective.reify one opp add mul x in + let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in + change (not (eq x' zero)); + apply (_LargeCharacteristicReflective.is_nonzero_correct(eq:=eq)(zero:=zero) C cg); + abstract (vm_cast_no_check (eq_refl true)) + end + end. +End IntegralDomain. + +(** Tactics for polynomial equations over integral domains *) + +Require Coq.nsatz.Nsatz. + +Ltac dropAlgebraSyntax := + cbv beta delta [ + Algebra_syntax.zero + Algebra_syntax.one + Algebra_syntax.addition + Algebra_syntax.multiplication + Algebra_syntax.subtraction + Algebra_syntax.opposite + Algebra_syntax.equality + Algebra_syntax.bracket + Algebra_syntax.power + ] in *. + +Ltac dropRingSyntax := + dropAlgebraSyntax; + cbv beta delta [ + Ncring.zero_notation + Ncring.one_notation + Ncring.add_notation + Ncring.mul_notation + Ncring.sub_notation + Ncring.opp_notation + Ncring.eq_notation + ] in *. +Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax. diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v new file mode 100644 index 000000000..f71efff3e --- /dev/null +++ b/src/Algebra/Monoid.v @@ -0,0 +1,60 @@ +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Algebra. + +Section Monoid. + Context {T eq op id} {monoid:@monoid T eq op id}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "*" := op. + Local Infix "=" := eq : eq_scope. + Local Open Scope eq_scope. + + Lemma cancel_right z iz (Hinv:op z iz = id) : + forall x y, x * z = y * z <-> x = y. + Proof. + split; intros. + { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity). + rewrite <-associative in Hcut. + rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. } + { rewrite_hyp ->!*. reflexivity. } + Qed. + + Lemma cancel_left z iz (Hinv:op iz z = id) : + forall x y, z * x = z * y <-> x = y. + Proof. + split; intros. + { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity). + rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } + { rewrite_hyp ->!*; reflexivity. } + Qed. + + Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x. + Proof. + intros Hi Hii. + assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity). + rewrite associative, Hii, left_identity, right_identity in H; exact H. + Qed. + + Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id. + Proof. + intros Hx Hy. + cut (iy * (ix*x) * y = id); try intro H. + { rewrite <-!associative; rewrite <-!associative in H; exact H. } + rewrite Hx, right_identity, Hy. reflexivity. + Qed. + +End Monoid. + +Section Homomorphism. + Context {T EQ OP ID} {monoidT: @monoid T EQ OP ID }. + Context {T' eq op id} {monoidT': @monoid T' eq op id }. + Context {phi:T->T'}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Class is_homomorphism := + { + homomorphism : forall a b, phi (OP a b) = op (phi a) (phi b); + + is_homomorphism_phi_proper : Proper (respectful EQ eq) phi + }. + Global Existing Instance is_homomorphism_phi_proper. +End Homomorphism. \ No newline at end of file diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v new file mode 100644 index 000000000..2d8061ddc --- /dev/null +++ b/src/Algebra/Ring.v @@ -0,0 +1,369 @@ +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid. +Require Coq.ZArith.ZArith Coq.PArith.PArith. + +Section Ring. + Context {T eq zero one opp add sub mul} `{@ring T eq zero one opp add sub mul}. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. + + Lemma mul_0_l : forall x, 0 * x = 0. + Proof. + intros. + assert (0*x = 0*x) as Hx by reflexivity. + rewrite <-(right_identity 0), right_distributive in Hx at 1. + assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (rewrite Hx; reflexivity). + rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx. + Qed. + + Lemma mul_0_r : forall x, x * 0 = 0. + Proof. + intros. + assert (x*0 = x*0) as Hx by reflexivity. + rewrite <-(left_identity 0), left_distributive in Hx at 1. + assert (opp (x*0) + (x*0 + x*0) = opp (x*0) + x*0) as Hxx by (rewrite Hx; reflexivity). + rewrite associative, left_inverse, left_identity in Hxx; exact Hxx. + Qed. + + Lemma sub_0_l x : 0 - x = opp x. + Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed. + + Lemma mul_opp_r x y : x * opp y = opp (x * y). + Proof. + assert (Ho:x*(opp y) + x*y = 0) + by (rewrite <-left_distributive, left_inverse, mul_0_r; reflexivity). + rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. + rewrite <-!associative, right_inverse, right_identity; reflexivity. + Qed. + + Lemma mul_opp_l x y : opp x * y = opp (x * y). + Proof. + assert (Ho:opp x*y + x*y = 0) + by (rewrite <-right_distributive, left_inverse, mul_0_l; reflexivity). + rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. + rewrite <-!associative, right_inverse, right_identity; reflexivity. + Qed. + + Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero. + + Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul). + Proof. + split; intros. rewrite !ring_sub_definition, left_distributive. + eapply Group.cancel_left, mul_opp_r. + Qed. + + Global Instance is_right_distributive_sub : is_right_distributive (eq:=eq)(add:=sub)(mul:=mul). + Proof. + split; intros. rewrite !ring_sub_definition, right_distributive. + eapply Group.cancel_left, mul_opp_l. + Qed. + + Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0. + Proof. + intro Hsub. apply Hxy. rewrite <-(left_identity y), <-Hsub, ring_sub_definition. + rewrite <-associative, left_inverse, right_identity. reflexivity. + Qed. + + Lemma zero_product_iff_zero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} : + forall x y : T, eq (mul x y) zero <-> eq x zero \/ eq y zero. + Proof. + split; eauto using zero_product_zero_factor; []. + intros [Hz|Hz]; rewrite Hz; eauto using mul_0_l, mul_0_r. + Qed. + + Lemma nonzero_product_iff_nonzero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} : + forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)). + Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed. + + Lemma nonzero_hypothesis_to_goal {Hzpzf:@is_zero_product_zero_factor T eq zero mul} : + forall x y : T, (not (eq x zero) -> eq y zero) <-> (eq (mul x y) zero). + Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed. + + Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq. + Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops. + Proof. + split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances. + - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *) + eapply @left_identity; eauto with typeclass_instances. + - eapply @right_identity; eauto with typeclass_instances. + - eapply associative. + - intros; eapply right_distributive. + - intros; eapply left_distributive. + Qed. +End Ring. + +Section Homomorphism. + Context {R EQ ZERO ONE OPP ADD SUB MUL} `{@ring R EQ ZERO ONE OPP ADD SUB MUL}. + Context {S eq zero one opp add sub mul} `{@ring S eq zero one opp add sub mul}. + Context {phi:R->S}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + + Class is_homomorphism := + { + homomorphism_is_homomorphism : Monoid.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq); + homomorphism_mul : forall x y, phi (MUL x y) = mul (phi x) (phi y); + homomorphism_one : phi ONE = one + }. + Global Existing Instance homomorphism_is_homomorphism. + + Context `{phi_homom:is_homomorphism}. + + Lemma homomorphism_zero : phi ZERO = zero. + Proof. apply Group.homomorphism_id. Qed. + + Lemma homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y). + Proof. apply Monoid.homomorphism. Qed. + + Definition homomorphism_opp : forall x, phi (OPP x) = opp (phi x) := + (Group.homomorphism_inv (INV:=OPP) (inv:=opp)). + + Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y). + Proof. + intros. + rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity. + Qed. +End Homomorphism. + +Ltac push_homomorphism phi := + let H := constr:(_:is_homomorphism(phi:=phi)) in + repeat rewrite + ?(homomorphism_zero( phi_homom:=H)), + ?(homomorphism_one(is_homomorphism:=H)), + ?(homomorphism_add( phi_homom:=H)), + ?(homomorphism_opp( phi_homom:=H)), + ?(homomorphism_sub( phi_homom:=H)), + ?(homomorphism_mul(is_homomorphism:=H)). + +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 TacticSupportCommutative. + Context {T eq zero one opp add sub mul} `{@commutative_ring T eq zero one opp add sub mul}. + + Global Instance Cring_Cring_commutative_ring : + @Cring.Cring T zero one add mul sub opp eq Ncring_Ring_ops Ncring_Ring. + Proof. unfold Cring.Cring; intros; cbv. eapply commutative. Qed. + + Lemma ring_theory_for_stdlib_tactic : Ring_theory.ring_theory zero one add mul sub opp eq. + Proof. + constructor; intros. (* TODO(automation): make [auto] do this? *) + - apply left_identity. + - apply commutative. + - apply associative. + - apply left_identity. + - apply commutative. + - apply associative. + - apply right_distributive. + - apply ring_sub_definition. + - apply right_inverse. + Qed. +End TacticSupportCommutative. + +Section Z. + Import ZArith. + Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed. + + Global Instance commutative_ring_Z : @commutative_ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. eauto using @commutative_ring, @is_commutative, ring_Z with zarith. Qed. + + Global Instance integral_domain_Z : @integral_domain Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. + Proof. + split. + { apply commutative_ring_Z. } + { split. intros. eapply Z.eq_mul_0; assumption. } + { split. discriminate. } + Qed. +End Z. + +Section of_Z. + Import ZArith PArith. Local Open Scope Z_scope. + Context {R Req Rzero Rone Ropp Radd Rsub Rmul} + {Rring : @ring R Req Rzero Rone Ropp Radd Rsub Rmul}. + Local Infix "=" := Req. Local Infix "=" := Req : type_scope. + + Fixpoint of_nat (n:nat) : R := + match n with + | O => Rzero + | S n' => Radd (of_nat n') Rone + end. + Definition of_Z (x:Z) : R := + match x with + | Z0 => Rzero + | Zpos p => of_nat (Pos.to_nat p) + | Zneg p => Ropp (of_nat (Pos.to_nat p)) + end. + + Lemma of_Z_0 : of_Z 0 = Rzero. + Proof. reflexivity. Qed. + + Lemma of_nat_add x : + of_nat (Nat.add x 1) = Radd (of_nat x) Rone. + Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed. + + Lemma of_nat_sub x (H: (0 < x)%nat): + of_nat (Nat.sub x 1) = Rsub (of_nat x) Rone. + Proof. + induction x; [omega|simpl]. + rewrite <-of_nat_add. + rewrite Nat.sub_0_r, Nat.add_1_r. + simpl of_nat. + rewrite ring_sub_definition, <-associative. + rewrite right_inverse, right_identity. + reflexivity. + Qed. + + Lemma of_Z_add_1_r : + forall x, of_Z (Z.add x 1) = Radd (of_Z x) Rone. + Proof. + destruct x; [reflexivity| | ]; simpl of_Z. + { rewrite Pos2Nat.inj_add, of_nat_add. + reflexivity. } + { rewrite Z.pos_sub_spec; break_match; + match goal with + | H : _ |- _ => rewrite Pos.compare_eq_iff in H + | H : _ |- _ => rewrite Pos.compare_lt_iff in H + | H : _ |- _ => rewrite Pos.compare_gt_iff in H; + apply Pos.nlt_1_r in H; tauto + end; + subst; simpl of_Z; simpl of_nat. + { rewrite left_identity, left_inverse; reflexivity. } + { rewrite Pos2Nat.inj_sub by assumption. + rewrite of_nat_sub by apply Pos2Nat.is_pos. + rewrite ring_sub_definition, Group.inv_op, Group.inv_inv. + rewrite commutative; reflexivity. } } + Qed. + + Lemma of_Z_sub_1_r : + forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone. + Proof. + induction x. + { simpl; rewrite ring_sub_definition, !left_identity; + reflexivity. } + { case_eq (1 ?= p)%positive; intros; + match goal with + | H : _ |- _ => rewrite Pos.compare_eq_iff in H + | H : _ |- _ => rewrite Pos.compare_lt_iff in H + | H : _ |- _ => rewrite Pos.compare_gt_iff in H; + apply Pos.nlt_1_r in H; tauto + end. + { subst. simpl; rewrite ring_sub_definition, !left_identity, + right_inverse; reflexivity. } + { rewrite <-Pos2Z.inj_sub by assumption; simpl of_Z. + rewrite Pos2Nat.inj_sub by assumption. + rewrite of_nat_sub by apply Pos2Nat.is_pos. + reflexivity. } } + { simpl. rewrite Pos2Nat.inj_add, of_nat_add. + rewrite ring_sub_definition, Group.inv_op, commutative. + reflexivity. } + Qed. + + Lemma of_Z_opp : forall a, + of_Z (Z.opp a) = Ropp (of_Z a). + Proof. + destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv; + reflexivity. + Qed. + + Lemma of_Z_add : forall a b, + of_Z (Z.add a b) = Radd (of_Z a) (of_Z b). + Proof. + intros. + let x := match goal with |- ?x => x end in + let f := match (eval pattern b in x) with ?f _ => f end in + apply (Z.peano_ind f); intros. + { rewrite !right_identity. reflexivity. } + { replace (a + Z.succ x) with ((a + x) + 1) by ring. + replace (Z.succ x) with (x+1) by ring. + rewrite !of_Z_add_1_r, H. + rewrite associative; reflexivity. } + { replace (a + Z.pred x) with ((a+x)-1) + by (rewrite <-Z.sub_1_r; ring). + replace (Z.pred x) with (x-1) by apply Z.sub_1_r. + rewrite !of_Z_sub_1_r, H. + rewrite !ring_sub_definition. + rewrite associative; reflexivity. } + Qed. + + Lemma of_Z_mul : forall a b, + of_Z (Z.mul a b) = Rmul (of_Z a) (of_Z b). + Proof. + intros. + let x := match goal with |- ?x => x end in + let f := match (eval pattern b in x) with ?f _ => f end in + apply (Z.peano_ind f); intros until 0; try intro IHb. + { rewrite !mul_0_r; reflexivity. } + { rewrite Z.mul_succ_r, <-Z.add_1_r. + rewrite of_Z_add, of_Z_add_1_r. + rewrite IHb. + rewrite left_distributive, right_identity. + reflexivity. } + { rewrite Z.mul_pred_r, <-Z.sub_1_r. + rewrite of_Z_sub_1_r. + rewrite <-Z.add_opp_r. + rewrite of_Z_add, of_Z_opp. + rewrite IHb. + rewrite ring_sub_definition, left_distributive. + rewrite mul_opp_r,right_identity. + reflexivity. } + Qed. + + + Global Instance homomorphism_of_Z : + @is_homomorphism + Z Logic.eq Z.one Z.add Z.mul + R Req Rone Radd Rmul + of_Z. + Proof. + repeat constructor; intros. + { apply of_Z_add. } + { repeat intro; subst; reflexivity. } + { apply of_Z_mul. } + { simpl. rewrite left_identity; reflexivity. } + Qed. +End of_Z. + +Definition char_gt + {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R} + C := + @Algebra.char_gt R eq zero (fun n => (@of_Z R zero one opp add) (BinInt.Z.of_N n)) C. +Existing Class char_gt. + +(*** Tactics for ring equations *) +Require Export Coq.setoid_ring.Ring_tac. +Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t). + +Ltac ring_simplify_subterms_in_all := + reverse_nondep; ring_simplify_subterms; intros. + +Create HintDb ring_simplify discriminated. +Create HintDb ring_simplify_subterms discriminated. +Create HintDb ring_simplify_subterms_in_all discriminated. +Hint Extern 1 => progress ring_simplify : ring_simplify. +Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms. +Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all. \ No newline at end of file diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v new file mode 100644 index 000000000..33c236775 --- /dev/null +++ b/src/Algebra/ScalarMult.v @@ -0,0 +1,90 @@ +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Algebra Crypto.Algebra.Monoid. + +Module Import ModuloCoq8485. + Import NPeano Nat. + Infix "mod" := modulo. +End ModuloCoq8485. + +Section ScalarMultProperties. + Context {G eq add zero} `{monoidG:@monoid G eq add zero}. + Context {mul:nat->G->G}. + Local Infix "=" := eq : type_scope. Local Infix "=" := eq. + Local Infix "+" := add. Local Infix "*" := mul. + Class is_scalarmult := + { + scalarmult_0_l : forall P, 0 * P = zero; + scalarmult_S_l : forall n P, S n * P = P + n * P; + + scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul + }. + Global Existing Instance scalarmult_Proper. + Context `{mul_is_scalarmult:is_scalarmult}. + + Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := + match n with + | O => zero + | S n' => add P (scalarmult_ref n' P) + end. + + Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. + Proof. + repeat intro; subst. + match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. + repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + Qed. + + Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + Qed. + + Lemma scalarmult_1_l : forall P, 1*P = P. + Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. + + Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). + Proof. + induction n; intros; + rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + Qed. + + Lemma scalarmult_zero_r : forall m, m * zero = zero. + Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. + + Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. + Proof. + induction n; intros. + { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } + { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. + rewrite IHn. reflexivity. } + Qed. + + Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. + Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed. + + Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. + Proof. + intros ? ? Hnz Hmod ?. + rewrite (NPeano.Nat.div_mod n l Hnz) at 2. + rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. + Qed. +End ScalarMultProperties. + +Section ScalarMultHomomorphism. + Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}. + Context {H eq add zero} {monoidH:@monoid H eq add zero}. + Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope. + Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }. + Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }. + Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}. + Context (phi_ZERO:phi ZERO = zero). + + Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). + Proof. + setoid_rewrite scalarmult_ext. + induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. + Qed. +End ScalarMultHomomorphism. + +Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} + : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). +Proof. split; try exact _; intros; reflexivity. Qed. \ No newline at end of file diff --git a/src/Algebra/ZToRing.v b/src/Algebra/ZToRing.v deleted file mode 100644 index 0c423222e..000000000 --- a/src/Algebra/ZToRing.v +++ /dev/null @@ -1,150 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.PArith.PArith. -Require Import Crypto.Algebra. -Require Import Crypto.Util.Tactics. -Local Open Scope Z_scope. - -Section ZToRing. - Context {R Req Rzero Rone Ropp Radd Rsub Rmul} - {Rring : @ring R Req Rzero Rone Ropp Radd Rsub Rmul}. - Local Infix "=" := Req. Local Infix "=" := Req : type_scope. - - Fixpoint natToRing (n:nat) : R := - match n with - | O => Rzero - | S n' => Radd (natToRing n') Rone - end. - Definition ZToRing (x:Z) : R := - match x with - | Z0 => Rzero - | Zpos p => natToRing (Pos.to_nat p) - | Zneg p => Ropp (natToRing (Pos.to_nat p)) - end. - - Lemma ZToRing_zero_correct : ZToRing 0 = Rzero. - Proof. reflexivity. Qed. - - Lemma natToRing_plus_correct x : - natToRing (Nat.add x 1) = Radd (natToRing x) Rone. - Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed. - - Lemma natToRing_minus_correct x (H: (0 < x)%nat): - natToRing (Nat.sub x 1) = Rsub (natToRing x) Rone. - Proof. - induction x; [omega|simpl]. - rewrite <-natToRing_plus_correct. - rewrite Nat.sub_0_r, Nat.add_1_r. - simpl natToRing. - rewrite ring_sub_definition, <-associative. - rewrite right_inverse, right_identity. - reflexivity. - Qed. - - Lemma ZToRing_plus_correct : - forall x, ZToRing (Z.add x 1) = Radd (ZToRing x) Rone. - Proof. - destruct x; [reflexivity| | ]; simpl ZToRing. - { rewrite Pos2Nat.inj_add, natToRing_plus_correct. - reflexivity. } - { rewrite Z.pos_sub_spec; break_match; - match goal with - | H : _ |- _ => rewrite Pos.compare_eq_iff in H - | H : _ |- _ => rewrite Pos.compare_lt_iff in H - | H : _ |- _ => rewrite Pos.compare_gt_iff in H; - apply Pos.nlt_1_r in H; tauto - end; - subst; simpl ZToRing; simpl natToRing. - { rewrite left_identity, left_inverse; reflexivity. } - { rewrite Pos2Nat.inj_sub by assumption. - rewrite natToRing_minus_correct by apply Pos2Nat.is_pos. - rewrite ring_sub_definition, Group.inv_op, Group.inv_inv. - rewrite commutative; reflexivity. } } - Qed. - - Lemma ZToRing_minus_correct : - forall x, ZToRing (Z.sub x 1) = Rsub (ZToRing x) Rone. - Proof. - induction x. - { simpl; rewrite ring_sub_definition, !left_identity; - reflexivity. } - { case_eq (1 ?= p)%positive; intros; - match goal with - | H : _ |- _ => rewrite Pos.compare_eq_iff in H - | H : _ |- _ => rewrite Pos.compare_lt_iff in H - | H : _ |- _ => rewrite Pos.compare_gt_iff in H; - apply Pos.nlt_1_r in H; tauto - end. - { subst. simpl; rewrite ring_sub_definition, !left_identity, - right_inverse; reflexivity. } - { rewrite <-Pos2Z.inj_sub by assumption; simpl ZToRing. - rewrite Pos2Nat.inj_sub by assumption. - rewrite natToRing_minus_correct by apply Pos2Nat.is_pos. - reflexivity. } } - { simpl. rewrite Pos2Nat.inj_add, natToRing_plus_correct. - rewrite ring_sub_definition, Group.inv_op, commutative. - reflexivity. } - Qed. - - Lemma ZToRing_inj_opp : forall a, - ZToRing (Z.opp a) = Ropp (ZToRing a). - Proof. - destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv; - reflexivity. - Qed. - - Lemma ZToRing_inj_add : forall a b, - ZToRing (Z.add a b) = Radd (ZToRing a) (ZToRing b). - Proof. - intros. - let x := match goal with |- ?x => x end in - let f := match (eval pattern b in x) with ?f _ => f end in - apply (Z.peano_ind f); intros. - { rewrite !right_identity; reflexivity. } - { replace (a + Z.succ x) with ((a + x) + 1) by ring. - replace (Z.succ x) with (x+1) by ring. - rewrite !ZToRing_plus_correct, H. - rewrite associative; reflexivity. } - { replace (a + Z.pred x) with ((a+x)-1) - by (rewrite <-Z.sub_1_r; ring). - replace (Z.pred x) with (x-1) by apply Z.sub_1_r. - rewrite !ZToRing_minus_correct, H. - rewrite !ring_sub_definition. - rewrite associative; reflexivity. } - Qed. - - Lemma ZToRing_inj_mul : forall a b, - ZToRing (Z.mul a b) = Rmul (ZToRing a) (ZToRing b). - Proof. - intros. - let x := match goal with |- ?x => x end in - let f := match (eval pattern b in x) with ?f _ => f end in - apply (Z.peano_ind f); intros until 0; try intro IHb. - { rewrite !Ring.mul_0_r; reflexivity. } - { rewrite Z.mul_succ_r, <-Z.add_1_r. - rewrite ZToRing_inj_add, ZToRing_plus_correct. - rewrite IHb. - rewrite left_distributive, right_identity. - reflexivity. } - { rewrite Z.mul_pred_r, <-Z.sub_1_r. - rewrite ZToRing_minus_correct. - rewrite <-Z.add_opp_r. - rewrite ZToRing_inj_add, ZToRing_inj_opp. - rewrite IHb. - rewrite ring_sub_definition, left_distributive. - rewrite Ring.mul_opp_r,right_identity. - reflexivity. } - Qed. - - - Lemma ZToRingHomom : @Ring.is_homomorphism - Z Z.eq Z.one Z.add Z.mul - R Req Rone Radd Rmul - ZToRing. - Proof. - repeat constructor; intros. - { apply ZToRing_inj_add. } - { repeat intro. cbv [Z.eq] in *. subst. reflexivity. } - { apply ZToRing_inj_mul. } - { simpl. rewrite left_identity; reflexivity. } - Qed. -End ZToRing. -- cgit v1.2.3