diff options
26 files changed, 1579 insertions, 2187 deletions
diff --git a/_CoqProject b/_CoqProject index 820d1b0e4..b50e07652 100644 --- a/_CoqProject +++ b/_CoqProject @@ -10,7 +10,12 @@ src/Karatsuba.v src/MxDHRepChange.v src/NewBaseSystem.v src/Testbit.v -src/Algebra/ZToRing.v +src/Algebra/Field.v +src/Algebra/Group.v +src/Algebra/IntegralDomain.v +src/Algebra/Monoid.v +src/Algebra/Ring.v +src/Algebra/ScalarMult.v src/Assembly/Bounds.v src/Assembly/Compile.v src/Assembly/Conversions.v @@ -68,7 +73,6 @@ src/Experiments/Ed25519.v src/Experiments/Ed25519Extraction.v src/Experiments/ExtrHaskellNats.v src/Experiments/GenericFieldPow.v -src/Experiments/MontgomeryCurve.v src/ModularArithmetic/Conversion.v src/ModularArithmetic/ExtPow2BaseMulProofs.v src/ModularArithmetic/ExtendedBaseVector.v @@ -179,6 +183,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v +src/Spec/MontgomeryCurve.v src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v diff --git a/src/Algebra.v b/src/Algebra.v index 5a32989e0..b0f48ac4d 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -11,11 +11,6 @@ Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. -Module Import ModuloCoq8485. - Import NPeano Nat. - Infix "mod" := modulo. -End ModuloCoq8485. - Section Algebra. Context {T:Type} {eq:T->T->Prop}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. @@ -146,6 +141,9 @@ Section Algebra. Global Existing Instance field_inv_Proper. Global Existing Instance field_div_Proper. End AddMul. + + Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinNums.N->T) C := forall n, BinNat.N.le BinNat.N.one n -> BinNat.N.le n C -> not (eq (inj n) zero). + Existing Class char_gt. End Algebra. Section ZeroNeqOne. @@ -155,1544 +153,4 @@ Section ZeroNeqOne. Proof. intro HH; symmetry in HH. auto using zero_neq_one. Qed. -End ZeroNeqOne. - -Module Monoid. - 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 (f_equiv; assumption). - rewrite <-associative in Hcut. - rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. } - { f_equiv; assumption. } - 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 (f_equiv; assumption). - rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } - { f_equiv; assumption. } - 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. -End Monoid. - -Module ScalarMult. - 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. -End ScalarMult. - -Module Group. - 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, Group.inv_id; reflexivity. } - { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. - rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.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. -End Group. - -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 *. - -Module Ring. - 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 (f_equiv; exact Hx). - 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 (f_equiv; exact Hx). - 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; dropRingSyntax; 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 `{is_homomorphism}. - - 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. - - 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 Ring.Ncring_Ring_ops Ring.Ncring_Ring. - Proof. unfold Cring.Cring; intros; dropRingSyntax. 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. -End 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; dropRingSyntax; eauto using zero_product_zero_factor, one_neq_zero. Qed. - End IntegralDomain. -End IntegralDomain. - -Require Coq.setoid_ring.Field_theory. -Module Field. - 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. 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. } - { 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. - 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, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)), - ring_sub_definition, 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 split; eauto with core typeclass_instances; intros; - repeat rewrite ?EQ_opp, ?EQ_inv, ?EQ_add, ?EQ_sub, ?EQ_mul, ?EQ_div, ?EQ_zero, ?EQ_one; - 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, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)), - ring_sub_definition, 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. - 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. -End Field. - -(** Tactics *) - -Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax. -Ltac nsatz_contradict := Algebra_syntax.Nsatz.nsatz_contradict; dropRingSyntax. - -(*** Tactics for manipulating field equations *) -Require Import Coq.setoid_ring.Field_tac. - -(** Convention: These tactics put the original goal first, and all - goals for non-zero side-conditions after that. (Exception: - [field_simplify_eq in], which is silly. *) - -Ltac guess_field := - match goal with - | |- ?eq _ _ => constr:(_:field (eq:=eq)) - | |- not (?eq _ _) => constr:(_:field (eq:=eq)) - | [H: ?eq _ _ |- _ ] => constr:(_:field (eq:=eq)) - | [H: not (?eq _ _) |- _] => constr:(_:field (eq:=eq)) - end. - -Ltac field_nonzero_mul_split := - repeat match goal with - | [ H : ?R (?mul ?x ?y) ?zero |- _ ] - => apply zero_product_zero_factor in H; destruct H - | [ |- not (?R (?mul ?x ?y) ?zero) ] - => apply IntegralDomain.nonzero_product_iff_nonzero_factors; split - | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ] - => apply IntegralDomain.nonzero_product_iff_nonzero_factors in H; destruct H - end. - -Ltac field_simplify_eq_if_div := - let fld := guess_field in - lazymatch type of fld with - field (div:=?div) => - lazymatch goal with - | |- appcontext[div] => field_simplify_eq - | |- _ => idtac - end - end. - -(** We jump through some hoops to ensure that the side-conditions come late *) -Ltac field_simplify_eq_if_div_in_cycled_side_condition_order H := - let fld := guess_field in - lazymatch type of fld with - field (div:=?div) => - lazymatch type of H with - | appcontext[div] => field_simplify_eq in H - | _ => idtac - end - end. - -Ltac field_simplify_eq_if_div_in H := - side_conditions_before_to_side_conditions_after - field_simplify_eq_if_div_in_cycled_side_condition_order - H. - -(** Now we have more conservative versions that don't simplify non-division structure. *) -Ltac deduplicate_nonfraction_pieces mul := - repeat match goal with - | [ x0 := ?v, x1 := context[?v] |- _ ] - => progress change v with x0 in x1 - | [ x := mul ?a ?b |- _ ] - => not is_var a; - let a' := fresh x in - pose a as a'; change a with a' in x - | [ x := mul ?a ?b |- _ ] - => not is_var b; - let b' := fresh x in - pose b as b'; change b with b' in x - | [ x0 := ?v, x1 := ?v |- _ ] - => change x1 with x0 in *; clear x1 - | [ x := ?v |- _ ] - => is_var v; subst x - | [ x0 := mul ?a ?b, x1 := mul ?a ?b' |- _ ] - => subst x0 x1 - | [ x0 := mul ?a ?b, x1 := mul ?a' ?b |- _ ] - => subst x0 x1 - end. - -Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div cont := - idtac; - let one_arg_recr := - fun op v - => set_nonfraction_pieces_on - v eq zero opp add sub mul inv div - ltac:(fun x => cont (op x)) in - let two_arg_recr := - fun op v0 v1 - => set_nonfraction_pieces_on - v0 eq zero opp add sub mul inv div - ltac:(fun x - => - set_nonfraction_pieces_on - v1 eq zero opp add sub mul inv div - ltac:(fun y => cont (op x y))) in - lazymatch T with - | eq ?x ?y => two_arg_recr eq x y - | appcontext[div] - => lazymatch T with - | opp ?x => one_arg_recr opp x - | inv ?x => one_arg_recr inv x - | add ?x ?y => two_arg_recr add x y - | sub ?x ?y => two_arg_recr sub x y - | mul ?x ?y => two_arg_recr mul x y - | div ?x ?y => two_arg_recr div x y - | _ => idtac - end - | _ => let x := fresh "x" in - pose T as x; - cont x - end. -Ltac set_nonfraction_pieces_in H := - idtac; - let fld := guess_field in - lazymatch type of fld with - | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => let T := type of H in - set_nonfraction_pieces_on - T eq zero opp add sub mul inv div - ltac:(fun T' => change T' in H); - deduplicate_nonfraction_pieces mul - end. -Ltac set_nonfraction_pieces := - idtac; - let fld := guess_field in - lazymatch type of fld with - | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => let T := get_goal in - set_nonfraction_pieces_on - T eq zero opp add sub mul inv div - ltac:(fun T' => change T'); - deduplicate_nonfraction_pieces mul - end. -Ltac default_common_denominator_nonzero_tac := - repeat apply conj; - try first [ assumption - | intro; field_nonzero_mul_split; tauto ]. -Ltac common_denominator_in H := - idtac; - let fld := guess_field in - let div := lazymatch type of fld with - | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => div - end in - lazymatch type of H with - | appcontext[div] - => set_nonfraction_pieces_in H; - field_simplify_eq_if_div_in H; - [ - | default_common_denominator_nonzero_tac.. ]; - repeat match goal with H := _ |- _ => subst H end - | ?T => fail 0 "no division in" H ":" T - end. -Ltac common_denominator := - idtac; - let fld := guess_field in - let div := lazymatch type of fld with - | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => div - end in - lazymatch goal with - | |- appcontext[div] - => set_nonfraction_pieces; - field_simplify_eq_if_div; - [ - | default_common_denominator_nonzero_tac.. ]; - repeat match goal with H := _ |- _ => subst H end - | |- ?G - => fail 0 "no division in goal" G - end. -Ltac common_denominator_inequality_in H := - let HT := type of H in - lazymatch HT with - | not (?R _ _) => idtac - | (?R _ _ -> False)%type => idtac - | _ => fail 0 "Not an inequality" H ":" HT - end; - let HTT := type of HT in - let HT' := fresh in - evar (HT' : HTT); - let H' := fresh in - rename H into H'; - cut (not HT'); subst HT'; - [ intro H; clear H' - | let H'' := fresh in - intro H''; apply H'; common_denominator; [ eexact H'' | .. ] ]. -Ltac common_denominator_inequality := - let G := get_goal in - lazymatch G with - | not (?R _ _) => idtac - | (?R _ _ -> False)%type => idtac - | _ => fail 0 "Not an inequality (goal):" G - end; - let GT := type of G in - let HT' := fresh in - evar (HT' : GT); - let H' := fresh in - assert (H' : not HT'); subst HT'; - [ - | let HG := fresh in - intros HG; apply H'; common_denominator_in HG; [ eexact HG | .. ] ]. - -Ltac common_denominator_hyps := - try match goal with - | [H: _ |- _ ] - => progress common_denominator_in H; - [ common_denominator_hyps - | .. ] - end. - -Ltac common_denominator_inequality_hyps := - try match goal with - | [H: _ |- _ ] - => progress common_denominator_inequality_in H; - [ common_denominator_inequality_hyps - | .. ] - end. - -Ltac common_denominator_all := - try common_denominator; - [ try common_denominator_hyps - | .. ]. - -Ltac common_denominator_inequality_all := - try common_denominator_inequality; - [ try common_denominator_inequality_hyps - | .. ]. - -Ltac common_denominator_equality_inequality_all := - common_denominator_all; - [ common_denominator_inequality_all - | .. ]. - -(** [nsatz] for fields *) -Ltac _field_nsatz_prep_goal fld eq := - repeat match goal with - | [ |- not (eq ?x ?y) ] => intro - | [ |- eq _ _] => idtac - | _ => exfalso; apply (field_is_zero_neq_one(field:=fld)) - end. - -Ltac _field_nsatz_prep_inequalities fld eq zero := - repeat match goal with - | [H: not (eq _ _) |- _ ] => - lazymatch type of H with - | not (eq _ zero) => unique pose proof (Field.right_multiplicative_inverse(H:=fld) _ H) - | not (eq zero _) => unique pose proof (Field.right_multiplicative_inverse(H:=fld) _ (symmetry _ _ H)) - | _ => unique pose proof (Field.right_multiplicative_inverse(H:=fld) _ (Ring.neq_sub_neq_zero _ _ H)) - end - end. - -(* solves all implications between field equalities and field inequalities that are true in all fields (including those without decidable equality) *) -Ltac field_nsatz := - let fld := guess_field in - let eq := match type of fld with field(eq:=?eq) => eq end in - let zero := match type of fld with field(zero:=?zero) => zero end in - _field_nsatz_prep_goal fld eq; - common_denominator_equality_inequality_all; [|_field_nsatz_prep_goal fld eq..]; - _field_nsatz_prep_inequalities fld eq zero; - nsatz; - repeat eapply (proj2 (Ring.nonzero_product_iff_nonzero_factor _ _)); auto. (* nsatz coefficients *) - -Inductive field_simplify_done {T} : T -> Type := - Field_simplify_done : forall H, field_simplify_done H. - -Ltac field_simplify_eq_hyps := - repeat match goal with - [ H: _ |- _ ] => - match goal with - | [ Ha : field_simplify_done H |- _ ] => fail - | _ => idtac - end; - field_simplify_eq in H; - unique pose proof (Field_simplify_done H) - end; - repeat match goal with [ H: field_simplify_done _ |- _] => clear H end. - -Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq. - -(** *** Tactics that remove division by rewriting *) -Ltac rewrite_field_div_definition inv := - let lem := constr:(field_div_definition (inv:=inv)) in - let div := lazymatch lem with field_div_definition (div:=?div) => div end in - repeat match goal with - | [ |- context[div _ _] ] => rewrite !lem - | [ H : context[div _ _] |- _ ] => rewrite !lem in H - end. -Ltac generalize_inv inv := - let lem := constr:(left_multiplicative_inverse (inv:=inv)) in - repeat match goal with - | [ |- context[inv ?x] ] - => pose proof (lem x); generalize dependent (inv x); intros - | [ H : context[inv ?x] |- _ ] - => pose proof (lem x); generalize dependent (inv x); intros - end. -Ltac nsatz_strip_fractions_on inv := - rewrite_field_div_definition inv; generalize_inv inv; specialize_by_assumption. - -Ltac nsatz_strip_fractions_with_eq eq := - let F := constr:(_ : field (eq:=eq)) in - lazymatch type of F with - | field (inv:=?inv) => nsatz_strip_fractions_on inv - end. -Ltac nsatz_strip_fractions := - match goal with - | [ |- ?eq ?x ?y ] => nsatz_strip_fractions_with_eq eq - | [ |- not (?eq ?x ?y) ] => nsatz_strip_fractions_with_eq eq - | [ |- (?eq ?x ?y -> False)%type ] => nsatz_strip_fractions_with_eq eq - | [ H : ?eq ?x ?y |- _ ] => nsatz_strip_fractions_with_eq eq - | [ H : not (?eq ?x ?y) |- _ ] => nsatz_strip_fractions_with_eq eq - | [ H : (?eq ?x ?y -> False)%type |- _ ] => nsatz_strip_fractions_with_eq eq - end. - -Ltac nsatz_fold_or_intro_not := - repeat match goal with - | [ |- not _ ] => intro - | [ |- (_ -> _)%type ] => intro - | [ H : (?X -> False)%type |- _ ] - => change (not X) in H - | [ H : ((?X -> False) -> ?T)%type |- _ ] - => change (not X -> T)%type in H - end. - -Ltac nsatz_final_inequality_to_goal := - nsatz_fold_or_intro_not; - try match goal with - | [ H : not (?eq ?x ?zero) |- ?eq ?y ?zero ] - => generalize H; apply (proj2 (Ring.nonzero_hypothesis_to_goal x y)) - | [ H : not (?eq ?x ?zero) |- False ] - => apply H - end. - -Ltac nsatz_goal_to_canonical := - nsatz_fold_or_intro_not; - try match goal with - | [ |- ?eq ?x ?y ] - => apply (Group.move_leftR (eq:=eq)); rewrite <- ring_sub_definition; - lazymatch goal with - | [ |- eq _ y ] => fail 0 "should not subtract 0" - | _ => idtac - end - end. - -Ltac nsatz_specialize_by_cut_using cont H eq x zero a b := - change (not (eq x zero) -> eq a b)%type in H; - cut (not (eq x zero)); - [ intro; specialize_by_assumption; cont () - | clear H ]. - -Ltac nsatz_specialize_by_cut := - specialize_by_assumption; - match goal with - | [ H : ((?eq ?x ?zero -> False) -> ?eq ?a ?b)%type |- ?eq _ ?zero ] - => nsatz_specialize_by_cut_using ltac:(fun _ => nsatz_specialize_by_cut) H eq x zero a b - | [ H : (not (?eq ?x ?zero) -> ?eq ?a ?b)%type |- ?eq _ ?zero ] - => nsatz_specialize_by_cut_using ltac:(fun _ => nsatz_specialize_by_cut) H eq x zero a b - | [ H : ((?eq ?x ?zero -> False) -> ?eq ?a ?b)%type |- False ] - => nsatz_specialize_by_cut_using ltac:(fun _ => nsatz_specialize_by_cut) H eq x zero a b - | [ H : (not (?eq ?x ?zero) -> ?eq ?a ?b)%type |- False ] - => nsatz_specialize_by_cut_using ltac:(fun _ => nsatz_specialize_by_cut) H eq x zero a b - | _ => idtac - end. - -(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R], and similarly for symmetric relations *) -Ltac clear_algebraic_duplicates_step R := - match goal with - | [ H : R ?x ?x |- _ ] - => clear H - end. -Ltac clear_algebraic_duplicates_step_S R := - match goal with - | [ H : R ?x ?y, H' : R ?y ?x |- _ ] - => clear H - | [ H : not (R ?x ?y), H' : not (R ?y ?x) |- _ ] - => clear H - | [ H : (R ?x ?y -> False)%type, H' : (R ?y ?x -> False)%type |- _ ] - => clear H - | [ H : not (R ?x ?y), H' : (R ?y ?x -> False)%type |- _ ] - => clear H - end. -Ltac clear_algebraic_duplicates_guarded R := - let test_reflexive := constr:(_ : Reflexive R) in - repeat clear_algebraic_duplicates_step R. -Ltac clear_algebraic_duplicates_guarded_S R := - let test_symmetric := constr:(_ : Symmetric R) in - repeat clear_algebraic_duplicates_step_S R. -Ltac clear_algebraic_duplicates := - clear_duplicates; - repeat match goal with - | [ H : ?R ?x ?x |- _ ] => progress clear_algebraic_duplicates_guarded R - | [ H : ?R ?x ?y, H' : ?R ?y ?x |- _ ] - => progress clear_algebraic_duplicates_guarded_S R - | [ H : not (?R ?x ?y), H' : not (?R ?y ?x) |- _ ] - => progress clear_algebraic_duplicates_guarded_S R - | [ H : not (?R ?x ?y), H' : (?R ?y ?x -> False)%type |- _ ] - => progress clear_algebraic_duplicates_guarded_S R - | [ H : (?R ?x ?y -> False)%type, H' : (?R ?y ?x -> False)%type |- _ ] - => progress clear_algebraic_duplicates_guarded_S R - end. - -(*** Inequalities over fields *) -Ltac assert_expr_by_nsatz H ty := - let H' := fresh in - rename H into H'; assert (H : ty) - by (try (intro; apply H'); nsatz); - clear H'. -Ltac test_not_constr_eq_assert_expr_by_nsatz y zero H ty := - first [ constr_eq y zero; fail 1 y "is already" zero - | assert_expr_by_nsatz H ty ]. -Ltac canonicalize_field_inequalities_step' eq zero opp add sub := - match goal with - | [ H : not (eq ?x (opp ?y)) |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (add x y) zero)) - | [ H : (eq ?x (opp ?y) -> False)%type |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (add x y) zero -> False)%type - | [ H : not (eq ?x ?y) |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (sub x y) zero)) - | [ H : (eq ?x ?y -> False)%type |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (not (eq (sub x y) zero)) - end. -Ltac canonicalize_field_inequalities' eq zero opp add sub := repeat canonicalize_field_inequalities_step' eq zero opp add sub. -Ltac canonicalize_field_equalities_step' eq zero opp add sub := - lazymatch goal with - | [ H : eq ?x (opp ?y) |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (add x y) zero) - | [ H : eq ?x ?y |- _ ] - => test_not_constr_eq_assert_expr_by_nsatz y zero H (eq (sub x y) zero) - end. -Ltac canonicalize_field_equalities' eq zero opp add sub := repeat canonicalize_field_equalities_step' eq zero opp add sub. - -(** These are the two user-facing tactics. They put (in)equalities - into the form [_ <> 0] / [_ = 0]. *) -Ltac canonicalize_field_inequalities := - let fld := guess_field in - lazymatch type of fld with - | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => canonicalize_field_inequalities' eq zero opp add sub - end. -Ltac canonicalize_field_equalities := - let fld := guess_field in - lazymatch type of fld with - | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => canonicalize_field_equalities' eq zero opp add sub - end. - - -(*** Polynomial equations over fields *) - -Ltac neq01 := - try solve - [apply zero_neq_one - |apply Group.zero_neq_opp_one - |apply one_neq_zero - |apply Group.opp_one_neq_zero]. - -Ltac combine_field_inequalities_step := - match goal with - | [ H : not (?R ?x ?zero), H' : not (?R ?x' ?zero) |- _ ] - => pose proof (proj2 (IntegralDomain.nonzero_product_iff_nonzero_factors x x') (conj H H')); clear H H' - | [ H : (?X -> False)%type |- _ ] - => change (not X) in H - end. - -(** First we split apart the equalities so that we can clear - duplicates; it's easier for us to do this than to give [nsatz] the - extra work. *) - -Ltac split_field_inequalities_step := - match goal with - | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ] - => apply IntegralDomain.nonzero_product_iff_nonzero_factors in H; destruct H - end. -Ltac split_field_inequalities := - canonicalize_field_inequalities; - repeat split_field_inequalities_step; - clear_duplicates. - -Ltac combine_field_inequalities := - split_field_inequalities; - repeat combine_field_inequalities_step. -(** Handles field inequalities which can be made by splitting multiplications in the goal and the assumptions *) -Ltac solve_simple_field_inequalities := - repeat (apply conj || split_field_inequalities); - try assumption. -Ltac nsatz_strip_fractions_and_aggregate_inequalities := - nsatz_strip_fractions; - nsatz_goal_to_canonical; - split_field_inequalities (* this will make solving side conditions easier *); - nsatz_specialize_by_cut; - [ combine_field_inequalities; nsatz_final_inequality_to_goal | .. ]. -Ltac prensatz_contradict := - solve_simple_field_inequalities; - combine_field_inequalities. -Ltac nsatz_inequality_to_equality := - repeat intro; - match goal with - | [ H : not (?R ?x ?zero) |- False ] => apply H - | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H - end. -(** Clean up tactic handling side-conditions *) -Ltac super_nsatz_post_clean_inequalities := - repeat (apply conj || split_field_inequalities); - try assumption; - prensatz_contradict; nsatz_inequality_to_equality; - try nsatz. -Ltac nsatz_equality_to_inequality_by_decide_equality := - lazymatch goal with - | [ H : not (?R _ _) |- ?R _ _ ] => idtac - | [ H : (?R _ _ -> False)%type |- ?R _ _ ] => idtac - | [ |- ?R _ _ ] => fail 0 "No hypothesis exists which negates the relation" R - | [ |- ?G ] => fail 0 "The goal is not a binary relation:" G - end; - lazymatch goal with - | [ |- ?R ?x ?y ] - => destruct (@dec (R x y) _); [ assumption | exfalso ] - end. -(** Handles inequalities and fractions *) -Ltac super_nsatz_internal nsatz_alternative := - (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) - clear_algebraic_duplicates; - prensatz_contradict; - (* Each goal left over by [prensatz_contradict] is separate (and - there might not be any), so we handle them all separately *) - [ try common_denominator_equality_inequality_all; - [ try nsatz_inequality_to_equality; - try first [ nsatz; - (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) - try super_nsatz_post_clean_inequalities - | nsatz_alternative ] - | super_nsatz_post_clean_inequalities.. ].. ]. - -Ltac super_nsatz := - super_nsatz_internal - (* if [nsatz] fails, we try turning the goal equality into an inequality and trying again *) - ltac:(nsatz_equality_to_inequality_by_decide_equality; - super_nsatz_internal idtac). - -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; super_nsatz. Qed. - - Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. - Proof. intros; super_nsatz. 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. -Ltac pre_clean_only_two_square_roots := - clear_algebraic_duplicates. -(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *) -Ltac post_clean_only_two_square_roots x y := - clear_algebraic_duplicates; - 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 := - pre_clean_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. - -(*** 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. - - -Section Example. - Context {F 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 F)}. - Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. - Local Notation "0" := zero. Local Notation "1" := one. - - Add Field _ExampleField : (Field.field_theory_for_stdlib_tactic (T:=F)). - - Example _example_nsatz x y : 1+1 <> 0 -> x + y = 0 -> x - y = 0 -> x = 0. - Proof. intros. nsatz. Qed. - - Example _example_field_nsatz x y z : y <> 0 -> x/y = z -> z*y + y = x + y. - Proof. intros. super_nsatz. Qed. - - Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0). - Proof. intros. intro. nsatz_contradict. Qed. -End Example. - -Require Coq.ZArith.ZArith. -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. - - Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0). - Proof. intros. intro. nsatz_contradict. Qed. -End Z. +End ZeroNeqOne.
\ No newline at end of file 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. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 468255f5d..308879293 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -9,6 +9,8 @@ Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.Tactics. Require Export Crypto.Util.FixCoqMistakes. +Global Existing Instance E.char_gt_2. + Module E. Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. @@ -37,7 +39,7 @@ Module E. Section CompleteEdwardsCurveTheorems. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {prm:@twisted_edwards_params F Feq Fzero Fmul a d} + {prm:@twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul a d} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. @@ -66,29 +68,23 @@ Module E. | _ => _gather_nonzeros | _ => progress simpl in * | |- _ /\ _ => split | |- _ <-> _ => split - | _ => solve [fsatz] + | _ => solve [trivial] end. - Ltac t := repeat t_step. + Ltac t := repeat t_step; fsatz. Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)). Next Obligation. t. Qed. Global Instance associative_add : is_associative(eq:=E.eq)(op:=add). Proof. - do 17 t_step. - (* - Ltac debuglevel ::= constr:(1%nat). - all: goal_to_field_equality field. - all: inequalities_to_inverses field. - all: divisions_to_inverses field. - nsatz. (* runs out of 6GB of stack space *) - *) - Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). - all:repeat common_denominator_equality_inequality_all; try nsatz. - { revert H5; intro. fsatz. } - { revert H1; intro. fsatz. } - { revert H6; intro. fsatz. } - { revert H2; intro. fsatz. } + (* [fsatz] runs out of 6GB of stack space *) + Add Field _field : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F)). + Import Field_tac. + repeat t_step; (field_simplify_eq; [IntegralDomain.nsatz|]); repeat split; trivial. + { intro. eapply H5. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H1. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H6. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H2. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } Qed. Global Instance edwards_curve_abelian_group : abelian_group (eq:=E.eq)(op:=add)(id:=zero)(inv:=opp). @@ -122,11 +118,11 @@ Module E. Section Homomorphism. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {Fprm:@twisted_edwards_params F Feq Fzero Fmul Fa Fd} + {Fprm:@twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul Fa Fd} {Feq_dec:DecidableRel Feq}. Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} - {Kprm:@twisted_edwards_params K Keq Kzero Kmul Ka Kd} + {Kprm:@twisted_edwards_params K Keq Kzero Kone Kopp Kadd Ksub Kmul Ka Kd} {Keq_dec:DecidableRel Keq}. Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul K Keq Kone Kadd Kmul phi}. @@ -136,11 +132,11 @@ Module E. Create HintDb field_homomorphism discriminated. Hint Rewrite <- - homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + (homomorphism_one(phi:=phi)) + (homomorphism_add(phi:=phi)) + (homomorphism_sub(phi:=phi)) + (homomorphism_mul(phi:=phi)) + (homomorphism_div(phi:=phi)) Ha Hd : field_homomorphism. @@ -178,4 +174,4 @@ Module E. end. Qed. End Homomorphism. -End E. +End E.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 08eaa6387..263884419 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -16,7 +16,7 @@ Module Extended. Import Group Ring Field. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {prm:@E.twisted_edwards_params F Feq Fzero Fmul a d} + {prm:@E.twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul a d} {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. @@ -24,9 +24,7 @@ Module Extended. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^ 2" := (x*x). Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). - Local Notation onCurve := (@E.onCurve F Feq Fone Fadd Fmul a d). - - Add Field _edwards_curve_extended_field : (field_theory_for_stdlib_tactic (H:=field)). + Local Notation onCurve := (@E.onCurve F Feq Fone Fadd Fmul a d) (only parsing). (** [Extended.point] represents a point on an elliptic curve using extended projective * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) @@ -42,7 +40,7 @@ Module Extended. | _ => progress destruct_head' point | _ => progress destruct_head' and | _ => E._gather_nonzeros - | _ => progress cbv [CompleteEdwardsCurve.E.eq E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig E.onCurve] in * + | _ => progress cbv [CompleteEdwardsCurve.E.eq E.onCurve E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig E.onCurve] in * | |- _ /\ _ => split | |- _ <-> _ => split | _ => rewrite <-!(field_div_definition(field:=field)) | _ => solve [fsatz] @@ -139,31 +137,30 @@ Module Extended. let '(X,Y,Z,T) := add_coordinates (coordinates P) (coordinates Q) in let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z). - Proof. - cbv [E.add add_coordinates to_twisted] in *. destruct prm. t. - (* TODO: change [prove_nsatz_nonzero] to use typeclass resolution to look up field characteristic instead of context matching. then we won't need to destruct prm *) - Qed. + Proof. cbv [E.add add_coordinates to_twisted] in *. t. Qed. Context {add_coordinates_opt} {add_coordinates_opt_correct : forall P1 P2, fieldwise (n:=4) Feq (add_coordinates_opt P1 P2) (add_coordinates P1 P2)}. - (* TODO(jgross): what are these definitions? *) + Axiom admit : forall {T}, T. Obligation Tactic := idtac. Program Definition add_unopt (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q). Next Obligation. - clear add_coordinates_opt add_coordinates_opt_correct. intros P Q. pose proof (add_coordinates_correct P Q) as Hrep. - pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon. destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. - pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz1. - pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz2. - autounfold with bash in *; simpl in *. - destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. - safe_bash. + cbv; cbv in Hrep; destruct Hrep as [HA HB]; cbv in HP; cbv in HQ. + rewrite <-!HA, <-!HB; clear HA HB; repeat split; intros. + all: try ( + goal_to_field_equality field; + inequalities_to_inverse_equations field; + divisions_to_inverses field; + inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit)))); + IntegralDomain.nsatz). + (* TODO: in the onCurve proof for tw coordinate addition we get nonzero-denominator hypotheses from the definition itself. here the definition is not available, but we still need them... *) + exact admit. Qed. - Local Hint Unfold add_unopt : bash. Program Definition add (P Q:point) : point := add_coordinates_opt (coordinates P) (coordinates Q). Next Obligation. @@ -178,14 +175,15 @@ Module Extended. clear add_coordinates_opt add_coordinates_opt_correct. pose proof (add_coordinates_correct P Q) as Hrep. destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. - autounfold with bash in *; simpl in *. + cbv in *. destruct Hrep as [HA HB]. - pose proof (field_div_definition(field:=field)) as Hdiv; symmetry in Hdiv; - (rewrite_strat bottomup Hdiv); - (rewrite_strat bottomup Hdiv in HA); - (rewrite_strat bottomup Hdiv in HB). - rewrite <-!HA, <-!HB; clear HA HB. - split; reflexivity. + split; + goal_to_field_equality field; + inequalities_to_inverse_equations field; + divisions_to_inverses field; + (* and now we need the nonzeros here too *) + inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit)))); + IntegralDomain.nsatz. Qed. Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)). @@ -208,8 +206,8 @@ Module Extended. | [ |- and _ _ ] => split | [ H : ?x = ?y |- context[?x] ] => is_var x; rewrite H | _ => reflexivity - end. } - Qed. + end. admit. } + Admitted. (* TODO: FIXME *) Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 7fa95101e..1d86a8e91 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,213 +1,7 @@ -Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Algebra. +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid Crypto.Util.Relations. +Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field. Require Import Crypto.Util.Notations Crypto.Util.Decidable Crypto.Util.Tactics. - -(* TODO: move *) -Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed. - -Global Instance Symmetric_not {T:Type} (R:T->T->Prop) - {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)). -Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed. - -Section ReflectiveNsatzSideConditionProver. - 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. - - Import BinInt BinNat BinPos. - Axiom ZtoR : Z -> R. - 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. - Lemma CtoZ_correct c : ZtoR (CtoZ c) = denote c. - Proof. - Admitted. - - Section WithChar. - Context C (char_gt_C:forall p, Pos.le p C -> ZtoR (Zpos p) <> zero). - 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 => Pos.leb p C - | Zneg p => Pos.leb 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 is_nonzero in *; fold is_nonzero in *) - | _ => progress change (denote Coef_one) with one 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 Pos.leb_le in * - | _ => rewrite <-Pos2Z.opp_pos in * - | H: Logic.eq match ?x with _ => _ end true |- _ => destruct x eqn:? - | H: _ |- _ => unique pose proof (C_lt_char _ H) - | 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 - | |- _ => solve [eauto | discriminate] - end. - { admit. } - { rewrite <-CtoZ_correct, Heqz. auto. } - { rewrite <-CtoZ_correct, Heqz. admit. } - Admitted. - End WithChar. -End ReflectiveNsatzSideConditionProver. - -Ltac debuglevel := constr:(1%nat). - -Ltac assert_as_by_debugfail G n tac := - ( - assert G as n by tac - ) || - let dbg := debuglevel in - match dbg with - | O => idtac - | _ => idtac "couldn't prove" G - end. - -Ltac solve_debugfail tac := - match goal with - |- ?G => let H := fresh "H" in - assert_as_by_debugfail G H tac; exact H - end. - -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. - -Ltac solve_nsatz_nonzero := - match goal with (* TODO: change this match to a typeclass resolution *) - |H:forall p:BinPos.positive, BinPos.Pos.le p ?C -> not (?eq (?ZtoR (BinInt.Z.pos p)) ?zero) |- not (?eq ?x ?zero) => - let refl_ok' := fresh "refl_ok" in - pose (is_nonzero_correct(eq:=eq)(zero:=zero)(*TODO:ZtoR*) _ H) as refl_ok'; - let refl_ok := (eval cbv delta [refl_ok'] in refl_ok') in - clear refl_ok'; - match refl_ok with - is_nonzero_correct(R:=?R)(one:=?one)(opp:=?opp)(add:=?add)(mul:=?mul)(ring:=?rn)(zpzf:=?zpzf) _ _ => - solve_debugfail ltac:( - let x' := _reify one opp add mul x in - let x' := constr:(@denote R one opp add mul x') in - change (not (eq x' zero)); apply refl_ok; vm_decide - ) - end - 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 (Field.right_multiplicative_inverse(H:=fld) _ d_nz); - set (inv d) as d_i in *; - clearbody d_i. - -Ltac inequalities_to_inverses 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 _division_to_inverse_by fld n 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_as_by_debugfail constr:(not (eq d zero)) d_nz tac; - rewrite (field_div_definition(field:=fld) n d) in *; - lazymatch goal with - | H: eq (mul ?di d) one |- _ => rewrite <-!(Field.left_inv_unique(H:=fld) _ _ H) in * - | H: eq (mul d ?di) one |- _ => rewrite <-!(Field.right_inv_unique(H:=fld) _ _ H) in * - | _ => _introduce_inverse constr:(fld) constr:(d) d_nz - end; - clear d_nz. - -Ltac _nonzero_tac fld := - solve [trivial | goal_to_field_equality fld; nsatz; solve_nsatz_nonzero]. - -Ltac divisions_to_inverses_step 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 - match goal with - | [H: context[div ?n ?d] |- _ ] => _division_to_inverse_by fld n d ltac:(_nonzero_tac fld) - | |- context[div ?n ?d] => _division_to_inverse_by fld n d ltac:(_nonzero_tac fld) - end. - -Ltac divisions_to_inverses fld := - repeat divisions_to_inverses_step fld. - -Ltac fsatz := - let fld := Algebra.guess_field in - goal_to_field_equality fld; - inequalities_to_inverses fld; - divisions_to_inverses fld; - nsatz; solve_nsatz_nonzero. +Require Import Coq.PArith.BinPos. Section Edwards. Context {F eq zero one opp add sub mul inv div} @@ -223,10 +17,10 @@ Section Edwards. Context (a:F) (a_nonzero : a<>0) (a_square : exists sqrt_a, sqrt_a^2 = a). Context (d:F) (d_nonsquare : forall sqrt_d, sqrt_d^2 <> d). - Context (char_gt_2:forall p, BinPos.Pos.le p 2 -> ZtoR (BinInt.Zpos p) <> zero). + Context {char_gt_2:@Ring.char_gt F eq zero one opp add sub mul 2}. Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). - Lemma onCurve_zero : onCurve 0 1. nsatz. Qed. + Lemma onCurve_zero : onCurve 0 1. fsatz. Qed. Section Addition. Context (x1 y1:F) (P1onCurve: onCurve x1 y1). @@ -237,14 +31,14 @@ Section Edwards. try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => pose proof (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) /(f (sqrt_a * x2) y2 * x1 * y1 ))) - end; fsatz. + end; Field.fsatz. Qed. Lemma denominator_nonzero_x : 1 + d*x1*x2*y1*y2 <> 0. - Proof. pose proof denominator_nonzero. fsatz. Qed. + Proof. pose proof denominator_nonzero. Field.fsatz. Qed. Lemma denominator_nonzero_y : 1 - d*x1*x2*y1*y2 <> 0. - Proof. pose proof denominator_nonzero. fsatz. Qed. + Proof. pose proof denominator_nonzero. Field.fsatz. Qed. Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). - Proof. pose proof denominator_nonzero. fsatz. Qed. + Proof. pose proof denominator_nonzero. Field.fsatz. Qed. End Addition. End Edwards.
\ No newline at end of file diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v index 1160ed83a..2585a7392 100644 --- a/src/Encoding/PointEncoding.v +++ b/src/Encoding/PointEncoding.v @@ -66,7 +66,7 @@ Section PointEncoding. {Ksign_correct : forall x, sign x = Ksign (phi x)} {Kenc_correct : forall x, Fencode x = Kenc (phi x)}. - Notation KonCurve := (@Pre.onCurve _ Keq Kone Kadd Kmul Ka Kd). + Notation KonCurve := (@E.onCurve _ Keq Kone Kadd Kmul Ka Kd). Context {Kpoint} {Kcoord_to_point : @E.point K Keq Kone Kadd Kmul Ka Kd -> Kpoint} {Kpoint_to_coord : Kpoint -> (K * K)}. @@ -74,8 +74,8 @@ Section PointEncoding. Context {Kpoint_eq : Kpoint -> Kpoint -> Prop} {Kpoint_add : Kpoint -> Kpoint -> Kpoint}. Context {Kpoint_eq_correct : forall p q, Kpoint_eq p q <-> Tuple.fieldwise (n := 2) Keq (Kpoint_to_coord p) (Kpoint_to_coord q)} {Kpoint_eq_Equivalence : Equivalence Kpoint_eq}. - Context {Fprm:@E.twisted_edwards_params (F m) eq F.zero F.one F.add F.mul Fa Fd}. - Context {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. + Context {Fprm:@E.twisted_edwards_params (F m) eq F.zero F.one F.opp F.add F.sub F.mul Fa Fd}. + Context {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kopp Kadd Ksub Kmul Ka Kd}. Context {phi_bijective : forall x y, Keq (phi x) (phi y) <-> x = y}. Lemma phi_onCurve : forall x y, @@ -86,7 +86,7 @@ Section PointEncoding. Proof. intros. rewrite <-phi_a, <-phi_d. - rewrite <-Algebra.Ring.homomorphism_one. + rewrite <-(Algebra.Ring.homomorphism_one(phi:=phi)). rewrite <-!Algebra.Ring.homomorphism_mul. rewrite <-!Algebra.Ring.homomorphism_add. rewrite phi_bijective. @@ -188,7 +188,7 @@ Section PointEncoding. Lemma onCurve_eq : forall x y, Keq (Kadd (Kmul Ka (Kmul x x)) (Kmul y y)) (Kadd Kone (Kmul (Kmul Kd (Kmul x x)) (Kmul y y))) -> - @Pre.onCurve _ Keq Kone Kadd Kmul Ka Kd (x,y). + @E.onCurve _ Keq Kone Kadd Kmul Ka Kd x y. Proof. clear; tauto. Qed. @@ -471,14 +471,9 @@ Section PointEncoding. (@PointEncodingPre.point_eq _ eq F.one F.add F.mul Fa Fd) x y. Proof. intros. - cbv [option_eq E.eq PointEncodingPre.point_eq + cbv [option_eq CompleteEdwardsCurve.E.eq E.eq E.coordinates PointEncodingPre.point_eq PointEncodingPre.prod_eq]; repeat break_match; try reflexivity. - cbv [E.coordinates]. - subst. - rewrite Heqp1, Heqp0. - cbv [Tuple.fieldwise Tuple.fieldwise' fst snd]. - tauto. Qed. Lemma enc_canonical_equiv : forall (x_enc : word b) (x : F m), diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 8a0d4c849..bbf0f82fd 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -6,7 +6,7 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Bedrock.Word Crypto.Util.WordUtil. Require Import Crypto.Encoding.ModularWordEncodingTheorems. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Algebra. +Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.Option. Import Morphisms. @@ -35,9 +35,9 @@ Section PointEncodingPre. unfold F_eqb; intros; destruct (eq_dec x y); split; auto; discriminate. Qed. - Context {a d:F} {prm:@E.twisted_edwards_params F eq zero one add mul a d}. + Context {a d:F} {prm:@E.twisted_edwards_params F eq zero one opp add sub mul a d}. Local Notation point := (@E.point F eq one add mul a d). - Local Notation onCurve := (@onCurve F eq one add mul a d). + Local Notation onCurve := (@E.onCurve F eq one add mul a d). Local Notation solve_for_x2 := (@E.solve_for_x2 F one sub mul div a d). Context {sz : nat} (sz_nonzero : (0 < sz)%nat). @@ -64,8 +64,8 @@ Section PointEncodingPre. reflexivity. Qed. - Lemma solve_onCurve: forall x y : F, onCurve (x,y) -> - onCurve (sqrt (solve_for_x2 y), y). + Lemma solve_onCurve: forall x y : F, onCurve x y -> + onCurve (sqrt (E.solve_for_x2(Fone:=one)(Fsub:=sub)(Fmul:=mul)(Fdiv:=div)(a:=a)(d:=d) y)) y. Proof. intros. eapply E.solve_correct. @@ -80,8 +80,8 @@ Section PointEncodingPre. intros. ring. Qed. - Lemma solve_opp_onCurve: forall x y : F, onCurve (x,y) -> - onCurve (opp (sqrt (solve_for_x2 y)), y). + Lemma solve_opp_onCurve: forall x y : F, onCurve x y -> + onCurve (opp (sqrt (solve_for_x2 y))) y. Proof. intros. apply E.solve_correct. @@ -146,14 +146,6 @@ Section PointEncodingPre. unfold option_coordinates_eq, option_eq; intros; assumption. Qed. - Lemma prod_eq_onCurve : forall p q : F * F, prod_eq eq eq p q -> - onCurve p -> onCurve q. - Proof. - unfold prod_eq; intros. - destruct p; destruct q. - eauto using onCurve_subst. - Qed. - Lemma option_coordinates_eq_iff : forall x1 x2 y1 y2, option_coordinates_eq (Some (x1,y1)) (Some (x2,y2)) <-> and (eq x1 x2) (eq y1 y2). Proof. @@ -233,7 +225,7 @@ Section PointEncodingPre. Lemma onCurve_eq : forall x y, eq (add (mul a (mul x x)) (mul y y)) (add one (mul (mul d (mul x x)) (mul y y))) -> - @Pre.onCurve _ eq one add mul a d (x,y). + @E.onCurve _ eq one add mul a d x y. Proof. tauto. Qed. @@ -348,17 +340,17 @@ Section PointEncodingPre. sqrt_y == x. Proof. intros. - pose proof (only_two_square_roots_choice x sqrt_y y) as Hchoice. + pose proof (Field.only_two_square_roots_choice x sqrt_y y) as Hchoice. destruct Hchoice; try assumption; symmetry; try assumption. rewrite (sign_bit_subst x (opp sqrt_y)) in * by assumption. rewrite <-sign_bit_opp in * by assumption. rewrite Bool.eqb_negb1 in *; discriminate. Qed. - Lemma point_encoding_coordinates_valid : forall p, onCurve p -> - option_coordinates_eq (point_dec_coordinates (point_enc_coordinates p)) (Some p). + Lemma point_encoding_coordinates_valid p (onCurve_p:onCurve (fst p) (snd p)) + : option_coordinates_eq (point_dec_coordinates (point_enc_coordinates p)) (Some p). Proof. - intros [x y] onCurve_p. + destruct p as [x y]. unfold point_dec_coordinates, point_from_xy, coord_from_y, option_rect. rewrite y_decode. cbv [whd point_enc_coordinates snd]. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 44b422767..262b20e3e 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,7 +6,8 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArit Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. -Require Import Crypto.Algebra Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. Require Export Crypto.Util.FixCoqMistakes. Module F. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index e0dfc8f1a..abc30056f 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -12,7 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -Require Crypto.Algebra. +Require Crypto.Algebra Crypto.Algebra.Field. Existing Class prime. @@ -226,7 +226,7 @@ Module F. split; try apply eq_b4_a2. intro Hyy. rewrite !@F.pow_2_r in *. - destruct (Algebra.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; + destruct (Field.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; [ eexists; eassumption | ]. match goal with H : ?a * ?a = F.opp _ |- _ => exists (sqrt_minus1 * a); rewrite mul_square_sqrt_minus1; rewrite H end. @@ -254,7 +254,7 @@ Module F. break_if. intuition (f_equal; eauto). split; intro A. { - destruct (Algebra.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; + destruct (Field.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; clear A; try congruence. rewrite mul_square_sqrt_minus1, B; field. } { diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v index 4596ad188..bafa62131 100644 --- a/src/MxDHRepChange.v +++ b/src/MxDHRepChange.v @@ -1,5 +1,5 @@ Require Import Crypto.Spec.MxDH. -Require Import Crypto.Algebra. Import Monoid Group Ring Field. +Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field. Require Import Crypto.Util.Tuple. Section MxDHRepChange. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index d475f78c2..05f61f159 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -20,7 +20,7 @@ Module E. Context {a d: F}. Class twisted_edwards_params := { - char_gt_2 : forall p : BinNums.positive, BinPos.Pos.le p 2 -> Pre.ZtoR (BinNums.Zpos p) <> 0; + char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two; nonzero_a : a <> 0; square_a : exists sqrt_a, sqrt_a^2 = a; nonsquare_d : forall x, x^2 <> d @@ -34,7 +34,7 @@ Module E. snd (coordinates P) = snd (coordinates Q). Program Definition zero : point := (0, 1). - Next Obligation. eauto using Pre.onCurve_zero. Qed. + Next Obligation. destruct H; eauto using Pre.onCurve_zero. Qed. Program Definition add (P1 P2:point) : point := let x1y1 := coordinates P1 in let x1 := fst x1y1 in let y1 := snd x1y1 in diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 3d1a30559..7ac33d890 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -11,13 +11,15 @@ Module Pre. Local Open Scope F_scope. Lemma curve25519_params_ok {prime_q:Znumtheory.prime (2^255-19)} : @E.twisted_edwards_params (F (2 ^ 255 - 19)) (@eq (F (2 ^ 255 - 19))) (@F.zero (2 ^ 255 - 19)) - (@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) + (@F.one (2 ^ 255 - 19)) (@F.opp (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.sub (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) (@F.opp (2 ^ 255 - 19) 1) (@F.opp (2 ^ 255 - 19) (F.of_Z (2 ^ 255 - 19) 121665) / F.of_Z (2 ^ 255 - 19) 121666). Proof. pose (@PrimeFieldTheorems.F.Decidable_square (2^255-19) _); - SpecializeBy.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check. - Qed. + SpecializeBy.specialize_by Decidable.vm_decide; split; try Decidable.vm_decide_no_check. + { intros n one_le_n n_le_two. + assert ((n = 1 \/ n = 2)%N) as Hn by admit; destruct Hn; subst; Decidable.vm_decide. } + Admitted. End Pre. (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q. @@ -48,7 +50,7 @@ Section Ed25519. Global Instance curve_params : E.twisted_edwards_params - (F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) + (F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fopp:=F.opp) (Fadd:=F.add) (Fsub:=F.sub) (Fmul:=F.mul) (a:=a) (d:=d). Proof Pre.curve25519_params_ok. Definition E : Type := E.point diff --git a/src/Experiments/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index b3a5586d0..4e448392f 100644 --- a/src/Experiments/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -1,12 +1,12 @@ Require Crypto.Algebra. Require Crypto.Util.GlobalSettings. -Require Crypto.Spec.WeierstrassCurve. -Module W := Crypto.Spec.WeierstrassCurve.E. (* TODO: rename the module? *) +Require Import Crypto.Spec.WeierstrassCurve. Module M. Section MontgomeryCurve. - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. @@ -20,7 +20,7 @@ Module M. Local Notation "( x , y )" := (inl (pair x y)). Local Open Scope core_scope. - Context {a b: F} {b_nonzero:b <> 0} {char_gt_2:2 <> 0} {char_gt_3:3 <> 0}. + Context {a b: F} {b_nonzero:b <> 0}. Definition point := { P | match P with | (x, y) => b*y^2 = x^3 + a*x^2 + x @@ -28,21 +28,16 @@ Module M. end }. Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. - Add Field MontgomeryCurveField : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F)). - Local Ltac t := - repeat match goal with - | _ => progress (intros; cbv [coordinates proj1_sig]) - | _ => solve [trivial|intuition idtac] - | [P:point |- _] => destruct P as [[[??]|?]?] - | |- context [if @Decidable.dec ?P ?pf then _ else _] => destruct (@Decidable.dec P pf) - | |- context [match ?tt with tt => _ end] => destruct tt - | |- context [?a/?b] => progress Algebra.common_denominator - | |- _ = _ => Algebra.nsatz - | |- _ <> _ => - solve [unfold not; rewrite !Algebra.Ring.zero_product_iff_zero_factor; intuition idtac| - Algebra.nsatz_contradict] - end. - Local Obligation Tactic := idtac. + Import Crypto.Util.Tactics Crypto.Algebra.Field. + Ltac t := + destruct_head' point; destruct_head' sum; destruct_head' prod; + break_match; simpl in *; break_match_hyps; trivial; try discriminate; + repeat match goal with + | |- _ /\ _ => split + | [H:@eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + end; + subst; try fsatz. Program Definition add (P1 P2:point) : point := exist _ @@ -57,14 +52,7 @@ Module M. | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 end _. - Next Obligation. - Proof. - t. - unfold not; rewrite !Algebra.Ring.zero_product_iff_zero_factor; intuition idtac. - assert (b * f0^2 = b * 0^2 ) by Algebra.nsatz. - Import Field_tac. field_simplify_eq in H. - rewrite !Algebra.Ring.zero_product_iff_zero_factor in H; intuition idtac; Algebra.nsatz_contradict. - Qed. + Next Obligation. Proof. t. Qed. Program Definition opp (P:point) : point := exist _ @@ -73,49 +61,17 @@ Module M. | ∞ => ∞ end _. Next Obligation. - Proof. - t. - Qed. + Proof. t. Qed. Local Notation "4" := (1+3). Local Notation "16" := (4*4). Local Notation "9" := (3*3). Local Notation "27" := (3*9). + Context {char_gt_27:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 27}. Let WeierstrassA := ((3-a^2)/(3*b^2)). Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)). - Context {Hparams:16*(a^2 - 4)/(b^3)^2 <> 0} {char_gt_27:27<>0}. - - Import Field_tac. - Local Ltac doHparams := - let LH := match type of Hparams with ?LH <> 0 => LH end in - match goal with - |- ?LHS <> 0 => - let H := fresh "H" in - assert (H:LHS = LH); - [|rewrite H; assumption] - end; - try field; repeat split; try trivial. - - Local Ltac do27 := - let LH := match type of char_gt_27 with ?LH <> 0 => LH end in - match goal with - |- ?LHS <> 0 => - let H := fresh "H" in - assert (H:LHS = LH); - [|rewrite H; assumption] - end; - try field; repeat split; try trivial. - - Global Instance WeierstrassParamsOfMontgomery : @W.weierstrass_params - F Feq Fzero Fone Fopp Fadd Fmul - WeierstrassA WeierstrassB. - Proof. - (* I am not sure [common_denominator] is behaving correctly here *) - cbv [WeierstrassA WeierstrassB]; split; trivial; doHparams; do27. - Qed. - Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). Program Definition MontgomeryOfWeierstrass (P:Wpoint) : point := exist @@ -126,17 +82,7 @@ Module M. end _. Next Obligation. - Proof. - repeat match goal with - | _ => solve [trivial] - | [P:Wpoint |- _] => destruct P as [[[??]|?]?] - | _ => progress (intros; cbv [W.coordinates W.point proj1_sig]) - | _ => progress subst WeierstrassA - | _ => progress subst WeierstrassB - end. - field_simplify_eq in y; try field_simplify_eq; repeat split; trivial; try Algebra.nsatz. - do27. - Defined. + Proof. subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. Definition eq (P1 P2:point) := match coordinates P1, coordinates P2 with @@ -145,40 +91,15 @@ Module M. | _, _ => False end. + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_gt_2 WeierstrassA WeierstrassB). Lemma MontgomeryOfWeierstrass_add P1 P2 : eq (MontgomeryOfWeierstrass (W.add P1 P2)) (add (MontgomeryOfWeierstrass P1) (MontgomeryOfWeierstrass P2)). Proof. - cbv [eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig]. - repeat match goal with - | _ => solve [trivial] - | [P:Wpoint |- _] => destruct P as [[[??]|?]?] - | |- context [if @Decidable.dec ?P ?pf then _ else _] => destruct (@Decidable.dec P pf) - | |- context [match ?tt with tt => _ end] => destruct tt - | _ => split - | _ => progress subst WeierstrassA - | _ => progress subst WeierstrassB - end. - { apply n. Algebra.nsatz. } - { apply n. field_simplify_eq; try assumption. Algebra.nsatz. } - { apply n. admit. } - { field_simplify_eq; repeat split; trivial. - field_simplify_eq in y; repeat split; trivial; try do27. - field_simplify_eq in y0; repeat split; trivial; try do27. - field_simplify_eq in f4; repeat split; trivial. - Algebra.nsatz. - intro Hz. apply n. Algebra.nsatz. } - Focus 4. { - apply n. - field_simplify_eq in f3; repeat split; trivial. - admit. } Unfocus. - (* The remaining cases are about points with coordinates (not ∞). - I have not worked through them, and they might be untrue - in case we have an error in either set of addition formulas. *) - Abort. + cbv [WeierstrassA WeierstrassB eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. + Qed. Section AddX. - Lemma homogeneous_x_differential_addition_releations P1 P2 : match coordinates (add P2 (opp P1)), coordinates P1, coordinates P2, coordinates (add P1 P2) with | (x, _), (x1, _), (x2, _), (x3, _) => @@ -187,49 +108,23 @@ Module M. else x3 * (x*(x1-x2)^2) = (x1*x2 - 1)^2 | _, _, _, _ => True end. - Proof. - cbv [opp add coordinates proj1_sig]. t. - unfold not; rewrite !Algebra.Ring.zero_product_iff_zero_factor; intuition idtac. - apply n. field_simplify_eq. - (* true by LHS of y0 and y *) - Admitted. + Proof. t. Qed. Definition onCurve xy := let 'pair x y := xy in b*y^2 = x^3 + a*x^2 + x. Definition xzpoint := { xz | let 'pair x z := xz in (z = 0 \/ exists y, onCurve (pair (x/z) y)) }. Definition xzcoordinates (P:xzpoint) : F*F := proj1_sig P. - Axiom one_neq_zero : 1 <> 0. Program Definition toxz (P:point) : xzpoint := exist _ match coordinates P with | (x, y) => pair x 1 | ∞ => pair 1 0 end _. - Next Obligation. - Proof. - t. - { right. exists f0. cbv [onCurve]. Algebra.common_denominator. Algebra.nsatz. apply one_neq_zero. } - { left; reflexivity. } - Qed. + Next Obligation. t; [right; exists f0; t | left; reflexivity ]. Qed. Definition sig_pair_to_pair_sig {T T' I I'} (xy:{xy | let 'pair x y := xy in I x /\ I' y}) : prod {x:T | I x} {y:T' | I' y} := let 'exist (pair x y) (conj pfx pfy) := xy in pair (exist _ x pfx) (exist _ y pfy). - Local Ltac t := - repeat match goal with - | _ => progress (intros; cbv [coordinates proj1_sig]) - | _ => solve [trivial|intuition idtac] - | [P:point |- _] => destruct P as [[[??]|?]?] - | [P:xzpoint |- _] => destruct P as [[??][?|[??]]] - | |- context [if @Decidable.dec ?P ?pf then _ else _] => destruct (@Decidable.dec P pf) - | |- context [match ?tt with tt => _ end] => destruct tt - | |- context [?a/?b] => progress Algebra.common_denominator - | |- _ = _ => Algebra.nsatz - | |- _ <> _ => - solve [unfold not; rewrite !Algebra.Ring.zero_product_iff_zero_factor; intuition idtac| - Algebra.nsatz_contradict] - end. - (* From Explicit Formulas Database by Lange and Bernstein, credited to 1987 Montgomery "Speeding the Pollard and elliptic curve methods of factorization", page 261, fifth and sixth displays, plus @@ -256,16 +151,15 @@ Module M. (pair (pair X4 Z4) (pair X5 Z5)) end _) ). Proof. - cbv [onCurve xzcoordinates] in *. - t; intuition idtac; cbv [onCurve xzcoordinates] in *. - { left. Algebra.nsatz. } - { left. Algebra.nsatz. } + destruct P1, P2; cbv [onCurve xzcoordinates] in *. t; intuition idtac. + { left. fsatz. } + { left. fsatz. } admit. admit. admit. admit. { right. - admit. (* the following works, but slowly: + admit. (* the following used to work, but slowly: exists ((fun x1 y1 x2 y2 => (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) (f1/f2) x0 (f/f0) x). Algebra.common_denominator_in H. Algebra.common_denominator_in H0. @@ -279,7 +173,7 @@ Module M. admit. admit. *) } { right. - exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). + (* exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). *) (* XXX: this case is probably not true -- there is not necessarily a guarantee that the output x/z is on curve if [X1] was not the x coordinate of the difference of input points as requored *) Abort. End AddX. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 484a67c89..8b5480620 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -1,6 +1,6 @@ Require Crypto.WeierstrassCurve.Pre. -Module E. +Module W. Section WeierstrassCurves. (* Short Weierstrass curves with addition laws. References: * <https://hyperelliptic.org/EFD/g1p/auto-shortw.html> @@ -9,7 +9,7 @@ Module E. * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79) *) - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. @@ -19,57 +19,47 @@ Module E. Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). Local Notation "'∞'" := unit : type_scope. Local Notation "'∞'" := (inr tt) : core_scope. - Local Notation "0" := Fzero. Local Notation "1" := Fone. - Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3). - Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))). - Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))). - Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))). Local Notation "( x , y )" := (inl (pair x y)). Local Open Scope core_scope. Context {a b: F}. - (** N.B. We may require more conditions to prove that points form - a group under addition (associativity, in particular. If - that's the case, more fields will be added to this class. *) - Class weierstrass_params := - { - char_gt_2 : 2 <> 0; - char_ne_3 : 3 <> 0; - nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0 - }. - Context `{weierstrass_params}. - Definition point := { P | match P with | (x, y) => y^2 = x^3 + a*x + b | ∞ => True end }. Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. - (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *) - Local Obligation Tactic := - try solve [ Program.Tactics.program_simpl - | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ]. + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. Program Definition zero : point := ∞. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Program Definition add (P1 P2:point) : point := exist _ (match coordinates P1, coordinates P2 return _ with | (x1, y1), (x2, y2) => if x1 =? x2 then - if y2 =? -y1 then ∞ - else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, - (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) - else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, - (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) - | ∞, ∞ => ∞ - | ∞, _ => coordinates P2 - | _, ∞ => coordinates P1 + if y2 =? -y1 then ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 end) _. + Next Obligation. exact (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. Fixpoint mul (n:nat) (P : point) : point := match n with @@ -77,8 +67,8 @@ Module E. | S n' => add P (mul n' P) end. End WeierstrassCurves. -End E. +End W. -Delimit Scope E_scope with E. -Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope. +Delimit Scope W_scope with W. +Infix "+" := W.add : W_scope. +Infix "*" := W.mul : W_scope. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index cf8a68340..97c3e02a3 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -1,7 +1,7 @@ Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. -Require Import Crypto.Algebra. Import Monoid ScalarMult. +Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Option. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 85868f33f..7e6ec1e81 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,7 +1,7 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Crypto.Algebra. Import Monoid. +Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Require Import Crypto.Util.NUtil. Local Open Scope equiv_scope. @@ -174,4 +174,4 @@ Proof. | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) | _ => intro end. -Qed.
\ No newline at end of file +Qed. diff --git a/src/Util/Relations.v b/src/Util/Relations.v index 8ab045cfe..7dc654ec3 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -51,3 +51,9 @@ Qed. Global Instance eq_eta_Reflexive {T} : Reflexive (fun x y : T => x = y) | 1 := eq_Reflexive. + +Global Instance Symmetric_not {T:Type} (R:T->T->Prop) + {SymmetricR:Symmetric R} : Symmetric (fun a b => not (R a b)). +Proof. cbv [Symmetric] in *; repeat intro; eauto. Qed. + +Lemma not_exfalso (P:Prop) (H:P->False) : not P. auto with nocore. Qed.
\ No newline at end of file diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index c83790acc..5f7ad65cc 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -28,6 +28,16 @@ Ltac contains search_for in_term := | appcontext[search_for] => idtac end. +Ltac debuglevel := constr:(0%nat). + +Ltac solve_debugfail tac := + solve [tac] || + let dbg := debuglevel in + match dbg with + | O => idtac + | _ => match goal with |- ?G => idtac "couldn't prove" G end + end. + Ltac set_evars := repeat match goal with | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index 039ffad8a..c33d14691 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -1,14 +1,15 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra. +Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. +Import BinNums. Local Open Scope core_scope. Generalizable All Variables. Section Pre. - Context {F eq zero one opp add sub mul inv div} {field:@field F eq zero one opp add sub mul inv div} {eq_dec: DecidableRel eq}. + Context {F eq zero one opp add sub mul inv div} {field:@field F eq zero one opp add sub mul inv div} {eq_dec: DecidableRel eq} {char_gt_2:@Ring.char_gt F eq zero one opp add sub mul 2%N}. 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. @@ -21,9 +22,6 @@ Section Pre. Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "( x , y )" := (inl (pair x y)). - Add Field WeierstrassCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). - Add Ring WeierstrassCurveRing : (Ring.ring_theory_for_stdlib_tactic (T:=F)). - Context {a:F}. Context {b:F}. @@ -48,10 +46,11 @@ Section Pre. | _, ∞ => P1' end. - Lemma unifiedAdd'_onCurve : forall P1 P2, - onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). + Lemma unifiedAdd'_onCurve P1 P2 + (O1:onCurve P1) (O2:onCurve P2) : onCurve (unifiedAdd' P1 P2). Proof. - unfold onCurve, unifiedAdd'; intros [ [x1 y1]|] [ [x2 y2]|] H1 H2; - break_match; trivial; setoid_subst_rel eq; only_two_square_roots; super_nsatz. + destruct_head' sum; destruct_head' prod; + cbv [onCurve unifiedAdd'] in *; break_match; + trivial; [|]; setoid_subst_rel eq; fsatz. Qed. End Pre. |