aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES8
-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
-rw-r--r--parsing/g_tactic.ml412
-rw-r--r--parsing/pptactic.ml5
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/class_tactics.ml4163
-rw-r--r--tactics/equality.ml9
-rw-r--r--tactics/equality.mli3
-rw-r--r--tactics/tacinterp.ml14
-rw-r--r--theories/Ints/num/QvMake.v8
-rw-r--r--theories/NArith/BinPos.v2
-rw-r--r--theories/Numbers/Integer/NatPairs/ZNatPairs.v29
-rw-r--r--theories/Numbers/NatInt/NZOrder.v5
-rw-r--r--theories/Numbers/NatInt/NZTimesOrder.v17
-rw-r--r--theories/Numbers/Natural/Abstract/NIso.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NMinus.v16
-rw-r--r--theories/Numbers/Natural/Abstract/NOrder.v4
-rw-r--r--theories/QArith/Qpower.v12
22 files changed, 230 insertions, 165 deletions
diff --git a/CHANGES b/CHANGES
index e93eb275c..3bba84fc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,7 +10,7 @@ Language
- New experimental typeclass system giving ad-hoc polymorphism and
overloading based on dependent records and implicit arguments.
- New syntax "let| pat := b in c" for let-binding using irrefutable patterns.
-- New syntax "forall `A`, T" for specifying maximally inserted implicit
+- New syntax "forall {A}, T" for specifying maximally inserted implicit
arguments in terms.
Commands
@@ -139,9 +139,9 @@ Type Classes
- New theories directory "theories/Classes" for standard typeclasses
declarations. Module Classes.Relations is a typeclass port of
Relation_Definitions.
-- New experimental "setoid" rewriting tactic "clrewrite" based on typeclasses.
- Classes.Morphisms declares standard morphisms, Classes.SetoidClasses declares
- the new Setoid typeclass.
+- New experimental "setoid" rewriting tactic based on typeclasses.
+ Classes.Morphisms declares standard morphisms, Classes.Equivalence declares
+ the new Setoid typeclass and some derived tactics.
Program
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 77d405e15..a0cbe22b3 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 4d28a22a9..c5a8c756a 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 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.
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4e5d4cb8..96db00e3e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -319,6 +319,10 @@ GEXTEND Gram
[ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
| -> TacId [] ] ]
;
+ opt_by_tactic:
+ [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac
+ | -> None ] ]
+ ;
rename :
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
@@ -471,10 +475,10 @@ GEXTEND Gram
| IDENT "transitivity"; c = constr -> TacTransitivity c
(* Equality and inversion *)
- | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
- TacRewrite (false,l,cl)
- | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
- TacRewrite (true,l,cl)
+ | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+ TacRewrite (false,l,cl,t)
+ | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+ TacRewrite (true,l,cl,t)
| IDENT "dependent"; k =
[ IDENT "simple"; IDENT "inversion" -> SimpleInversion
| IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index da915a5cc..448b78e26 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -821,14 +821,15 @@ and pr_atom1 = function
| TacTransitivity c -> str "transitivity" ++ pr_constrarg c
(* Equality and inversion *)
- | TacRewrite (ev,l,cl) ->
+ | TacRewrite (ev,l,cl,by) ->
hov 1 (str (if ev then "erewrite" else "rewrite") ++
prlist_with_sep
(fun () -> str ","++spc())
(fun (b,m,c) ->
pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
l
- ++ pr_clauses pr_ident cl)
+ ++ pr_clauses pr_ident cl
+ ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a63fd1aeb..f74413704 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -194,7 +194,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Equality and inversion *)
| TacRewrite of
- evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause
+ evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
| TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
(* For ML extensions *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 193f0966e..bb73d4094 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -516,6 +516,33 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
[ a, r ] -> (proof, (a, r, oldt, newt))
| _ -> assert(false)
+(* Adapted from setoid_replace. *)
+
+type hypinfo = {
+ cl : clausenv;
+ prf : constr;
+ rel : constr;
+ l2r : bool;
+ c1 : constr;
+ c2 : constr;
+ c : constr option;
+ abs : (constr * types) option;
+}
+
+let decompose_setoid_eqhyp gl c left2right =
+ let ctype = pf_type_of gl c in
+ let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let rec split_last_two = function
+ | [c1;c2] -> [],(c1, c2)
+ | x::y::z ->
+ let l,res = split_last_two (y::z) in x::l, res
+ | _ -> error "The term provided is not an applied relation" in
+ let others, (c1,c2) = split_last_two args in
+ { cl=eqclause; prf=(Clenv.clenv_value eqclause);
+ rel=mkApp (equiv, Array.of_list others);
+ l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
+
let rewrite_unif_flags = {
Unification.modulo_conv_on_closed_terms = false;
Unification.use_metas_eagerly = true;
@@ -549,8 +576,9 @@ let rewrite2_unif_flags = {
let allowK = true
-let unify_eqn gl (cl, rel, l2r, c1, c2) t =
+let unify_eqn gl hypinfo t =
try
+ let {cl=cl; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
let env' =
try clenv_unify allowK ~flags:rewrite_unif_flags
CONV (if l2r then c1 else c2) t cl
@@ -559,14 +587,26 @@ let unify_eqn gl (cl, rel, l2r, c1, c2) t =
CONV (if l2r then c1 else c2) t cl
in
let c1 = Clenv.clenv_nf_meta env' c1
- and c2 = Clenv.clenv_nf_meta env' c2
- and typ = Clenv.clenv_type env' in
- let (rel, args) = destApp typ in
- let relargs, args = array_chop (Array.length args - 2) args in
- let rel = mkApp (rel, relargs) in
+ and c2 = Clenv.clenv_nf_meta env' c2
+ and rel = Clenv.clenv_nf_meta env' rel in
let car = pf_type_of gl c1 in
- let prf = Clenv.clenv_value env' in
- let res =
+ let prf =
+ if abs = None then
+(* let (rel, args) = destApp typ in *)
+(* let relargs, args = array_chop (Array.length args - 2) args in *)
+(* let rel = mkApp (rel, relargs) in *)
+ let prf = Clenv.clenv_value env' in
+ begin
+ match c with
+ | Some c when occur_meta prf ->
+ (* Refresh the clausenv to not get the same meta twice in the goal. *)
+ hypinfo := decompose_setoid_eqhyp gl c l2r;
+ | _ -> ()
+ end;
+ prf
+ else prf
+ in
+ let res =
if l2r then (prf, (car, rel, c1, c2))
else
try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
@@ -626,25 +666,11 @@ let build_new gl env sigma occs hypinfo concl cstr evars =
| _ -> None, occ
in aux concl 1 cstr
-(* Adapted from setoid_replace. *)
-
-let decompose_setoid_eqhyp gl c left2right =
- let ctype = pf_type_of gl c in
- let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
- let rec split_last_two = function
- | [c1;c2] -> [],(c1, c2)
- | x::y::z ->
- let l,res = split_last_two (y::z) in x::l, res
- | _ -> error "The term provided is not an applied relation" in
- let others, (c1,c2) = split_last_two args in
- eqclause, mkApp (equiv, Array.of_list others), left2right, c1, c2
-
let resolve_all_typeclasses env evd =
resolve_all_evars false (true, 15) env
(fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
-let cl_rewrite_clause_aux hypinfo occs clause gl =
+let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl =
let concl, is_hyp =
match clause with
Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
@@ -670,17 +696,26 @@ let cl_rewrite_clause_aux hypinfo occs clause gl =
let rewtac, cleantac =
match is_hyp with
| Some id ->
-(* let meta = Evarutil.new_meta() in *)
-(* let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in *)
-(* tclTHEN *)
-(* (tclEVARS (evars_of clenv.evd)) *)
- cut_replacing id newt (fun x ->
- refine (mkApp (p, [| mkVar id |]))),
+ let term =
+ match !hypinfo.abs with
+ None -> p
+ | Some (t, ty) ->
+ mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+ in
+ cut_replacing id newt
+ (fun x -> Tactics.refine (mkApp (term, [| mkVar id |]))),
unfold_in_hyp unfoldrefs (([], id), Tacexpr.InHyp)
| None ->
- let meta = Evarutil.new_meta() in
- let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in
- refine term, Tactics.unfold_in_concl unfoldrefs
+(* let term = mkApp (p, [| mkCast (mkMeta goal_meta, DEFAULTcast, newt) |]) in *)
+ let term = match !hypinfo.abs with
+ None -> mkApp (p, [| mkCast (mkMeta goal_meta, DEFAULTcast, newt) |])
+ | Some (t, ty) ->
+ mkApp (mkLambda (Name (id_of_string "newt"), newt,
+ mkLambda (Name (id_of_string "lemma"), ty,
+ mkApp (p, [| mkRel 2 |]))),
+ [| mkMeta goal_meta; t |])
+ in
+ Tactics.refine term, Tactics.unfold_in_concl unfoldrefs
in
let evartac =
let evd = Evd.evars_of undef in
@@ -690,13 +725,14 @@ let cl_rewrite_clause_aux hypinfo occs clause gl =
with UserError (env, e) ->
tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl)
| None ->
- let (_, _, l2r, x, y) = hypinfo in
+ let {l2r=l2r; c1=x; c2=y} = !hypinfo in
raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y)))
(* tclFAIL 1 (str"setoid rewrite failed") gl *)
let cl_rewrite_clause c left2right occs clause gl =
- let hypinfo = decompose_setoid_eqhyp gl c left2right in
- cl_rewrite_clause_aux hypinfo occs clause gl
+ let meta = Evarutil.new_meta() in
+ let hypinfo = ref (decompose_setoid_eqhyp gl c left2right) in
+ cl_rewrite_clause_aux hypinfo meta occs clause gl
open Genarg
open Extraargs
@@ -1021,8 +1057,6 @@ let default_morphism sign m =
let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))])
-let ($) g f = fun x -> g (f x)
-
VERNAC COMMAND EXTEND AddSetoid1
[ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
[ init_setoid ();
@@ -1082,7 +1116,26 @@ END
(** Taken from original setoid_replace, to emulate the old rewrite semantics where
lemmas are first instantiated once and then rewrite proceeds. *)
-let unification_rewrite l2r c1 c2 cl but gl =
+let check_evar_map_of_evars_defs evd =
+ let metas = Evd.meta_list evd in
+ let check_freemetas_is_empty rebus =
+ Evd.Metaset.iter
+ (fun m ->
+ if Evd.meta_defined evd m then () else
+ raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+ in
+ List.iter
+ (fun (_,binding) ->
+ match binding with
+ Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
+ check_freemetas_is_empty rebus freemetas
+ | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_),
+ {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
+ check_freemetas_is_empty rebus1 freemetas1 ;
+ check_freemetas_is_empty rebus2 freemetas2
+ ) metas
+
+let unification_rewrite l2r c1 c2 cl rel but gl =
let (env',c') =
try
(* ~flags:(false,true) to allow to mark occurences that must not be
@@ -1099,23 +1152,31 @@ let unification_rewrite l2r c1 c2 cl but gl =
let cl' = {cl with evd = env' } in
let c1 = Clenv.clenv_nf_meta cl' c1
and c2 = Clenv.clenv_nf_meta cl' c2 in
- cl', Clenv.clenv_value cl', l2r, c1, c2
+ check_evar_map_of_evars_defs env';
+ let prf = Clenv.clenv_value cl' in
+ let prfty = Clenv.clenv_type cl' in
+ if occur_meta prf then
+ {cl=cl'; prf=(mkRel 1); rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
+ else
+ {cl=cl'; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=None}
let get_hyp gl c clause l2r =
match kind_of_term (pf_type_of gl c) with
Prod _ ->
- let cl, rel, _, c1, c2 = decompose_setoid_eqhyp gl c l2r in
+ let hi = decompose_setoid_eqhyp gl c l2r in
let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
- unification_rewrite l2r c1 c2 cl but gl
+ unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl
| _ -> decompose_setoid_eqhyp gl c l2r
let general_s_rewrite l2r c ~new_goals gl =
- let hypinfo = get_hyp gl c None l2r in
- cl_rewrite_clause_aux hypinfo [] None gl
+ let meta = Evarutil.new_meta() in
+ let hypinfo = ref (get_hyp gl c None l2r) in
+ cl_rewrite_clause_aux hypinfo meta [] None gl
let general_s_rewrite_in id l2r c ~new_goals gl =
- let hypinfo = get_hyp gl c (Some id) l2r in
- cl_rewrite_clause_aux hypinfo [] (Some (([],id), [])) gl
+ let meta = Evarutil.new_meta() in
+ let hypinfo = ref (get_hyp gl c (Some id) l2r) in
+ cl_rewrite_clause_aux hypinfo meta [] (Some (([],id), [])) gl
let general_s_rewrite_clause = function
| None -> general_s_rewrite
@@ -1215,15 +1276,3 @@ END
(* TACTIC EXTEND class_apply *)
(* | [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ] *)
(* END *)
-
-(* let default_morphism ?(filter=fun _ -> true) m = *)
-(* match List.filter filter (morphism_table_find m) with *)
-(* [] -> raise Not_found *)
-(* | m1::ml -> *)
-(* if ml <> [] then *)
-(* Flags.if_warn msg_warning *)
-(* (strbrk "There are several morphisms associated to \"" ++ *)
-(* pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ *)
-(* strbrk " is randomly chosen."); *)
-(* relation_morphism_of_constr_morphism m1 *)
-
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 93b555b34..214389f18 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -175,8 +175,13 @@ let general_multi_rewrite l2r with_evars c cl =
(general_rewrite_ebindings l2r c with_evars)
do_hyps
-let general_multi_multi_rewrite with_evars l cl =
- let do1 l2r c = general_multi_rewrite l2r with_evars c cl in
+let general_multi_multi_rewrite with_evars l cl tac =
+ let do1 l2r c =
+ match tac with
+ None -> general_multi_rewrite l2r with_evars c cl
+ | Some tac -> tclTHENSFIRSTn (general_multi_rewrite l2r with_evars c cl)
+ [|tclIDTAC|] (tclCOMPLETE tac)
+ in
let rec doN l2r c = function
| Precisely n when n <= 0 -> tclIDTAC
| Precisely 1 -> do1 l2r c
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 846487f96..91a0d33c6 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -53,7 +53,8 @@ val general_rewrite_in :
val general_multi_rewrite :
bool -> evars_flag -> constr with_ebindings -> clause -> tactic
val general_multi_multi_rewrite :
- evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> tactic
+ evars_flag -> (bool * multi * constr with_ebindings) list -> clause ->
+ tactic option -> tactic
val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
val conditional_rewrite_in :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8de4fcd10..3245c31c7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -742,11 +742,12 @@ let rec intern_atomic lf ist x =
| TacTransitivity c -> TacTransitivity (intern_constr ist c)
(* Equality and inversion *)
- | TacRewrite (ev,l,cl) ->
+ | TacRewrite (ev,l,cl,by) ->
TacRewrite
(ev,
- List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
- clause_app (intern_hyp_location ist) cl)
+ List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+ clause_app (intern_hyp_location ist) cl,
+ Option.map (intern_tactic ist) by)
| TacInversion (inv,hyp) ->
TacInversion (intern_inversion_strength lf ist inv,
intern_quantified_hypothesis ist hyp)
@@ -2105,10 +2106,11 @@ and interp_atomic ist gl = function
| TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
(* Equality and inversion *)
- | TacRewrite (ev,l,cl) ->
+ | TacRewrite (ev,l,cl,by) ->
Equality.general_multi_multi_rewrite ev
(List.map (fun (b,m,c) -> (b,m,interp_constr_with_bindings ist gl c)) l)
(interp_clause ist gl cl)
+ (Option.map (interp_tactic ist) by)
| TacInversion (DepInversion (k,c,ids),hyp) ->
Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
(interp_intro_pattern ist gl ids)
@@ -2403,11 +2405,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
(* Equality and inversion *)
- | TacRewrite (ev,l,cl) ->
+ | TacRewrite (ev,l,cl,by) ->
TacRewrite (ev,
List.map (fun (b,m,c) ->
b,m,subst_raw_with_bindings subst c) l,
- cl)
+ cl,Option.map (subst_tactic subst) by)
| TacInversion (DepInversion (k,c,l),hyp) ->
TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
| TacInversion (NonDepInversion _,_) as x -> x
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v
index e51291a04..c3db44bc6 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Ints/num/QvMake.v
@@ -429,8 +429,8 @@ Module Qv.
Theorem spec_sub x y: wf x -> wf y ->
([sub x y] == [x] - [y])%Q.
intros x y Hx Hy; unfold sub; rewrite spec_add; auto.
- apply wf_opp; auto.
rewrite spec_opp; ring.
+ apply wf_opp; auto.
Qed.
Theorem spec_subc x y: wf x -> wf y ->
@@ -450,8 +450,8 @@ Module Qv.
Theorem spec_sub_norm x y: wf x -> wf y ->
([sub_norm x y] == [x] - [y])%Q.
intros x y Hx Hy; unfold sub_norm; rewrite spec_add_norm; auto.
- apply wf_opp; auto.
rewrite spec_opp; ring.
+ apply wf_opp; auto.
Qed.
Theorem spec_sub_normc x y: wf x -> wf y ->
@@ -945,10 +945,10 @@ Module Qv.
Theorem spec_div x y: wf x -> wf y ->
([div x y] == [x] / [y])%Q.
intros x y Hx Hy; unfold div; rewrite spec_mul; auto.
- apply wf_inv; auto.
unfold Qdiv; apply Qmult_comp.
apply Qeq_refl.
apply spec_inv; auto.
+ apply wf_inv; auto.
Qed.
Theorem spec_divc x y: wf x -> wf y ->
@@ -969,10 +969,10 @@ Module Qv.
Theorem spec_div_norm x y: wf x -> wf y ->
([div_norm x y] == [x] / [y])%Q.
intros x y Hx Hy; unfold div_norm; rewrite spec_mul_norm; auto.
- apply wf_inv; auto.
unfold Qdiv; apply Qmult_comp.
apply Qeq_refl.
apply spec_inv; auto.
+ apply wf_inv; auto.
Qed.
Theorem spec_div_normc x y: wf x -> wf y ->
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 36a845824..f0751f670 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -802,7 +802,7 @@ Qed.
Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
Proof.
intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
- simpl in |- *; auto; intro H;
+ simpl in |- *; auto; intro H ;
[ rewrite (IHp q); trivial
| absurd ((p ?= q) Gt = Eq);
[ elim (Pcompare_not_Eq p q); auto | assumption ]
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index fc9115e20..a40832507 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -210,8 +210,9 @@ destruct n as [n m].
cut (forall p : N, A (p, 0)); [intro H1 |].
cut (forall p : N, A (0, p)); [intro H2 |].
destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
-rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
+rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm).
+apply H2.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1.
induct p. assumption. intros p IH.
apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
now apply <- AS.
@@ -302,13 +303,13 @@ Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
Proof.
intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by
now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
unfold Zeq in H1. rewrite H1. ring.
-rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by
now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
unfold Zeq in H2. rewrite H2. ring.
@@ -318,13 +319,13 @@ Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
Proof.
intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by
now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
unfold Zeq in H2. rewrite H2. ring.
-rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by
now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
unfold Zeq in H1. rewrite H1. ring.
@@ -350,25 +351,25 @@ Qed.
Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
Proof.
unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_l. assumption. ring.
+rewrite min_l by assumption. ring.
Qed.
Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
Proof.
unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_r. assumption. ring.
+rewrite min_r by assumption. ring.
Qed.
Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
Proof.
unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_l. assumption. ring.
+rewrite max_l by assumption. ring.
Qed.
Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
Proof.
unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_r. assumption. ring.
+rewrite max_r by assumption. ring.
Qed.
End NZOrdAxiomsMod.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index bc3600f9c..133bbde4d 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by
now setoid_replace (S n <= n) with False using relation iff by
(apply -> neg_false; apply NZnle_succ_diag_l).
intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r.
-rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m).
+rewrite NZsucc_inj_wd.
+rewrite (NZlt_eq_cases n m).
rewrite or_cancel_r.
+reflexivity.
intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
apply NZlt_neq.
-reflexivity.
Qed.
Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 51d2172de..b51e3d22b 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -60,7 +60,7 @@ split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
apply <- NZle_ngt in H3. le_elim H3.
apply NZlt_asymm in H2. apply H2. now apply LR.
rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZtimes_lt_pred p (S p)); [reflexivity |].
+rewrite (NZtimes_lt_pred p (S p)) by reflexivity.
rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
Qed.
@@ -109,9 +109,9 @@ assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
false_hyp H2 H.
apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l).
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l).
rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
now rewrite H1.
Qed.
@@ -135,9 +135,9 @@ Qed.
Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
Proof.
intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
-now rewrite -> (NZtimes_cancel_l n m p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (NZtimes_cancel_l n m p) by
+(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
Qed.
Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
@@ -149,9 +149,8 @@ Qed.
Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
Proof.
intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
-rewrite -> (NZtimes_cancel_l m n p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 10c341cbf..4df46e20e 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
Proof.
unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq);
-[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |].
+intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
+[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
Qed.
Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index faf4759bd..5e1d5d8c3 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -63,8 +63,8 @@ Proof.
intros n m p; induct p.
intro; now do 2 rewrite minus_0_r.
intros p IH H. do 2 rewrite minus_succ_r.
-rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |].
-rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l.
+rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
+rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l).
reflexivity.
Qed.
@@ -76,13 +76,13 @@ Qed.
Theorem plus_minus : forall n m : N, (n + m) - m == n.
Proof.
-intros n m. rewrite <- plus_minus_assoc. apply le_refl.
+intros n m. rewrite <- plus_minus_assoc by (apply le_refl).
rewrite minus_diag; now rewrite plus_0_r.
Qed.
Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
Proof.
-intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
+intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption.
rewrite plus_comm. apply plus_minus.
Qed.
@@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
Proof.
intros n m p H.
rewrite (plus_comm n m).
-rewrite <- plus_minus_assoc; [assumption |].
+rewrite <- plus_minus_assoc by assumption.
now rewrite (plus_comm m (n - p)).
Qed.
@@ -151,8 +151,8 @@ Proof.
intros n m; cases m.
now rewrite pred_0, times_0_r, minus_0_l.
intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-now apply eq_le_incl.
now rewrite minus_diag, plus_0_r.
+now apply eq_le_incl.
Qed.
Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
@@ -160,9 +160,9 @@ Proof.
intros n m p; induct n.
now rewrite minus_0_l, times_0_l, minus_0_l.
intros n IH. destruct (le_gt_cases m n) as [H | H].
-rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
+rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l.
rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
-rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
+rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r.
now apply <- plus_cancel_l.
assert (H1 : S n <= m); [now apply <- le_succ_l |].
setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 7b4645be3..1e53d8063 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
Proof.
intros n m H1; split; intro H2.
assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
-now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
+now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
[apply <- succ_lt_mono | | |].
assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
apply lt_le_trans with (P m). assumption. apply le_pred_l.
@@ -515,7 +515,7 @@ Qed.
Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
Proof.
-intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
+intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ.
Qed.
Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 78034802f..8672592d9 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -121,8 +121,8 @@ destruct (Qeq_dec a 0).
rewrite q.
repeat rewrite Qpower_positive_0.
reflexivity.
-rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)).
- apply Qpower_not_0_positive; assumption.
+rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by
+ (apply Qpower_not_0_positive; assumption).
apply Qdiv_comp;[|reflexivity].
rewrite Qmult_comm.
rewrite <- Qpower_plus_positive.
@@ -150,8 +150,7 @@ Proof.
intros a n m H.
destruct (Qeq_dec a 0)as [X|X].
rewrite X.
-rewrite Qpower_0.
-assumption.
+rewrite Qpower_0 by assumption.
destruct n; destruct m; try (elim H; reflexivity);
simpl; repeat rewrite Qpower_positive_0; ring_simplify;
reflexivity.
@@ -191,9 +190,8 @@ induction n using Pind.
rewrite Zpos_succ_morphism.
unfold Zsucc.
rewrite Zpower_exp; auto with *; try discriminate.
-rewrite Qpower_plus'; try discriminate.
-rewrite <- IHn.
- discriminate.
+rewrite Qpower_plus' by discriminate.
+rewrite <- IHn by discriminate.
replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring.
ring_simplify.
reflexivity.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 11:38:09 +0000