diff options
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 51 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 14 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 8 |
3 files changed, 38 insertions, 35 deletions
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index adaa340db..f5c550417 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -317,11 +317,12 @@ assert (HH: ~ r5*r6 == 0). apply field_is_integral_domain. intros H1; case H; rewrite H1; ring. intros H1; case H0; rewrite H1; ring. -rewrite <- rdiv4; auto. +rewrite <- rdiv4 ; auto. + rewrite rdiv_r_r; auto. + apply field_is_integral_domain. intros H1; case H; rewrite H1; ring. intros H1; case H0; rewrite H1; ring. -rewrite rdiv_r_r; auto. Qed. @@ -353,11 +354,11 @@ assert (HH: ~ r5*r6 == 0). apply field_is_integral_domain. intros H2; case H0; rewrite H2; ring. intros H2; case H1; rewrite H2; ring. -rewrite <- rdiv4; auto. +rewrite <- rdiv4 ; auto. +rewrite rdiv_r_r; auto. apply field_is_integral_domain. intros H2; case H; rewrite H2; ring. intros H2; case H0; rewrite H2; ring. -rewrite rdiv_r_r; auto. Qed. @@ -379,8 +380,7 @@ transitivity (r1 / r2 * (r4 / r4)). rewrite H1 in |- *. rewrite (ARmul_comm ARth r2 r4) in |- *. rewrite <- rdiv4 in |- *; trivial. - rewrite rdiv_r_r in |- *. - trivial. + rewrite rdiv_r_r in |- * by trivial. apply (ARmul_1_r Rsth ARth). Qed. @@ -780,7 +780,7 @@ Proof. case_eq ((p1 ?= p2)%positive Eq);intros;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _). rewrite (Pcompare_Eq_eq _ _ H0). - rewrite H;[trivial | ring [ (morph1 CRmorph)]]. + rewrite H by trivial. ring [ (morph1 CRmorph)]. fold (NPEpow e2 (Npos (p2 - p1))). rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. @@ -1048,10 +1048,11 @@ Proof. induction p;simpl. intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H). apply IHp. - rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). rewrite H1. rewrite Hp;ring. ring. - reflexivity. + rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + reflexivity. + rewrite H1. ring. rewrite Hp;ring. intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). - rewrite Hp;ring. reflexivity. trivial. + reflexivity. rewrite Hp;ring. trivial. Qed. Theorem Pcond_Fnorm: @@ -1234,13 +1235,15 @@ generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1))) (Pcond_Fnorm _ _ Hcond). intros r r0 Hdiff;induction p;simpl. repeat (rewrite <- rdiv4;trivial). -intro Hp;apply (pow_pos_not_0 Hdiff p). +rewrite IHp. reflexivity. +apply pow_pos_not_0;trivial. +apply pow_pos_not_0;trivial. +intro Hp. apply (pow_pos_not_0 Hdiff p). rewrite (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p) 0). - apply pow_pos_not_0;trivial. ring [Hp]. reflexivity. -apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. -rewrite IHp;reflexivity. -rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. + reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. +rewrite <- rdiv4;trivial. rewrite IHp;reflexivity. +apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. reflexivity. Qed. @@ -1253,9 +1256,9 @@ Theorem Fnorm_crossproduct: PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval in |- *. +rewrite Fnorm_FEeval_PEeval in |- * by apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval in |- *. + rewrite Fnorm_FEeval_PEeval in |- * by apply PCond_app_inv_r with (1 := Hcond). apply cross_product_eq; trivial. apply Pcond_Fnorm. @@ -1473,18 +1476,18 @@ Proof. rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). intro Heq; apply AFth.(AF_1_neq_0). rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (AFth.(AFdiv_def)). - repeat rewrite <- Fnorm_FEeval_PEeval;trivial. - apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7). + repeat rewrite <- Fnorm_FEeval_PEeval ; trivial. + apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). Qed. Theorem Field_simplify_eq_in_correct : @@ -1523,18 +1526,18 @@ Proof. rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). intro Heq; apply AFth.(AF_1_neq_0). rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (AFth.(AFdiv_def)). repeat rewrite <- Fnorm_FEeval_PEeval;trivial. - apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7). + apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). Qed. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 56b08a8fa..4d96bec4c 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -515,12 +515,12 @@ induction x; intros. simpl Nwadd in |- *. repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *. - destruct Reqe; constructor; trivial. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by + (destruct Reqe; constructor; trivial). - rewrite IHx in |- *. - norm. - add_push (- gen_phiNword x); reflexivity. + rewrite IHx in |- *. + norm. + add_push (- gen_phiNword x); reflexivity. Qed. Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. @@ -537,8 +537,8 @@ induction x; intros. simpl Nwscal in |- *. repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *. - destruct Reqe; constructor; trivial. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- * + by (destruct Reqe; constructor; trivial). rewrite IHx in |- *. norm. diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index 70199676c..45b38e2ed 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -1064,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite Padd_ok; rewrite PmulC_ok; rsimpl. intros i P5 H; rewrite H. intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl. + rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. assert (P4 = Q1 ++ P3 ** PX i P5 P6). injection H2; intros; subst;trivial. @@ -1258,7 +1258,7 @@ Section POWER. Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl. Qed. + Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl. Qed. End POWER. @@ -1334,7 +1334,7 @@ Section POWER. rewrite IHpe1;rewrite IHpe2;rrefl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl. rewrite IHpe;rrefl. - rewrite Ppow_N_ok. intros;rrefl. + rewrite Ppow_N_ok by (intros;rrefl). rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. @@ -1425,7 +1425,7 @@ Section POWER. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); destruct (mon_of_pol (norm_subst 0 nil p)). split. - rewrite <- norm_subst_spec. exact I. + rewrite <- norm_subst_spec by exact I. destruct lpe;try destruct H;rewrite <- H; rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial. apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. |