From d2bd5d87d23d443f6e41496bdfe5f8e82d675634 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:59 +0000 Subject: 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 --- theories/PArith/BinPos.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'theories/PArith') 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). -- cgit v1.2.3