From 32849ba878e74064e2bb312ea0a5f2e2e2ed6659 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 10 Feb 2017 09:03:24 -0500 Subject: Accidentally pushed wrong file in last commit; this is the correct one --- src/Algebra/ZToRing.v | 1807 ++++--------------------------------------------- 1 file changed, 131 insertions(+), 1676 deletions(-) (limited to 'src/Algebra') diff --git a/src/Algebra/ZToRing.v b/src/Algebra/ZToRing.v index e126fd9af..8b9195d75 100644 --- a/src/Algebra/ZToRing.v +++ b/src/Algebra/ZToRing.v @@ -1,1694 +1,149 @@ -Require Export Crypto.Util.FixCoqMistakes. -Require Export Crypto.Util.Decidable. - -Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Coq.ZArith.ZArith. +Require Import Coq.PArith.PArith. +Require Import Crypto.Algebra. Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. - -Require Coq.setoid_ring.Field_theory. -Require Crypto.Tactics.Algebra_syntax.Nsatz. -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. - - Section SingleOperation. - Context {op:T->T->T}. - - Class is_associative := { associative : forall x y z, op x (op y z) = op (op x y) z }. - - Context {id:T}. - - Class is_left_identity := { left_identity : forall x, op id x = x }. - Class is_right_identity := { right_identity : forall x, op x id = x }. - - Class monoid := - { - monoid_is_associative : is_associative; - monoid_is_left_identity : is_left_identity; - monoid_is_right_identity : is_right_identity; - - monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op; - monoid_Equivalence : Equivalence eq - }. - Global Existing Instance monoid_is_associative. - Global Existing Instance monoid_is_left_identity. - Global Existing Instance monoid_is_right_identity. - Global Existing Instance monoid_Equivalence. - Global Existing Instance monoid_op_Proper. - - Context {inv:T->T}. - Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }. - Class is_right_inverse := { right_inverse : forall x, op x (inv x) = id }. - - Class group := - { - group_monoid : monoid; - group_is_left_inverse : is_left_inverse; - group_is_right_inverse : is_right_inverse; - - group_inv_Proper: Proper (respectful eq eq) inv - }. - Global Existing Instance group_monoid. - Global Existing Instance group_is_left_inverse. - Global Existing Instance group_is_right_inverse. - Global Existing Instance group_inv_Proper. - - Class is_commutative := { commutative : forall x y, op x y = op y x }. - - Record abelian_group := - { - abelian_group_group : group; - abelian_group_is_commutative : is_commutative - }. - Existing Class abelian_group. - Global Existing Instance abelian_group_group. - Global Existing Instance abelian_group_is_commutative. - End SingleOperation. - - Section AddMul. - Context {zero one:T}. Local Notation "0" := zero. Local Notation "1" := one. - Context {opp:T->T}. Local Notation "- x" := (opp x). - Context {add:T->T->T} {sub:T->T->T} {mul:T->T->T}. - Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. - - Class is_left_distributive := { left_distributive : forall a b c, a * (b + c) = a * b + a * c }. - Class is_right_distributive := { right_distributive : forall a b c, (b + c) * a = b * a + c * a }. - - - Class ring := - { - ring_abelian_group_add : abelian_group (op:=add) (id:=zero) (inv:=opp); - ring_monoid_mul : monoid (op:=mul) (id:=one); - ring_is_left_distributive : is_left_distributive; - ring_is_right_distributive : is_right_distributive; - - ring_sub_definition : forall x y, x - y = x + opp y; - - ring_mul_Proper : Proper (respectful eq (respectful eq eq)) mul; - ring_sub_Proper : Proper(respectful eq (respectful eq eq)) sub - }. - Global Existing Instance ring_abelian_group_add. - Global Existing Instance ring_monoid_mul. - Global Existing Instance ring_is_left_distributive. - Global Existing Instance ring_is_right_distributive. - Global Existing Instance ring_mul_Proper. - Global Existing Instance ring_sub_Proper. - - Class commutative_ring := - { - commutative_ring_ring : ring; - commutative_ring_is_commutative : is_commutative (op:=mul) - }. - Global Existing Instance commutative_ring_ring. - Global Existing Instance commutative_ring_is_commutative. - - Class is_zero_product_zero_factor := - { zero_product_zero_factor : forall x y, x*y = 0 -> x = 0 \/ y = 0 }. - - Class is_zero_neq_one := { zero_neq_one : zero <> one }. - - Class integral_domain := - { - integral_domain_commutative_ring : commutative_ring; - integral_domain_is_zero_product_zero_factor : is_zero_product_zero_factor; - integral_domain_is_zero_neq_one : is_zero_neq_one - }. - Global Existing Instance integral_domain_commutative_ring. - Global Existing Instance integral_domain_is_zero_product_zero_factor. - Global Existing Instance integral_domain_is_zero_neq_one. - - Context {inv:T->T} {div:T->T->T}. - Class is_left_multiplicative_inverse := { left_multiplicative_inverse : forall x, x<>0 -> (inv x) * x = 1 }. - - Class field := - { - field_commutative_ring : commutative_ring; - field_is_left_multiplicative_inverse : is_left_multiplicative_inverse; - field_is_zero_neq_one : is_zero_neq_one; - - field_div_definition : forall x y , div x y = x * inv y; - - field_inv_Proper : Proper (respectful eq eq) inv; - field_div_Proper : Proper (respectful eq (respectful eq eq)) div - }. - Global Existing Instance field_commutative_ring. - Global Existing Instance field_is_left_multiplicative_inverse. - Global Existing Instance field_is_zero_neq_one. - Global Existing Instance field_inv_Proper. - Global Existing Instance field_div_Proper. - End AddMul. -End Algebra. - -Section ZeroNeqOne. - Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}. - - Lemma one_neq_zero : not (eq one zero). +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. - intro HH; symmetry in HH. auto using zero_neq_one. + 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. -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 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. - - 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. + Lemma ZToRing_plus_correct : + forall x, ZToRing (Z.add x 1) = Radd (ZToRing x) Rone. 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. + 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 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. + Lemma ZToRing_minus_correct : + forall x, ZToRing (Z.sub x 1) = Rsub (ZToRing x) Rone. Proof. - repeat intro. - transitivity (f x); auto. - transitivity (f y); auto. - symmetry; auto. + 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 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. + Lemma ZToRing_inj_opp : forall a, + ZToRing (Z.opp a) = Ropp (ZToRing a). 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) => eq 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'. + destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv; + reflexivity. Qed. - Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y. + Lemma ZToRing_inj_add : forall a b, + ZToRing (Z.add a b) = Radd (ZToRing a) (ZToRing b). 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. + 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 only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y. + + Lemma ZToRing_inj_mul : forall a b, + ZToRing (Z.mul a b) = Rmul (ZToRing a) (ZToRing b). Proof. - intros; setoid_subst z; eauto using only_two_square_roots'_choice. + 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. -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. + + + Lemma ZToRingHomom : @Ring.is_homomorphism + Z Z.eq Z.one Z.add Z.mul + R Req Rone Radd Rmul + ZToRing. 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. + 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. \ No newline at end of file -- cgit v1.2.3