diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
| commit | d2bd5d87d23d443f6e41496bdfe5f8e82d675634 (patch) | |
| tree | d9cb49b25b4e49ccda4dd424ef2595f53d9e61c0 /theories/PArith | |
| parent | f1c9bb9d37e3bcefb5838c57e7ae45923d99c4ff (diff) | |
Modularization of BinInt, related fixes in the stdlib
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPos.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 5284afe95..19c10f87d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -40,8 +40,8 @@ Include BinPosDef.Pos. (** * Logical Predicates *) -Definition eq := @Logic.eq t. -Definition eq_equiv := @eq_equivalence t. +Definition eq := @Logic.eq positive. +Definition eq_equiv := @eq_equivalence positive. Include BackportEq. Definition lt x y := (x ?= y) = Lt. @@ -525,16 +525,18 @@ Qed. (** ** Inversion of multiplication *) -Lemma mul_1_inversion_l p q : p * q = 1 -> p = 1. +Lemma mul_eq_1_l p q : p * q = 1 -> p = 1. Proof. now destruct p, q. Qed. -Lemma mul_1_inversion_r p q : p * q = 1 -> q = 1. +Lemma mul_eq_1_r p q : p * q = 1 -> q = 1. Proof. now destruct p, q. Qed. +Notation mul_eq_1 := mul_eq_1_l. + (** ** Square *) Lemma square_xO p : p~0 * p~0 = (p*p)~0~0. @@ -1816,7 +1818,7 @@ Proof. destruct Hp1 as (r,Hr). exists r. now rewrite <- Hr, mul_assoc. destruct Hp2 as (r,Hr). exists r. now rewrite <- Hr, mul_assoc. destruct H' as (q,H'). - apply mul_1_inversion_l with q. + apply mul_eq_1 with q. apply mul_reg_l with g. now rewrite mul_assoc, mul_1_r. Qed. @@ -1951,7 +1953,7 @@ Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (only parsing). Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing). Notation Pmult_reg_r := Pos.mul_reg_r (only parsing). Notation Pmult_reg_l := Pos.mul_reg_l (only parsing). -Notation Pmult_1_inversion_l := Pos.mul_1_inversion_l (only parsing). +Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing). Notation Psquare_xO := Pos.square_xO (only parsing). Notation Psquare_xI := Pos.square_xI (only parsing). Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing). |