From 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2017 14:35:43 -0400 Subject: Add [Proof using] to most proofs This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper). --- src/Algebra/Field.v | 28 +++++++++++----------- src/Algebra/Field_test.v | 34 +++++++++++++++------------ src/Algebra/Group.v | 40 +++++++++++++++---------------- src/Algebra/IntegralDomain.v | 18 +++++++------- src/Algebra/Monoid.v | 8 +++---- src/Algebra/Ring.v | 56 ++++++++++++++++++++++---------------------- src/Algebra/ScalarMult.v | 18 +++++++------- 7 files changed, 104 insertions(+), 98 deletions(-) (limited to 'src/Algebra') diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index f35e2c1cc..e71b24018 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -12,12 +12,12 @@ Section Field. Local Infix "+" := add. Local Infix "*" := mul. Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one. - Proof. + Proof using Type*. intros. rewrite commutative. auto using left_multiplicative_inverse. Qed. Lemma left_inv_unique x ix : ix * x = one -> ix = inv x. - Proof. + Proof using Type*. intro Hix. assert (ix*x*inv x = inv x). - rewrite Hix, left_identity; reflexivity. @@ -28,17 +28,17 @@ Section Field. Definition inv_unique := left_inv_unique. Lemma right_inv_unique x ix : x * ix = one -> ix = inv x. - Proof. rewrite commutative. apply left_inv_unique. Qed. + Proof using Type*. rewrite commutative. apply left_inv_unique. Qed. Lemma div_one x : div x one = x. - Proof. + Proof using Type*. 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. + Proof using Type*. intros. split; intros. + rewrite <-(right_multiplicative_inverse y) by assumption. @@ -50,7 +50,7 @@ Section Field. Qed. Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq. - Proof. + Proof using Type*. constructor. { apply Ring.ring_theory_for_stdlib_tactic. } { intro H01. symmetry in H01. auto using (zero_neq_one(eq:=eq)). } @@ -61,7 +61,7 @@ Section Field. Context {eq_dec:DecidableRel eq}. Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul. - Proof. + Proof using Type*. split. intros x y Hxy. eapply not_not; try typeclasses eauto; []; intuition idtac; eapply (zero_neq_one(eq:=eq)). transitivity ((inv y * (inv x * x)) * y). @@ -71,7 +71,7 @@ Section Field. Qed. Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul. - Proof. + Proof using Type*. split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero. Qed. End Field. @@ -126,7 +126,7 @@ Section Homomorphism. Lemma homomorphism_multiplicative_inverse : forall x, not (EQ x ZERO) -> phi (INV x) = inv (phi x). - Proof. + Proof using Type*. intros. eapply inv_unique. rewrite <-Ring.homomorphism_mul. @@ -137,14 +137,14 @@ Section Homomorphism. { EQ_dec : DecidableRel EQ } : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x)) -> phi (INV x) = inv (phi x). - Proof. + Proof using Type*. 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. + Proof using Type*. intros. rewrite !field_div_definition. rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse; (eauto || reflexivity). @@ -154,7 +154,7 @@ Section Homomorphism. { 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. + Proof using Type*. intros. rewrite !field_div_definition. rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete; (eauto || reflexivity). @@ -181,7 +181,7 @@ Section Homomorphism_rev. : @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. + Proof using Type*. repeat match goal with | [ H : field |- _ ] => destruct H; try clear H | [ H : commutative_ring |- _ ] => destruct H; try clear H @@ -320,7 +320,7 @@ Section FieldSquareRoot. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := add. Local Infix "*" := mul. Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y. - Proof. + Proof using Type*. intros. setoid_rewrite <-sub_zero_iff. eapply zero_product_zero_factor. diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v index 2df673163..0743729c2 100644 --- a/src/Algebra/Field_test.v +++ b/src/Algebra/Field_test.v @@ -13,33 +13,37 @@ Module _fsatz_test. Local Infix "-" := sub. Local Infix "/" := div. Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c). - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c). - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma zero_neq_one : 0 <> 1. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma only_two_square_roots x y : x * x = y * y -> x <> opp y -> x = y. - Proof. intros; fsatz. Qed. + Proof using Type*. intros; fsatz. Qed. Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1. - Proof. fsatz. Qed. - Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed. - Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed. + Proof using Type*. fsatz. Qed. + Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. + Proof using Type*. + fsatz. Qed. + Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. + Proof using Type*. + fsatz. Qed. Import BinNums. Context {char_ge_16:@Ring.char_ge F eq zero one opp add sub mul 16}. @@ -50,10 +54,10 @@ Module _fsatz_test. Local Notation nine := (three+three+three) (only parsing). Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two). - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False. - Proof. fsatz. Qed. + Proof using Type*. fsatz. Qed. Local Notation "x ^ 2" := (x*x). Lemma recursive_nonzero_solving @@ -62,7 +66,7 @@ Module _fsatz_test. (Hsqrt : sqrt_a^2 = a) (Hfrac : (sqrt_a / y)^2 <> d) : x^2 = (y^2 - one) / (d * y^2 - a). - Proof. fsatz. Qed. + Proof using eq_dec fld. fsatz. Qed. Local Notation "x ^ 3" := (x^2*x). Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4 @@ -86,6 +90,6 @@ Module _fsatz_test. x9 (Hx9: x9 = λ9^2-x1-x6) y9 (Hy9: y9 = λ9*(x1-x9)-y1) : x7 = x9 /\ y7 = y9. - Proof. fsatz_prepare_hyps; split; fsatz. Qed. + Proof using Type*. fsatz_prepare_hyps; split; fsatz. Qed. End _test. End _fsatz_test. \ No newline at end of file diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index b053fc844..64e378281 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -9,16 +9,16 @@ Section BasicProperties. 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. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. eauto using Monoid.inv_op, left_inverse. Qed. Lemma inv_unique x ix : ix * x = id -> ix = inv x. - Proof. + Proof using Type*. intro Hix. cut (ix*x*inv x = inv x). - rewrite <-associative, right_inverse, right_identity; trivial. @@ -26,14 +26,14 @@ Section BasicProperties. Qed. Lemma inv_bijective x y : inv x = inv y <-> x = y. - Proof. + Proof using Type*. split; intro Hi; rewrite ?Hi; try reflexivity. assert (Hii:inv (inv x) = inv (inv y)) by (rewrite Hi; reflexivity). rewrite 2inv_inv in Hii; exact Hii. Qed. Lemma inv_op x y : inv (x*y) = inv y*inv x. - Proof. + Proof using Type*. symmetry. etransitivity. 2:eapply inv_unique. 2:eapply inv_op_ext. @@ -41,19 +41,19 @@ Section BasicProperties. Qed. Lemma inv_id : inv id = id. - Proof. symmetry. eapply inv_unique, left_identity. Qed. + Proof using Type*. symmetry. eapply inv_unique, left_identity. Qed. Lemma inv_id_iff x : inv x = id <-> x = id. - Proof. + Proof using Type*. split; intro Hi; rewrite ?Hi, ?inv_id; try reflexivity. rewrite <-inv_id, inv_bijective in Hi; exact Hi. Qed. Lemma inv_nonzero_nonzero x : x <> id <-> inv x <> id. - Proof. setoid_rewrite inv_id_iff; reflexivity. Qed. + Proof using Type*. setoid_rewrite inv_id_iff; reflexivity. Qed. Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c. - Proof. + Proof using Type*. split; intro Hx; rewrite Hx || rewrite <-Hx; rewrite <-!associative, ?left_inverse, ?right_inverse, right_identity; reflexivity. @@ -62,9 +62,9 @@ Section BasicProperties. Section ZeroNeqOne. Context {one} `{is_zero_neq_one T eq id one}. Lemma opp_one_neq_zero : inv one <> id. - Proof. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed. + Proof using Type*. setoid_rewrite inv_id_iff. exact 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. + Proof using Type*. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed. End ZeroNeqOne. End BasicProperties. @@ -75,14 +75,14 @@ Section Homomorphism. Local Infix "=" := eq. Local Infix "=" := eq : type_scope. Lemma homomorphism_id : phi ID = id. - Proof. + Proof using Type*. 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. + Proof using Type*. apply inv_unique. rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. Qed. @@ -91,11 +91,11 @@ Section Homomorphism. 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. + Proof using Type*. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed. Import ScalarMult. Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P). - Proof. + Proof using groupH mul_is_scalarmult. induction n; intros. { rewrite !scalarmult_0_l, inv_id; reflexivity. } { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. @@ -117,7 +117,7 @@ Section Homomorphism_rev. Lemma group_from_redundant_representation : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'. - Proof. + Proof using Type*. repeat match goal with | [ H : _/\_ |- _ ] => destruct H; try clear H | [ H : group |- _ ] => destruct H; try clear H @@ -141,7 +141,7 @@ Section Homomorphism_rev. Definition homomorphism_from_redundant_representation : @Monoid.is_homomorphism G EQ OP H eq op phi. - Proof. + Proof using groupG phi'_eq phi'_op phi'_phi_id. split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy. Qed. End Homomorphism_rev. @@ -204,7 +204,7 @@ Section HomomorphismComposition. {phi'':G->K} (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x)) : @Monoid.is_homomorphism G EQ OP K eqK opK phi''. - Proof. + Proof using Hphi Hphi' groupK. split; repeat intro; rewrite <- !Hphi''. { rewrite !Monoid.homomorphism; reflexivity. } { apply Hphi', Hphi; assumption. } diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 083c10242..4ab50c6e3 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -11,12 +11,12 @@ Module IntegralDomain. 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. + Proof using Type*. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed. Global Instance Integral_domain : @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring. - Proof. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed. + Proof using Type. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed. End IntegralDomain. Module _LargeCharacteristicReflective. @@ -51,14 +51,14 @@ Module IntegralDomain. Let of_Z := (@Ring.of_Z R zero one opp add). Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c. - Proof. + Proof using ring. induction c; simpl CtoZ; simpl denote; repeat (rewrite_hyp ?* || Ring.push_homomorphism of_Z); reflexivity. Qed. (* TODO: move *) Lemma nonzero_of_Z_abs z : of_Z (Z.abs z) <> zero <-> of_Z z <> zero. - Proof. + Proof using ring. destruct z; simpl Z.abs; [reflexivity..|]. simpl of_Z. setoid_rewrite opp_zero_iff. reflexivity. Qed. @@ -70,13 +70,13 @@ Module IntegralDomain. match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end. Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true) : of_Z (Z.of_N n) <> zero. - Proof. + Proof using char_ge_C. destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_ge_C, Pos.ltb_lt, refl. Qed. Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero) : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero. - Proof. + Proof using HC char_ge_C ring zpzf. rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right. { eapply char_ge_C; assumption. } { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z. @@ -90,7 +90,7 @@ Module IntegralDomain. end. Lemma is_constant_nonzero_correct z (refl:Logic.eq (is_constant_nonzero z) true) : of_Z z <> zero. - Proof. + Proof using HC char_ge_C ring zpzf. rewrite <-nonzero_of_Z_abs, <-Znat.N2Z.inj_abs_N. repeat match goal with | _ => progress cbv [is_constant_nonzero] in * @@ -109,7 +109,7 @@ Module IntegralDomain. | _ => is_constant_nonzero (CtoZ c) end. Lemma is_nonzero_correct' c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. - Proof. + Proof using HC char_ge_C ring zpzf. induction c; repeat match goal with | H:_|-_ => progress rewrite Bool.andb_true_iff in H; destruct H @@ -131,7 +131,7 @@ Module IntegralDomain. (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) c (refl:Logic.eq (andb (Pos.ltb xH C) (is_nonzero C c)) true) : denote c <> zero. - Proof. + Proof using ring zpzf. rewrite Bool.andb_true_iff in refl; destruct refl. eapply @is_nonzero_correct'; try apply Pos.ltb_lt; eauto. Qed. diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v index 565058cf7..bd15290c7 100644 --- a/src/Algebra/Monoid.v +++ b/src/Algebra/Monoid.v @@ -11,7 +11,7 @@ Section Monoid. Lemma cancel_right z iz (Hinv:op z iz = id) : forall x y, x * z = y * z <-> x = y. - Proof. + Proof using Type*. split; intros. { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity). rewrite <-associative in Hcut. @@ -21,7 +21,7 @@ Section Monoid. Lemma cancel_left z iz (Hinv:op iz z = id) : forall x y, z * x = z * y <-> x = y. - Proof. + Proof using Type*. split; intros. { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity). rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. } @@ -29,14 +29,14 @@ Section Monoid. Qed. Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x. - Proof. + Proof using Type*. 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. + Proof using Type*. intros Hx Hy. cut (iy * (ix*x) * y = id); try intro H. { rewrite <-!associative; rewrite <-!associative in H; exact H. } diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 2b0e1ba80..cff27bdb3 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -15,7 +15,7 @@ Section Ring. Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. Lemma mul_0_l : forall x, 0 * x = 0. - Proof. + Proof using Type*. intros. assert (0*x = 0*x) as Hx by reflexivity. rewrite <-(right_identity 0), right_distributive in Hx at 1. @@ -24,7 +24,7 @@ Section Ring. Qed. Lemma mul_0_r : forall x, x * 0 = 0. - Proof. + Proof using Type*. intros. assert (x*0 = x*0) as Hx by reflexivity. rewrite <-(left_identity 0), left_distributive in Hx at 1. @@ -33,10 +33,10 @@ Section Ring. Qed. Lemma sub_0_l x : 0 - x = opp x. - Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed. + Proof using Type*. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed. Lemma mul_opp_r x y : x * opp y = opp (x * y). - Proof. + Proof using Type*. 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. @@ -44,7 +44,7 @@ Section Ring. Qed. Lemma mul_opp_l x y : opp x * y = opp (x * y). - Proof. + Proof using Type*. 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. @@ -54,19 +54,19 @@ Section Ring. Definition opp_zero_iff : forall x, opp x = 0 <-> x = 0 := Group.inv_id_iff. Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul). - Proof. + Proof using Type*. 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. + Proof using Type*. split; intros. rewrite !ring_sub_definition, right_distributive. eapply Group.cancel_left, mul_opp_l. Qed. Lemma sub_zero_iff x y : x - y = 0 <-> x = y. - Proof. + Proof using Type*. split; intro E. { rewrite <-(right_identity y), <- E, ring_sub_definition. rewrite commutative, <-associative, commutative. @@ -75,25 +75,25 @@ Section Ring. Qed. Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0. - Proof. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances. - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *) eapply @left_identity; eauto with typeclass_instances. @@ -121,23 +121,23 @@ Section Homomorphism. Context `{phi_homom:is_homomorphism}. Lemma homomorphism_zero : phi ZERO = zero. - Proof. apply Group.homomorphism_id. Qed. + Proof using Type*. apply Group.homomorphism_id. Qed. Lemma homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y). - Proof. apply Monoid.homomorphism. Qed. + Proof using phi_homom. 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. + Proof using Type*. intros. rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity. Qed. Global Instance monoid_homomorphism_mul : Monoid.is_homomorphism (phi:=phi) (OP:=MUL) (op:=mul) (EQ:=EQ) (eq:=eq). - Proof. split; destruct phi_homom; assumption || exact _. Qed. + Proof using phi_homom. split; destruct phi_homom; assumption || exact _. Qed. End Homomorphism. (* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *) @@ -200,7 +200,7 @@ Section Isomorphism. : @ring H eq zero one opp add sub mul /\ @is_homomorphism F EQ ONE ADD MUL H eq one add mul phi /\ @is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'. - Proof. + Proof using phi'_add phi'_eq phi'_mul phi'_one phi'_opp phi'_phi_id phi'_sub phi'_zero ringF. repeat match goal with | [ H : field |- _ ] => destruct H; try clear H | [ H : commutative_ring |- _ ] => destruct H; try clear H @@ -236,10 +236,10 @@ Section TacticSupportCommutative. Global Instance Cring_Cring_commutative_ring : @Cring.Cring T zero one add mul sub opp eq Ncring_Ring_ops Ncring_Ring. - Proof. unfold Cring.Cring; intros; cbv. eapply commutative. Qed. + Proof using Type. unfold Cring.Cring; intros; cbv. eapply commutative. Qed. Lemma ring_theory_for_stdlib_tactic : Ring_theory.ring_theory zero one add mul sub opp eq. - Proof. + Proof using Type*. constructor; intros. (* TODO(automation): make [auto] do this? *) - apply left_identity. - apply commutative. @@ -289,15 +289,15 @@ Section of_Z. end. Lemma of_Z_0 : of_Z 0 = Rzero. - Proof. reflexivity. Qed. + Proof using Type*. reflexivity. Qed. Lemma of_nat_add x : of_nat (Nat.add x 1) = Radd (of_nat x) Rone. - Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed. + Proof using Type*. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed. Lemma of_nat_sub x (H: (0 < x)%nat): of_nat (Nat.sub x 1) = Rsub (of_nat x) Rone. - Proof. + Proof using Type*. induction x; [omega|simpl]. rewrite <-of_nat_add. rewrite Nat.sub_0_r, Nat.add_1_r. @@ -309,7 +309,7 @@ Section of_Z. Lemma of_Z_add_1_r : forall x, of_Z (Z.add x 1) = Radd (of_Z x) Rone. - Proof. + Proof using Type*. destruct x; [reflexivity| | ]; simpl of_Z. { rewrite Pos2Nat.inj_add, of_nat_add. reflexivity. } @@ -330,7 +330,7 @@ Section of_Z. Lemma of_Z_sub_1_r : forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone. - Proof. + Proof using Type*. induction x. { simpl; rewrite ring_sub_definition, !left_identity; reflexivity. } @@ -354,14 +354,14 @@ Section of_Z. Lemma of_Z_opp : forall a, of_Z (Z.opp a) = Ropp (of_Z a). - Proof. + Proof using Type*. destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv; reflexivity. Qed. Lemma of_Z_add : forall a b, of_Z (Z.add a b) = Radd (of_Z a) (of_Z b). - Proof. + Proof using Type*. intros. let x := match goal with |- ?x => x end in let f := match (eval pattern b in x) with ?f _ => f end in @@ -381,7 +381,7 @@ Section of_Z. Lemma of_Z_mul : forall a b, of_Z (Z.mul a b) = Rmul (of_Z a) (of_Z b). - Proof. + Proof using Type*. intros. let x := match goal with |- ?x => x end in let f := match (eval pattern b in x) with ?f _ => f end in @@ -408,7 +408,7 @@ Section of_Z. Z Logic.eq Z.one Z.add Z.mul R Req Rone Radd Rmul of_Z. - Proof. + Proof using Type*. repeat constructor; intros. { apply of_Z_add. } { repeat intro; subst; reflexivity. } diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v index 33c236775..5c17a6bb5 100644 --- a/src/Algebra/ScalarMult.v +++ b/src/Algebra/ScalarMult.v @@ -28,30 +28,32 @@ Section ScalarMultProperties. end. Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. - Proof. + Proof using monoidG. 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. + Proof using Type*. + 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. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. 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. + Proof using Type*. induction n; intros. { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. @@ -59,10 +61,10 @@ Section ScalarMultProperties. 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. + Proof using Type*. 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. + Proof using Type*. 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. @@ -79,7 +81,7 @@ Section ScalarMultHomomorphism. Context (phi_ZERO:phi ZERO = zero). Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). - Proof. + Proof using Type*. setoid_rewrite scalarmult_ext. induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. Qed. -- cgit v1.2.3