aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/interface/depends.ml2
-rw-r--r--contrib/interface/xlate.ml7
-rw-r--r--contrib/setoid_ring/Field_theory.v51
-rw-r--r--contrib/setoid_ring/InitialRing.v14
-rw-r--r--contrib/setoid_ring/Ring_polynom.v8
5 files changed, 43 insertions, 39 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 77d405e15d..a0cbe22b36 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -363,7 +363,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacTransitivity c -> depends_of_'constr c acc
(* Equality and inversion *)
- | TacRewrite (_,cbl,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
+ | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
| TacInversion (is, _) -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc
(* For ML extensions *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4d28a22a98..c5a8c756a8 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1011,14 +1011,15 @@ and xlate_tac =
CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
in
CT_replace_with (c1, c2,cl,tac_opt)
- | TacRewrite(false,[b,Precisely 1,cbindl],cl) ->
+ | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) ->
let cl = xlate_clause cl
and c = xlate_formula (fst cbindl)
and bindl = xlate_bindings (snd cbindl) in
if b then CT_rewrite_lr (c, bindl, cl)
else CT_rewrite_rl (c, bindl, cl)
- | TacRewrite(false,_,cl) -> xlate_error "TODO: rewrite of several hyps at once"
- | TacRewrite(true,_,cl) -> xlate_error "TODO: erewrite"
+ | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by"
+ | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once"
+ | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite"
| TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index adaa340db3..f5c5504176 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 56b08a8fa1..4d96bec4cf 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 70199676ca..45b38e2edd 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 08:45:52 +0000