From 750fe7116b03a52739d37bbac7f8766a61b11bc9 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 9 Feb 2017 14:00:49 -0500 Subject: Added ZToRing lemmas --- src/Algebra/ZToRing.v | 1694 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1694 insertions(+) create mode 100644 src/Algebra/ZToRing.v (limited to 'src/Algebra') diff --git a/src/Algebra/ZToRing.v b/src/Algebra/ZToRing.v new file mode 100644 index 000000000..e126fd9af --- /dev/null +++ b/src/Algebra/ZToRing.v @@ -0,0 +1,1694 @@ +Require Export Crypto.Util.FixCoqMistakes. +Require Export Crypto.Util.Decidable. + +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +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). + 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 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. + 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) => 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'. + 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. -- cgit v1.2.3