From fc2613e871dffffa788d90044a81598f671d0a3b Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:16 +0000 Subject: ZArith + other : favor the use of modern names instead of compat notations - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/Cring.v | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) (limited to 'plugins/setoid_ring/Cring.v') diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 3d6e53fcd..592efbf6d 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -42,10 +42,9 @@ Section cring. Context {R:Type}`{Rr:Cring R}. Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_. -intros. apply mk_reqe;intros. -rewrite H. rewrite H0. reflexivity. -rewrite H. rewrite H0. reflexivity. - rewrite H. reflexivity. Defined. +Proof. +intros. apply mk_reqe; solve_proper. +Defined. Lemma cring_almost_ring_theory: almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_. @@ -64,11 +63,11 @@ rewrite ring_sub_def ; reflexivity. Defined. Lemma cring_morph: ring_morph zero one _+_ _*_ _-_ -_ _==_ - 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Ncring_initial.gen_phiZ. intros. apply mkmorph ; intros; simpl; try reflexivity. rewrite Ncring_initial.gen_phiZ_add; reflexivity. -rewrite ring_sub_def. unfold Zminus. rewrite Ncring_initial.gen_phiZ_add. +rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add. rewrite Ncring_initial.gen_phiZ_opp; reflexivity. rewrite Ncring_initial.gen_phiZ_mul; reflexivity. rewrite Ncring_initial.gen_phiZ_opp; reflexivity. @@ -80,7 +79,7 @@ Lemma cring_power_theory : intros; apply Ring_theory.mkpow_th. reflexivity. Defined. Lemma cring_div_theory: - div_theory _==_ Zplus Zmult Ncring_initial.gen_phiZ Z.quotrem. + div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem. intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory. simpl. apply ring_setoid. Defined. @@ -102,7 +101,7 @@ Ltac cring_gen := ring_setoid cring_eq_ext cring_almost_ring_theory - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Ncring_initial.gen_phiZ cring_morph N @@ -126,7 +125,7 @@ Ltac cring:= cring_compute. Instance Zcri: (Cring (Rr:=Zr)). -red. exact Zmult_comm. Defined. +red. exact Z.mul_comm. Defined. (* Cring_simplify *) @@ -136,7 +135,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := match lexpr with | ?e::?le => let t := constr:(@Ring_polynom.norm_subst - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Z.quotrem O nil e) in + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in let te := constr:(@Ring_polynom.Pphi_dev _ 0 1 _+_ _*_ _-_ -_ @@ -149,7 +148,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := let t':= fresh "t" in pose (t' := nft); assert (eq1 : t = t'); - [vm_cast_no_check (refl_equal t')| + [vm_cast_no_check (eq_refl t')| let eq2 := fresh "ring" in assert (eq2:(@Ring_polynom.PEeval _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) @@ -159,7 +158,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := ring_setoid cring_eq_ext cring_almost_ring_theory - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Ncring_initial.gen_phiZ cring_morph N @@ -169,7 +168,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := Z.quotrem cring_div_theory get_signZ get_signZ_th - O nil fv I nil (refl_equal nil) ); + O nil fv I nil (eq_refl nil) ); intro eq3; apply eq3; reflexivity| match hyp with | 1%nat => rewrite eq2 -- cgit v1.2.3